As idealized descriptions of mathematical language, there is a sense in which formal systems specify too little, and there is a sense in which they specify too much. On the one hand, formal languages fail to account for a number of features of informal mathematical language that are essential to the communicative and inferential goals of the subject. On the other hand, many of these features are independent of the choice of a formal foundation, so grounding their analysis on a (...) particular choice of a formal system introduces unnecessary specificity. This chapter begins to map out the design features of mathematical language without descending to the level of formal implementation, drawing on examples from the mathematical literature and insights from the design of computational proof assistants and their libraries. (shrink)

Over the last two decades, social scientists across disciplines have been researching how value is extracted and governed in the reproductive bioeconomy, which broadly refers to the various ways reproductive tissues, bodies, services, customers, workers, and data are inserted into capitalist modes of accumulation. While many of these studies are empirically grounded in single country–based analyses, this paper proposes an integrative political economy framework, structured around the concept of “global fertility chains.” The latter articulates the reproductive bioeconomy as a nexus (...) of intraconnected practices, operations, and transactions between enterprises, states, and households across the globe, through which reproductive services and commodities are produced, distributed, and consumed. Employing a diffractive reading of the literature on commodity chains and care chains, this unified approach scrutinizes the coproduction of value, biology, and technoscience and their governance mechanisms in the accumulation of capital by taking into account the unevenly developed geographies of global fertility chains, their reliance on women’s waged and unwaged reproductive labor, and the networked role of multiple actors at multiple scales without losing sight of the constitutive role of national states in creating demand, organizing supply, and accommodating the distribution of surplus value. We empirically ground this integrative political economy approach of the reproductive bioeconomy through collaborative, multisited fieldwork on transnational reproduction networks in Israel/palestine, Romania, Georgia, and Spain. (shrink)

This article presents qualitative research conducted in an Israeli ova `extraction' clinic in Romania. Following on from a piece written by Jyotsna Gupta and published in this journal in February 2006, this article asks what kinds of feminist alliances can or should be made in the arena of reproductive technologies. In conversation with Gupta, the author asks whether `an ethic of universal human dignity' is possible or desirable. This article looks to the voices of Romanian egg sellers themselves as a (...) source of theoretical and political direction for transnational feminists who try to think about responses to reproductive technologies. (shrink)

Of all the demands that mathematics imposes on its practitioners, one of the most fundamental is that proofs ought to be correct. It has been common since the turn of the twentieth century to take correctness to be underwritten by the existence of formal derivations in a suitable axiomatic foundation, but then it is hard to see how this normative standard can be met, given the differences between informal proofs and formal derivations, and given the inherent fragility and complexity of (...) the latter. This essay describes some of the ways that mathematical practice makes it possible to reliably and robustly meet the formal standard, preserving the standard normative account while doing justice to epistemically important features of informal mathematical justification. (shrink)

We present a formal system, E, which provides a faithful model of the proofs in Euclid's Elements, including the use of diagrammatic reasoning.

In a wide range of fields, the word “modular” is used to describe complex systems that can be decomposed into smaller systems with limited interactions between them. This essay argues that mathematical knowledge can fruitfully be understood as having a modular structure and explores the ways in which modularity in mathematics is epistemically advantageous.

On a traditional view, the primary role of a mathematical proof is to warrant the truth of the resulting theorem. This view fails to explain why it is very often the case that a new proof of a theorem is deemed important. Three case studies from elementary arithmetic show, informally, that there are many criteria by which ordinary proofs are valued. I argue that at least some of these criteria depend on the methods of inference the proofs employ, and that (...) standard models of formal deduction are not well-equipped to support such evaluations. I discuss a model of proof that is used in the automated deduction community, and show that this model does better in that respect. (shrink)

In 1837, Dirichlet proved that there are infinitely many primes in any arithmetic progression in which the terms do not all share a common factor. Modern presentations of the proof are explicitly higher-order, in that they involve quantifying over and summing over Dirichlet characters, which are certain types of functions. The notion of a character is only implicit in Dirichlet’s original proof, and the subsequent history shows a very gradual transition to the modern mode of presentation. In this essay, we (...) describe an approach to the philosophy of mathematics in which it is an important task to understand the roles of our ontological posits and assess the extent to which they enable us to achieve our mathematical goals. We use the history of Dirichlet’s theorem to understand some of the reasons that functions are treated as ordinary objects in contemporary mathematics, as well as some of the reasons one might want to resist such treatment. We also use these considerations to illuminate the formal treatment of functions and objects in Frege’s logical foundation, and we argue that his philosophical and logical decisions were influenced by many of the same factors. (shrink)

A number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.

We show that certain model-theoretic forcing arguments involving subsystems of second-order arithmetic can be formalized in the base theory, thereby converting them to effective proof-theoretic arguments. We use this method to sharpen the conservation theorems of Harrington and Brown-Simpson, giving an effective proof that WKL+0 is conservative over RCA0 with no significant increase in the lengths of proofs.

A notion called Herbrand saturation is shown to provide the model-theoretic analogue of a proof-theoretic method, Herbrand analysis, yielding uniform model-theoretic proofs of a number of important conservation theorems. A constructive, algebraic variation of the method is described, providing yet a third approach, which is finitary but retains the semantic flavor of the model-theoretic version.

In 1837, Dirichlet proved that there are infinitely many primes in any arithmetic progression in which the terms do not all share a common factor. We survey implicit and explicit uses ofDirichlet characters in presentations of Dirichlet’s proof in the nineteenth and early twentieth centuries, with an eye toward understanding some of the pragmatic pressures that shaped the evolution of modern mathematical method.

is a fragment of first-order aritlimetic so weak that it cannot prove the totality of an iterated exponential fimction. Surprisingly, however, the theory is remarkably robust. I will discuss formal results that show that many theorems of number theory and combinatorics are derivable in elementary arithmetic, and try to place these results in a broader philosophical context.

We show that the theory ATR 0 is equivalent to a second-order generalization of the theory $\widehat{ID}_{ . As a result, ATR 0 is conservative over $\widehat{ID}_{ for arithmetic sentences, though proofs in ATR 0 can be much shorter than their $\widehat{ID}_{ counterparts.

Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects (...) of forcing that are useful in this respect, and some sample applications. The latter include ways of obtaining conservation results for classical and intuitionistic theories, interpreting classical theories in constructive ones, and constructivizing model-theoretic arguments. (shrink)

We describe a model-theoretic approach to ordinal analysis via the finite combinatorial notion of an α-large set of natural numbers. In contrast to syntactic approaches that use cut elimination, this approach involves constructing finite sets of numbers with combinatorial properties that, in nonstandard instances, give rise to models of the theory being analyzed. This method is applied to obtain ordinal analyses of a number of interesting subsystems of first- and second-order arithmetic.

We develop fundamental aspects of the theory of metric, Hilbert, and Banach spaces in the context of subsystems of second-order arithmetic. In particular, we explore issues having to do with distances, closed subsets and subspaces, closures, bases, norms, and projections. We pay close attention to variations that arise when formalizing definitions and theorems, and study the relationships between them.

We analyze the pointwise convergence of a sequence of computable elements of L1 in terms of algorithmic randomness. We consider two ways of expressing the dominated convergence theorem and show that, over the base theory RCA0, each is equivalent to the assertion that every Gδ subset of Cantor space with positive measure has an element. This last statement is, in turn, equivalent to weak weak Königʼs lemma relativized to the Turing jump of any set. It is also equivalent to the (...) conjunction of the statement asserting the existence of a 2-random relative to any given set and the principle of Σ2 collection. (shrink)

Solovay has shown that if $\cal{O}$ is an open subset of $P(\omega)$ with code $S$ and no infinite set avoids $\cal{O}$ , then there is an infinite set hyperarithmetic in $S$ that lands in $\cal{O}$ . We provide a direct proof of this theorem that is easily formalizable in $ATR_0$.

Extending Gödel's Dialectica interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

Using a slight generalization, due to Palmgren, of sheaf semantics, we present a term-model construction that assigns a model to any first-order intuitionistic theory. A modification of this construction then assigns a nonstandard model to any theory of arithmetic, enabling us to reproduce conservation results of Moerdijk and Palmgren for nonstandard Heyting arithmetic. Internalizing the construction allows us to strengthen these results with additional transfer rules; we then show that even trivial transfer axioms or minor strengthenings of these rules destroy (...) conservativity over HA. The analysis also shows that nonstandard HA has neither the disjunction property nor the explicit definability property. Finally, careful attention to the complexity of our definitions allows us to show that a certain weak fragment of intuitionistic nonstandard arithmetic is conservative over primitive recursive arithmetic. (shrink)

Using a slight generalization, due to Palmgren, of sheaf semantics, we present a term-model construction that assigns a model to any first-order intuitionistic theory. A modification of this construction then assigns a nonstandard model to any theory of arithmetic, enabling us to reproduce conservation results of Moerdijk and Palmgren for nonstandard Heyting arithmetic. Internalizing the construction allows us to strengthen these results with additional transfer rules; we then show that even trivial transfer axioms or minor strengthenings of these rules destroy (...) conservativity over HA. The analysis also shows that nonstandard HA has neither the disjunction property nor the explicit definability property. Finally, careful attention to the complexity of our definitions allows us to show that a certain weak fragment of intuitionistic nonstandard arithmetic is conservative over primitive recursive arithmetic. (shrink)

The metamathematical tradition, tracing back to Hilbert, employs syntactic modeling to study the methods of contemporary mathematics. A central goal has been, in particular, to explore the extent to which infinitary methods can be understood in computational or otherwise explicit terms. Ergodic theory provides rich opportunities for such analysis. Although the field has its origins in seventeenth century dynamics and nineteenth century statistical mechanics, it employs infinitary, nonconstructive, and structural methods that are characteristically modern. At the same time, computational concerns (...) and recent applications to combinatorics and number theory force us to reconsider the constructive character of the theory and its methods. This paper surveys some recent contributions to the metamathematical study of ergodic theory, focusing on the mean and pointwise ergodic theorems and the Furstenberg structure theorem for measure preserving systems. In particular, I characterize the extent to which these theorems are nonconstructive, and explain how proof-theoretic methods can be used to locate their "constructive content.". (shrink)

Neo-Fregean logicists claim that Hume’s Principle (HP) may be taken as an implicit definition of cardinal number, true simply by fiat. A long-standing problem for neo-Fregean logicism is that HP is not deductively conservative over pure axiomatic second-order logic. This seems to preclude HP from being true by fiat. In this paper, we study Richard Kimberly Heck’s Two-Sorted Frege Arithmetic (2FA), a variation on HP which has been thought to be deductively conservative over second-order logic. We show that it isn’t. (...) In fact, 2FA is not conservative over n-th order logic, for all $n \geq 2$. It follows that in the usual one-sorted setting, HP is not deductively Field-conservative over second- or higher-order logic. (shrink)

We argue that the language of Zermelo Fraenkel set theory with definitions and partial functions provides the most promising bedrock semantics for communicating and sharing mathematical knowledge. We then describe a syntactic sugaring of that language that provides a way of writing remarkably readable assertions without straying far from the set-theoretic semantics. We illustrate with some examples of formalized textbook definitions from elementary set theory and point-set topology. We also present statistics concerning the complexity of these definitions, under various complexity (...) measures. (shrink)

This article utilises feminist technoscience studies’ notions of bodily ‘materialisation’ and ‘ontological choreographies’, offering a cyborg feminist account of ‘bioavailability’ as embodied becomings, rather than a fixed ontological state of being. Drawn from 2 years’ ethnographic study in in vitro fertilisation clinics in Spain with migrant women who provided eggs to the cross-border in vitro fertilisation industry, this work explores how global understandings of race and inequalities, clinical practices and women’s own emotional and physical labours collectively produce bioavailability. Through examples (...) from observations and interviews in in vitro fertilisation clinics, we examined women’s embodied stories to understand the ways in which bioavailability becomes. The article demonstrates a novel way in which to think about ‘bioavailability’, a concept which has already been of enormous use to the social sciences since its introduction by Lawrence Cohen. We examine recent configurations of bodily extraction in the reproduction–migration nexus that help us rethink the concept of bioavailability. (shrink)

The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term εx A denotes some x satisfying A(x), if there is one. In Hilbert's Program, the epsilon terms play the role of ideal elements; the aim of Hilbert's finitistic consistency proofs is to give a procedure which removes such terms (...) from a formal proof. The procedures by which this is to be carried out are based on Hilbert's epsilon substitution method. The epsilon calculus, however, has applications in other contexts as well. The first general application of the epsilon calculus was in Hilbert's epsilon theorems, which in turn provide the basis for the first correct proof of Herbrand's theorem. More recently, variants of the epsilon operator have been applied in linguistics and linguistic philosophy to deal with anaphoric pronouns. (shrink)

We use model-theoretic methods described in [3] to obtain ordinal analyses of a number of theories of first- and second-order arithmetic, whose proof-theoretic ordinals are less than or equal to Γ0.

A seminal theorem due to Weyl [14] states that if $(a_n)$ is any sequence of distinct integers, then, for almost every $x \in \mathbb{R}$, the sequence $(a_n x)$ is uniformly distributed modulo one. In particular, for almost every $x$ in the unit interval, the sequence $(a_n x)$ is uniformly distributed modulo one for every computable sequence $(a_n)$ of distinct integers. Call such an $x$ UD random. Here it is shown that every Schnorr random real is UD random, but there are (...) Kurtz random reals that are not UD random. On the other hand, Weyl's theorem still holds relative to a particular effectively closed null set, so there are UD random reals that are not Kurtz random. (shrink)

“Now, in calm weather, to swim in the open ocean is as easy to the practised swimmer as to ride in a spring-carriage ashore. But the awful lonesomeness is intolerable. The intense concentration of self in the middle of such a heartless immensity, my God! who can tell it? Mark, how when sailors in a dead calm bathe in the open sea—mark how closely they hug their ship and only coast along her sides.” (Herman Melville, Moby Dick, Chapter 94).

In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type. Here we extend Gödel's T to theories Pn of “predicative” functionals, which are defined using Martin-Löf's universes of transfinite types. We then extend Gödel's interpretation to the theories of arithmetic inductive definitions IDn, so that each IDn is interpreted in the corresponding Pn. Since the strengths of the theories IDn are cofinal in the ordinal Γ0, as (...) a corollary this analysis provides an ordinal-free characterization of the <Γ0-recursive functions. (shrink)

The notion of a function from ℕ to ℕ defined by recursion on ordinal notations is fundamental in proof theory. Here this notion is generalized to functions on the universe of sets, using notations for well orderings longer than the class of ordinals. The generalization is used to bound the rate of growth of any function on the universe of sets that is Σ1-definable in Kripke–Platek admissible set theory with an axiom of infinity. Formalizing the argument provides an ordinal analysis.

Summary. A constructive realizablity interpretation for classical arithmetic is presented, enabling one to extract witnessing terms from proofs of 1 sentences. The interpretation is shown to coincide with modified realizability, under a novel translation of classical logic to intuitionistic logic, followed by the Friedman-Dragalin translation. On the other hand, a natural set of reductions for classical arithmetic is shown to be compatible with the normalization of the realizing term, implying that certain strategies for eliminating cuts and extracting a witness from (...) the proof of a 1 sentence are insensitive to the order in which reductions are applied. (shrink)

V’yugin has shown that there are a computable shift-invariant measure on $2^{\mathbb{N}}$ and a simple function $f$ such that there is no computable bound on the rate of convergence of the ergodic averages $A_{n}f$ . Here it is shown that in fact one can construct an example with the property that there is no computable bound on the complexity of the limit; that is, there is no computable bound on how complex a simple function needs to be to approximate the (...) limit to within a given $\varepsilon$. (shrink)

To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean’s (...) elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved. (shrink)