The question of whether the use of a certain method or axiom isnecessary in order to prove a given theorem is widespread inmathematics. Two historical examples are particularly prominent: theparallel postulate in Euclidean geometry, and the axiom of choice inset theory. In both cases, one demonstrates that the axiom is indeednecessary by proving a “reversal” from the theorem to theaxiom: that is, by assuming the theorem and deriving the axiom fromit, relative to a set of background assumptions known as the basetheory. Reverse mathematics is a program in mathematical logic thatseeks to give precise answers to the question of which axioms arenecessary in order to prove theorems of “ordinarymathematics”: roughly speaking, those concerning structures thatare either themselves countable, or which can be represented bycountable “codes”. This includes many fundamental theoremsof real, complex, and functional analysis, countable algebra,countable infinitary combinatorics, descriptive set theory, andmathematical logic. Countable codes are just sets of natural numbers,so these theorems can be formalized in a language with minimalexpressive resources, quantifying only over natural numbers and setsof natural numbers, known as second-order arithmetic.

Formalizing theorems from diverse areas of mathematics within aunified framework opens the door to comparing them. For example, theHeine–Borel covering theorem, which asserts the compactness ofthe closed unit interval, is equivalent to the compactness theorem forfirst-order logic. The connection between these two compactnessprinciples is thus not merely an analogy, but a precisecorrespondence: they both express the same underlyingcomputability-theoretic closure condition, also expressed by the setexistence principle known as weak König’s lemma, which isnecessary and sufficient to prove the two theorems.

Questions of necessity and sufficiency in mathematics havehistorically been closely linked to issues in the foundations ofmathematics, and in particular to the foundational programs initiatedin the early twentieth century: constructivism, finitism, andpredicativism. Using reverse mathematical results to determine theextent of the mathematics that can be developed on the basis of agiven foundational doctrine is a natural and appealing idea,especially since many of the systems studied in reverse mathematicshave technical and historical links to those very foundationalprograms. In addition to its intrinsic mathematical interest, reversemathematics thus has a role to play in the foundations of mathematics,as well as in addressing broader philosophical issues such as the roleof mathematics in science and the indispensability argument.

This entry aims to give the reader a broad introduction to thehistory, methodology, and results of the reverse mathematics program,with a particular focus on its connections to foundational programs.§1 provides a historical introduction to reverse mathematics, tracingits development from the nineteenth century arithmetization ofanalysis, through the development of proof theory and computabilitytheory in the twentieth century, until its emergence as a subject inits own right in the mid-1970s.§2 provides an introduction to subsystems of second-order arithmetic,the formal systems used in reverse mathematics.§3 introduces the base theory \(\sfRCA_0\), sketches the coding used torepresent a wide variety of mathematical objects within it, andexplains some fundamental connections between reverse mathematics andcomputability theory.§4 gives an overview of the other four of the Big Five subsystems:\(\WKL_0\) (§4.1), \(\ACA_0\) (§4.1), \(\ATR_0\) (§4.3), and \(\Pi^1_1\text{-}\CA_0\) (§4.4), including some of the theorems equivalent to the characteristicaxioms of each system (weak König’s lemma, arithmeticalcomprehension, arithmetical transfinite recursion, and \(\Pi^1_1\)comprehension). Building on the previous two sections,§5 explores the connections between the Big Five subsystems andtraditional foundational programs including constructivism (§5.1), finitism (§5.2–§5.3), and predicativism (§5.4–§5.5). The final section (§6) suggests further reading and provides pointers to other resources onreverse mathematics.

• 1. A Historical Introduction to Reverse Mathematics
  • 1.1 Mathematical necessity and the axiomatic method
  • 1.2 The arithmetization of analysis
  • 1.3 From recursive counterexamples to reverse mathematics
  • 1.4 The early development of reverse mathematics
• 2. Second-Order Arithmetic and Its Subsystems
  • 2.1 The language of second-order arithmetic
  • 2.2 Semantics for second-order arithmetic
  • 2.3 Axioms of second-order arithmetic
• 3. The Base Theory
  • 3.1 Recursive comprehension
  • 3.2 Pairing, sequences, and the basics of coding
  • 3.3 Integer, rational, and real numbers
  • 3.4 \(\omega\)-models and computability
• 4. The Big Five
  • 4.1 Weak König’s lemma
  • 4.2 Arithmetical comprehension
  • 4.3 Arithmetical transfinite recursion
  • 4.4 \(\Pi^1_1\) comprehension
• 5. Foundational Programs and Reverse Mathematics
  • 5.1 Computable mathematics, constructive mathematics, and \(\sfRCA_0\)
  • 5.2 Finitism and \(\sfRCA_0\)
  • 5.3 Finitistic reductionism and \(\WKL_0\)
  • 5.4 Arithmetical definability and predicativity
  • 5.5 Arithmetical transfinite recursion and the limits of predicativity
• 6. Further Reading
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. A Historical Introduction to Reverse Mathematics

1.1 Mathematical necessity and the axiomatic method

Reverse mathematics is a relatively young subfield of mathematicallogic, having made its start in the mid-1970s as an outgrowth ofcomputability theory. In the field’s founding paper (Friedman 1975), Harvey Friedmanbegins by asking

What are the proper axioms to use in carrying out proofs of particulartheorems, or bodies of theorems, in mathematics? What are those formalsystems which isolate the essential principles needed to prove them?(1975: 235)

Friedman’s notion of the proper axioms to prove a given theoremis one on which not only can the theorem can be proved from theaxioms, but the axioms can be proved from the theorem. Put anotherway, the proper axioms are necessary in order to prove the theorem,and not merely sufficient.

In this sense, finding the proper axioms to prove a given theorem is along-standing endeavour in mathematics. Euclid’s fifthpostulate, the parallel postulate, is a well-worn example. It isnecessary in order to prove many important results in Euclideangeometry, such as the Pythagorean theorem, but mathematiciansthroughout history have found the postulate disquieting. Lewis (1920)suggests that Euclid was trying to find the right principles fromwhich to prove the propositions from 29 onwards, and that the parallelpostulate was in the end given as a postulate simply because no otherway to prove those propositions was found. Attempts would be madethroughout antiquity to prove the parallel postulate, notably byProclus, as well as in the medieval Islamic world and in the modernperiod (Bonola 1912; Rosenfeld 1976 [1988]). We now know that therewas an insurmountable barrier to these attempts. As discoveredin the nineteenth century, there are models of non-Euclidean geometry which satisfy the otherpostulates but do not satisfy the parallel postulate. Therefore, theparallel postulate does not follow from the others.

To see that the parallel postulate is necessary to prove thePythagorean theorem, we need areversal from theorem toaxiom. We do this by giving a proof of the parallel postulate from thePythagorean theorem, and thereby establishing the implication

while being careful to use only the other geometrical postulates andnot reason circularly by using the parallel postulate itself. Sincethe Pythagorean theorem follows from the parallel postulate, the twostatements are equivalent, modulo the other geometrical postulates.Moreover, because the parallel postulate is independent from the otherpostulates, it follows from this equivalence that the Pythagoreantheorem is too: it is true in all and only those geometries which areEuclidean, i.e., those in which the parallel postulate holds.

Hilbert’s axiomatizations of Euclidean and non-Euclideangeometries in hisGrundlagen der Geometrie (1899) provided asetting in which such proofs of equivalence between principles couldbe given. In particular, Hilbert’s axioms provided somethinglike a formalbase theory which could prove the Pythagoreantheorem from the parallel postulate, and conversely. Such proofs arenow standard exercises in undergraduate geometry textbooks (e.g.,Hartshorne 2000). Crucially, Hilbert’s base theory does notprove the parallel postulate: as Hilbert showed, the base theory hasanalytical models (ones constructed from the real numbers) in whichthe parallel postulate is true, but also ones in which it is false. Ona purely logical level, ifT is a formal theory such that both\(\varphi\) and \(\psi\) are provable inT, thenTproves that they are equivalent. Similarly, if both \(\neg\varphi\)and \(\neg\psi\) are provable, thenT also proves that\(\varphi\) and \(\psi\) are equivalent. The independence of theparallel postulate from Hilbert’s base theory thus shows thatthe equivalence between the parallel postulate and the Pythagoreantheorem is non-trivial, since it cannot be established on either thetrivial grounds that both are provable, or on the trivial grounds thatboth are refutable.

Although this entry will not engage further with the study ofequivalences in geometry, it should be noted that this field remainsalive and well. For example, the work of Pambuccian (1996, 2001, 2006,2009) is explicitly philosophical in its motivation, and has excitedinterest amongst philosophers engaged with questions of methodologicaland logical purity in mathematics. Some representative pieces areArana (2008; Arana & Mancosu 2012; Baldwin 2013; Pambuccian 2019),Pambuccian & Schacht (2021). Dean (2021) engages with reversemathematics and theGrundlagen der Geometrie from a differentdirection, namely their bearing on theFrege–Hilbert controversy.

A second historical precedent is theaxiom of choice (AC) in set theory. Zermelo (1904) brought widespread attention tothe axiom of choice by appealing to it in his proof of thewell-ordering theorem. In the process he ignited a controversy overthe principle, which attracted a wide range of criticisms from suchmathematical luminaries asHenri Poincaré and Émile Borel (Moore 1982). In his response to thesecriticisms, Zermelo (1908) argued that AC is “necessary forscience”, and in particular that there are

elementary and fundamental theorems and problems that, in my opinion,could not be dealt with at all without the principle of choice.(Zermelo 1967: 187–188)

The “elementary and fundamental theorems and problems” towhich Zermelo refers include such basic matters as whether thecardinalities of two sets are always comparable. As in the case of thePythagorean theorem, history has borne out Zermelo’s contentionthat the axiom of choice is necessary for proving such statements, inthe sense that they imply the axiom of choice modulo the other axiomsofZermelo–Fraenkel set theory (ZF) (Jech 1973; Rubin & Rubin 1963, 1985; Howard & Rubin1998). Paul Cohen’s discovery offorcing demonstrated a further similarity with the case of the parallelpostulate, as the axiom of choice was shown to be formally independentof the base theory ZF. The equivalence of AC with statements like thewell-ordering theorem was thereby shown to be non-trivial, just likethe equivalence of the parallel postulate with statements like thePythagorean theorem.

However, there are substantive differences between reverse mathematicsand the study of equivalences of the axiom of choice, and equivalencesprovable over ZF more generally. Reverse mathematics is concerned withstructures that can be represented by sets of natural numbers, and notwith sets of arbitrary cardinality. As we shall see in the course ofthis entry, these structures and the theorems that concern them arefar more extensive than one might at first suspect, including asubstantial part of what is often called “ordinarymathematics”. While the axiom of choice is equivalent to manyimportant general theorems in topology, functional analysis, andcombinatorics, the full generality of these results is rarely requiredin everyday mathematical applications. The fundamental characterizingtheorems about “concrete” structures such as the realnumbers require only the axioms of weak subsystems of second-orderarithmetic. Finally, the axiom of choice is also distinguished by itspurely existential nature: it does not give a method or procedure forchoosing elements from an infinite family of sets, but merely assertsthat some such choice exists. The set existence principles studied inreverse mathematics, on the other hand, all have acomputability-theoretic aspect and are thus closely connected todefinability, something which forms a major theme of this entry. Forprinciples like arithmetical comprehension (§4.2) this connection lies on the surface, while for others like weakKönig’s lemma (§4.1) it is less immediately apparent but no less real (Eastaugh 2019).

1.2 The arithmetization of analysis

Although many aspects of reverse mathematics are rooted in geometry, adifferent part of mathematics supplies many others: analysis. This isthe part of mathematics concerned with the continuum of real numbersand the many structures which are based upon it. Analysis suppliesmuch of the subject matter as many theorems of analysis turn out to beequivalent to the set existence principles studied in reversemathematics. It also much of the reverse mathematician’stoolkit, namely the diverse array of coding schemes required torepresent complex objects and structures within second-orderarithmetic.

Both aspects of the connection between reverse mathematics andanalysis can be traced to the nineteenth century, when mathematics ingeneral, and analysis in particular, underwent a sea change. Onedriving force was the desire to increase the level of rigour inmathematical analysis, replacing geometric intuition and infinitesimalquantities with “arithmetical” arguments based onproto-set-theoretic principles and constructions.

Of the many important advances that were made during thearithmetization of analysis, as it came to be called, we cansingle out three as particularly fundamental: the new definitions ofconvergent sequence and limit; of continuous function; and of the realnumber system itself. Suppose \(x = \str{x_n : n \in \bbN}\) is aninfinite sequence of real numbers. Then the real number \(y\) is thelimit of the sequence \(x\), in symbols \(y = \lim_{n \to\infty} x_n\), if for every real number \(\varepsilon \gt 0\) thereexists a natural number \(N\) such that for all natural numbers \(n\gt N\), \(|x_n - y| \lt \varepsilon\). This definition of the notionof a limit depends only on the concepts of real and natural numbers,together with the arithmetical operations, absolute value, order, andthe concept of an infinite sequence: no recourse to geometricalnotions is required. This development set the stage for a morethoroughgoing arithmetization in which the concept of a real numberwas similarly reduced.

Like the notions of continuity and convergence, definitions of thereal numbers underwent significant evolutions during this period.Historically, irrational numbers had been conceived of geometrically,for instance the square root of 2 as the length of the diagonal acrossthe unit square, or \(\pi\) as the ratio of the circumference of acircle to its diameter. While the analysts who developed arithmeticaldefinitions of the real numbers during the nineteenth century did notaim to eliminate this geometrical aspect, they tended to view appealsto geometric intuition in proofs with suspicion, and wanted to give atheory of real numbers that did not depend on such intuitiveconsiderations.

One such theory was that of Georg Cantor, who gave a construction ofreal numbers in terms of convergent sequences of rational numbers(Cantor 1872, 1883). With some anachronism, let \(x : \bbN\to \bbQ\)be a total function from natural numbers to rational numbers. We canthink of \(x\) as an infinite sequence of rationals \(\str{x_n : n \in\bbN}\). \(x\) is afundamental sequence if there exists \(k\in \bbN\) such that for every positive rational number\(\varepsilon\), \(|x_{n+m} - x_n| \lt \varepsilon\) for every \(m,n\in \bbN\) where \(n \gt k\). We can then conventionally associatewith the fundamental sequence \(x\) the real number \(y = \lim x\),the value that the sequence \(x\) achieves in the limit. Moreover,Cantor showed how the operations of addition, subtraction,multiplication, and division could be extended to real numbersconsidered as the limits of fundamental sequences.

Richard Dedekind, in his 1872 monographStetigkeit und irrationale Zahlen,developed a substantially different approach to the real numbers as“cuts” or partitions of the rational numbers into upperand lower parts. First worked out for an introductory course that hetaught at the Zürich Polytechnic in 1858, Dedekind’sapproach takes the real numbers to be in correspondence not with thelimits of convergent sequences of rational numbers, but with arbitrary“cuts” in the rational numbers. A cut is a disjoint pair\((A_1,A_2)\) of nonempty sets of rational numbers, such that \(A_1\cup A_2 = \bbQ\) and \(A_1\) is downwards closed while \(A_2\) isupwards closed: if \(p\) and \(q\) are rational numbers such that \(p\lt q\), if \(q \in A_1\) then \(p \in A_1\), and if \(p \in A_2\)then \(q \in A_2\). A real number \(x \in \bbR\) corresponds to, or is“created by”, a cut \((A_1,A_2)\) just in case for every\(p \in A_1\), \(p \leq x\), and for every \(q \in A_2\), \(x \ltq\).

Despite their conceptual differences, Dedekind and Cantor’sconstructions have much in common. They both take the rational numbersas the basis for the real numbers, together with some set-theoreticmachinery. In Dedekind’s case this involves the notion of anarbitrary subset of the rational numbers, while in Cantor’s itis the notion of an infinite sequence of rational numbers. Talk ofrational numbers can, as Cantor and Dedekind knew, be reduced inprinciple to talk of natural numbers, and their definitions can beseen as reducing the real numbers to the “arithmetical”:the natural numbers, and some part of the theory of sets. That part isin fact quite small, requiring only the concept of a set of naturalnumbers, and both Cantor and Dedekind’s definitions of a realnumber can (with some modifications) be formalized in second-orderarithmetic (see§3.3 for the former and Simpson (1984) for the latter).

In addition to its groundbreaking definition of the real numbers ascuts in the rationals, and its formulation of the principle ofcontinuity as the essential axiom of the arithmetical continuum,Dedekind (1872) also contains a striking anticipation of the method ofreversals, as first noted by Sieg (1988: 344, fn. 16). The finalsection ofStetigkeit und irrationale Zahlen is devoted tofundamental theorems of analysis, namely the monotone convergencetheorem and the Cauchy convergence theorem. Dedekind shows that notonly can the principle of continuity be used to derive these theorems,but that the theorems can in turn be used to derive the principle ofcontinuity.

From this point onwards, the story of arithmetization becomes bound upwith the story of logic. The development of quantificational logic byFrege and Pierce, the symbolism of Peano, and the development of typetheory by Russell all played important parts in the emergence of arecognizably modern framework suited for the formalization ofarithmetic and analysis in the work of the Hilbert school, mostnotably in Hilbert’s collaborations with Wilhelm Ackermann andPaul Bernays. These culminated in Hilbert and Bernays’smonumentalGrundlagen der Mathematik, published in twovolumes (1934, 1939). Interested readers may have an easier timeobtaining the second editions (1968, 1970).

Amongst the many contributions of Hilbert and Bernays’sGrundlagen to the foundations of mathematics, the mostobvious immediate connection with reverse mathematics and the study ofsubsystems of second-order arithmetic comes in Supplement IV of volume2 (1939/1970). This supplement introduces several formalisms forarithmetic which can be seen as ancestors of the axiom system\(\sfZ_2\) of second-order arithmetic used in reverse mathematics,defined in§2.3 of this entry. The bulk of Supplement IV uses a systemH whichincludes both free and bound first- and second-order variables. Theintended range of the first-order variables is the natural numbers.The second-order terms are unary function terms, not set or predicateterms, and the intended interpretation of the second-order variablesis as functions \(f : \bbN\to \bbN\) (Hilbert & Bernays 1970:467). These aspects of the formalism are quite similar to the language\(\calL_2\) of second-order arithmetic, but in other respects thesystemH diverges quite markedly from contemporary practice.One aspect is the inclusion of free formula variables, which someauthors such as Sanders (2022: 2) have interpreted as introducingthird-order parameters and operators into the system. Another is thatthe system uses a form of Hilbert’sepsilon calculus, although the revised formalismK introduced in section F ofSupplement IV shows how the systemH can be modified to removethis dependency. The use of function terms, rather than set terms,persisted into later work such as that of Grzegorczyk, Mostowski,& Ryll-Nardzewski (1958), but in fact Hilbert and Bernays alsodefine in section G of Supplement IV a systemL which exchangesthe free and bound function variables for free and bound formulavariables.

Having set up their formal systemH of higher-order arithmetic,Hilbert and Bernays proceed to formalize a substantial fragment ofreal analysis within it, including showing that a version of the leastupper bound principle holds. They comment explicitly (Hilbert &Bernays 1970: 482) that the possibility of representing sequences ofreal numbers by individual number-theoretic functions, as is now donein reverse mathematics by individual sets of natural numbers (see§3.3 for details), depends on being able to define an invertible mappingfrom (countable) sequences of number-theoretic functions onto theindividual number-theoretic functions, which itself arises from theinvertible mapping from pairs of natural numbers to individualnumbers. The existence and use of such representations can beunderstood as a continuation of the tradition of arithmetizationdeveloped in the nineteenth century, albeit now within aprecisely-delimited formal system rather than within informalmathematics.

Arithmetization can thus be understood as an essential component ofthe development of reverse mathematics, since it shows how to reducecomplex mathematical notions such as real numbers, continuousfunctions, measures and so on to more basic ones, namely the notion ofnatural number and the notion of collection or set. This reductivespirit retains its importance throughout the history of reversemathematics, although it manifests itself in a number of differentways. One is throughHilbert’s program of reducing infinitary to finitary mathematics, and its continuationthrough thereductive program in proof theory. Another is the omnipresent use of coding torepresent a wide variety of mathematical objects within the seeminglyaustere ontology of second-order arithmetic (see particularly§3.2–§3.3 for an introduction to the essentials of coding in reversemathematics).

For readers with an interest in tracing the development ofsecond-order arithmetic in more detail, from the work of Hilbert andBernays on, the work of Dean & Walsh (2017) is an importantstarting point. Sieg & Ravaglia (2005) review the contents of thetwo volumes of the first edition of theGrundlagen derMathematik, albeit without much discussion of Supplement IV.Hilbert’s lectures on the foundations of arithmetic and logic(Ewald & Sieg 2013) also provide much more detail on thedevelopment of the ideas that ultimately appeared in theGrundlagen. Sieg (1984, 2020) provides detailed accounts ofsome of the conceptual advances related in this section, and theirphilosophical ramifications. Additional references can be found in thebibliography of the entry onHilbert’s program.

1.3 From recursive counterexamples to reverse mathematics

Although it has deep roots in the work of the Hilbert school (§1.2), reverse mathematics is perhaps best understood methodologically (aswell as historically) as an outgrowth of computability theory, and ofdefinability theory more generally. In particular, the method ofreversals can be seen as originating in the tradition ofrecursivecounterexamples to classical theorems. These are computableobjects which witness the failure of classical mathematical theoremswhen their quantifiers are restricted to computable (recursive)objects. A characteristic example of a recursive counterexample is aSpecker sequence: a computable, bounded increasing sequenceof real numbers with no computable limit. Specker sequences arerecursive counterexamples to theorems like the monotone convergencetheorem and the Bolzano–Weierstraß theorem.

Specker (1949) refrained from drawing explicit philosophicalconclusions from his results, but it seems clear that he understoodthem as applying not only to computable analysis, but also toconstructive mathematics. This was a common attitude amongst logiciansof the time: because the formal notion of a recursive function allowsus to gives a precise mathematical characterization of the informalnotions of algorithm and effective procedure, it was natural topostulate that it could also allow us to understand the informalnotion of a mathematical construction. The use of computability theoryto study constructive mathematics was pioneered by Kleene with hisrealizability interpretation for intuitionistic logic (Kleene 1945). Kleene’s work onrealizability and on Brouwer’s fan theorem (Kleene 1952) led tohis construction of theKleene tree, a computable tree withno computable path, which was important for the discovery of thecomputability-theoretic properties of weak König’s lemma.An independent but equally important development was that of recursiveconstructive mathematics within Markov’s school in Russia, whichalso sought to understand the concept of a construction in terms ofthe concept of recursive function (Nagorny 1994; Kushner 2006;Moschovakis to appear).

Many constructivists either accept a form ofChurch’s thesis—the claim that every constructive process is extensionally equivalent, interms of its outputs, to a computable function—or accept asystem which is consistent with it. Theorems like the monotoneconvergence theorem are not compatible with this approach, because asSpecker discovered, there are computable (and thus constructive)bounded sequences of rational numbers with no computable limit.Therefore, the limit of a Specker sequence does not exist for theconstructivist, not only because it implies the falsity of theconstructive Church’s thesis, but also because it implies aprinciple known as thelimited principle of omniscience (orLPO), a weakening of the law of the excluded middle whichconstructivists typically also deny (Mandelkern 1988, 1989).

The discovery that classical mathematical theorems like the monotoneconvergence theorem or König’s lemma implied the existenceof non-computable sets was a major step towards reverse mathematics.This was because such results typically give more information thanmerely the existence of a non-computable set: they show the existenceof non-computable sets of a particular complexity, lying at a certainpoint in thearithmetical or analytical hierarchies. For example, Specker’s proof shows that the existence of limitsof bounded sequences of rational numbers implies the existence of thesetK of codes for Turing machines which halt on every input.This is the idea underlying the reversal from the monotone convergencetheorem to arithmetical comprehension.

The 1950s saw further interest in the use of tools from computabilitytheory (then known as recursive function theory) and definabilitytheory more generally in studying the foundational programs fromearlier in the century such as intuitionism, finitism, andpredicativism. All of them were viewed as involving a greater orlesser degree of constructivism, and this naturally led to an attemptto analyse them in terms of definable classes of sets or functions ofnatural numbers and real numbers. The most basic was theidentification of the class of computable real numbers as a model forconstructive mathematics (Mostowski 1959). The arithmetical sets werealso studied, by Grzegorczyk (1955), Kondô (1958), and Mostowski(1959), as providing a natural model for the predicativism of Weyl(1918) (§5.4). Following Bernays (1935), more platonistic theories were associatedwith more encompassing notions of computability or definability (Dean& Walsh 2017: 2.2–2.3). Perhaps the culmination of thismovement was Kreisel’s tentative proposal in 1960 to identifythe predicatively definable sets with the class of hyperarithmeticalsets (§5.5), and his associated work on the Cantor–Bendixson theorem, whichhe showed was false when its quantifiers were restricted to thehyperarithmetical sets (Kreisel 1959). Kreisel’s result can beunderstood as a recursive counterexample, and indeed ahyperarithmetical counterexample, to the Cantor–Bendixsontheorem. Internalising the result led to the proof of the equivalencebetween the Cantor–Bendixson theorem and the axiom scheme of\(\Pi^1_1\) comprehension (§4.4).

The work of Errett Bishop in the 1960s also exerted an influence onreverse mathematics. The revival of interest in constructivismfollowing the 1967 publication of Bishop’sFoundations ofConstructive Analysis and his forceful advocacy for aconstructive approach to mathematics led to new work on the limits ofconstructive mathematics. Many of the recursive counterexamples toclassical theorems discovered in the 1970s and 1980s were latertransformed into proofs of reversals from those theorems tonon-constructive set existence principles. For example, Brown andSimpson’s (1986) reversal of the Hahn–Banach theorem forseparable Banach spaces to weak König’s lemma (§4.1) is based on a recursive counterexample to the Hahn–Banachtheorem due to Metakides, Nerode, & Shore (1985), who were in turninspired by a Brouwerian counterexample to the Hahn–Banachtheorem constructed by Bishop himself.

1.4 The early development of reverse mathematics

Despite its many antecedents, reverse mathematics as a distinctivediscipline, with a specific formal setting and methodology, did notemerge until the mid-1970s. Its emergence can be traced quiteprecisely, to Harvey Friedman’s talk at the 1974 InternationalCongress of Mathematicians in Vancouver. Entitled “Some Systemsof Second Order Arithmetic and Their Use”, and published in theProceedings of the ICM (Friedman 1975), Friedman’s paperpresents a vision of reverse mathematics that is strikingly close tothe mature program described in the main sections of this entry. Theformal setting is that of second-order arithmetic and its subsystems,and the Big Five subsystems (\(\sfRCA_0\), \(\WKL_0\), \(\ACA_0\),\(\ATR_0\), and \(\Pi^1_1\text{-}\CA_0\)) and their characteristicaxioms are all present.

Friedman’s ICM paper presented a range of equivalences with themembers of the Big Five, modulo a base theory \(\rmRCA\) that onlyproved the existence of computable sets. Amongst the statementsstudied were formalizations of the fundamental theorems of analysisfrom the final chapter of Dedekind’sStetigkeit undirrationale Zahlen (1872), all of which are provably equivalentto one another and to the axiom scheme of arithmetical comprehension,modulo the base theory \(\rmRCA\). Specker’s proof that thereexist computable bounded sequences of rational numbers whose limitscompute the halting problem was thus transformed into a proof that thesequential completeness and sequential compactness of the real lineare equivalent to the existence of arithmetically definable sets.

On a technical level, the most substantial difference between theformalism of Friedman’s (1975) paper and that used incontemporary reverse mathematical practice is that his base theory\(\rmRCA\) includes the full induction scheme (\ref{eq:ind_scheme}).Friedman subsequently showed in 1976 that the equivalences of his 1975paper could be proved within a weaker base theory called \(\rmRCA_0\),in which the full induction scheme is replaced by quantifier-freeinduction. However, in the process of weakening the inductionprinciple Friedman substantially changed the definition of the basetheory from that used in his earlier paper. The resulting system\(\rmRCA_0\) is essentially a second-order version of primitiverecursive arithmetic. While formally rather different, this doesresult in a system that is proof-theoretically very close to thenow-standard base theory \(\sfRCA_0\) (§3).

The modern form of \(\sfRCA_0\) first appears in print in aninfluential paper by Friedman, Simpson, and Smith (1983), with theaxioms of \(\PA^-\) for \(\bbN\) as an ordered semiring, the recursivecomprehension axiom scheme, and the \(\Sigma^0_1\) induction scheme.By 1983 reverse mathematics was thus substantially as we know ittoday, even down to the use of the slogan “reversemathematics”, which Friedman coined during an AMS specialsession organized by Stephen Simpson (2009: 35).

The major developments that followed in the 1980s and 1990s, which sawreverse mathematics become a major subfield of computability theory,are to a large extent due to the work of Stephen Simpson and hisdoctoral students. They systematically investigated the reversemathematical status of hundreds of theorems spread across manydisparate fields of mathematics, from functional analysis tocombinatorics, commutative algebra to measure theory, order theory togeneral topology. Many of the fruits of this research program aresurveyed in Simpson’s textbook,Subsystems of Second OrderArithmetic, first published in 1999. A second edition waspublished in 2009.

2. Second-Order Arithmetic and Its Subsystems

2.1 The language of second-order arithmetic

The language of second-order arithmetic \(\calL_2\) is a two-sortedlanguage which augments the language of first-order arithmetic,familiar from systems such as Peano arithmetic, with a second sort ofvariables representing sets of natural numbers. Variables of the firstsort \(x_0, x_1, x_2, \dotsc\) are callednumber variablesand are intended to range over natural numbers, while variables of thesecond sort \(X_0, X_1, X_2, \dotsc\) are calledsetvariables and are intended to range over sets of natural numbers.The nonlogical symbols of second-order arithmetic are: the constantsymbols 0 and 1; the binary function symbols \(+\) and \(\times\); andthe binary relation symbols \(\lt\) and \(\in\). Anumericalterm is either a number variable, 0 or 1, or has the form \(t_1 +t_2\) or \(t_1 \times t_2\) where \(t_1\) and \(t_2\) are numericalterms (the only terms of the second sort are set variables). Anatomic formula has the form \(t_1 = t_2\), \(t_1 \lt t_2\),or \(t_1 \in X\), where \(t_1\) and \(t_2\) are numerical terms and\(X\) is any set variable. Second-order arithmetic can be presentedusing any standard classical proof system for a two-sorted language.The identity relation for sets is defined as coextensionality:

2.2 Semantics for second-order arithmetic

The name “second-order arithmetic” can be confusing.Coming across it for the first time, one might easily think that itsname implies that it usessecond-order logic, which is familiar from other contexts in the philosophy ofmathematics such aslogicism andmathematical structuralism. In the so-called standard semantics for second-order logic (sometimesalso called full semantics), the second-order quantifiers areinterpreted as ranging over the entire powerset of the first-orderdomain. For example, in a model \(\calM\) of second-order Peanoarithmetic \(\PA^2\), i.e., Peano arithmetic formulated insecond-order logic, the range of the second-order quantifiers is\(\powset{|\calM|}\), where \(|\calM|\) is the range of thefirst-order quantifiers. It follows from Dedekind’s categoricitytheorem that the system \(\PA^2\) only has one model up toisomorphism. This means that, at least for second-order semanticentailment \(\models_2\), \(\PA^2\) is semantically complete: forevery \(\varphi \in \calL_2\), either \(\PA^2 \models_2 \varphi\) or\(\PA^2 \models_2 \neg\varphi\).

It is therefore important to note that despite its name, the semanticsused in reverse mathematics for the language \(\calL_2\) ofsecond-order arithmetic is not the standard second-order semantics,but the general or Henkin semantics—in other words, those offirst-order logic. An\(\calL_2\)-structure is an orderedtuple of the form

where \(M\) is the domain over which number variables range,\(\calS^\calM\) is a set of subsets of \(M\) over which set variablesrange, \(0^\calM\) and \(1^\calM\) are distinguished elements of\(M\), \(+^\calM\) and \(\times^\calM\) are binary operations on\(M\), and \(\lt^\calM\) is a binary relation on \(M\). The domains\(M\) and \(\calS^\calM\) are always assumed to be disjoint andnonempty.

Since the range of the second-order quantifiers can be any nonemptyset \(\calS^\calM \subseteq \powset{|\calM|}\), there are manynon-isomorphic \(\calL_2\)-structures. Adding axioms does not changethis situation: both the formal system of second-order arithmetic\(\sfZ_2\) (introduced in§2.3) and its subsystems have many non-isomorphic models. Departing fromthe standard semantics of second-order logic is in fact an essentialpart of reverse mathematics, since in order to prove that a principle\(T_0\) does not imply another principle \(T_1\), one must prove thatthere is a model \(\calM\) such that \(\calM \models T_0\) and \(\calM\not\models T_1\). If every subsystem we considered had the sameunique model, this would be impossible.

A basic example is provided by the \(\calL_2\)-structure

where \(\REC= \set{ X : X \text{ is computable}}\). Here \(\omega\) isthe standard natural numbers \(0,1,2,\dotsc\), and the symbols\(0,1,+,\cdot,\lt\) have their standard interpretations. \(\calR\) isthus what is known as an\(\omega\)-model, one whosefirst-order part is the standard natural numbers.\(\omega\)-models are thus distinguished from one another entirely bytheirsecond-order parts. In the case of \(\calR\), itssecond-order part consists of \(\REC\), the set of all computable setsof natural numbers. Since different \(\omega\)-models differ from oneanother only in their second-order parts, they are frequently referredto by the names for those parts. The remainder of this essay willconsequently refer to \(\calR\) as \(\REC\), the \(\omega\)-model\(\calA\) whose second-order part consists of the arithmeticallydefinable sets will be referred to as \(\ARITH\), and so on.

Although many classical mathematical principles such as theintermediate value theorem \(\IVT\) are true in \(\REC\), others arenot, such as the least upper bound axiom \(\LUB\), which is equivalentto arithmetical comprehension (§4.2). From this we can conclude that \(\IVT\) does not entail \(\LUB\).This model also allows us to demonstrate an instance ofincompleteness. The base theory \(\sfRCA_0\) which we will introducein§3 is true in \(\REC\), and since \(\REC\not\models \LUB\), it followsby the soundness theorem for first-order logic that \(\sfRCA_0\not\vdash \LUB\). In this sense, reverse mathematics is a study ofincompleteness: it studies a hierarchy of theorems which areequivalent to certain set existence principles, but which are notproved either by the base theory or by strictly weaker principles inthe hierarchy (Simpson 2010; Eastaugh 2019).

2.3 Axioms of second-order arithmetic

Theformal system of second-order arithmetic, or \(\sfZ_2\),has as axioms the universal closures of the following formulas of\(\calL_2\).

1. \(\PA^-\), the axioms for a discrete ordered semi-ring:
   • \(n + 1 \neq 0\)
   • \(m + 1 = n + 1 \rightarrow m = n\)
   • \(m + 0 = m\)
   • \(m + (n + 1) = (m + n) + 1\)
   • \(m \times 0 = 0\)
   • \(m \times (n + 1) = (m \times n) + m\)
   • \(\neg m \lt 0\)
   • \(m \lt n + 1 \leftrightarrow (m \lt n \vee m = n)\)
2. Induction axiom: \[\label{eq:ind_axiom} \tag{\(\sfInd\)} (0 \in X \wedge \forall{n}(n \in X \rightarrow n + 1 \in X)) \rightarrow \forall{n}(n \in X)\]
3. Comprehension scheme: \[\label{eq:full_comp_scheme} \tag{\(\Pi^1_\infty\text{-}\CA\)} \exists{X}\forall{n}(n \in X \leftrightarrow\varphi(n))\]

   where \(\varphi(n)\) is any \(\calL_2\)-formula with \(X\) not free,but which may have other free set and number variables.

By applying the comprehension scheme (\ref{eq:full_comp_scheme}) andthe induction axiom (\ref{eq:ind_axiom}), \(\sfZ_2\) can prove theinduction scheme, which consists of the universal closuresof

where \(\varphi(n)\) is any \(\calL_2\)-formula.

Second-order arithmetic is sometimes referred to as the first-ordertheory of analysis, since the set variables can be interpreted asranging over real numbers. Many older presentations employ afunctional calculus where set variables are replaced by variables\(f^k\) fork-ary functions \(f : \bbN^k \rightarrow \bbN\).Grzegorczyk, Mostowski, and Ryll-Nardzewski (1958) present such asystem, which also includes adefinite description operator \(\iota\) and a form of the comprehension scheme which they call theLeśniewski schemata. In general, results about these variant systems transfersmoothly from one to another with only minor adjustments.

Asubsystem of second-order arithmetic is an axiom system\(T\) where every axiom \(\varphi \in T\) is an \(\calL_2\)-sentenceprovable in \(\sfZ_2\). Of the many subsystems of second-orderarithmetic which have been studied, five are of central importance inreverse mathematics, and are known colloquially as the “BigFive”. The first of these is the system \(\sfRCA_0\), which isthe standard base theory for reverse mathematics. The other members ofthe Big Five (\(\WKL_0\), \(\ACA_0\), \(\ATR_0\), and\(\Pi^1_1\text{-}\CA_0\)) are proper extensions of \(\sfRCA_0\), andare each equivalent over the base theory \(\sfRCA_0\) to a multitudeof ordinary mathematical theorems from analysis, algebra, infinitarycombinatorics, logic, and topology. Each of these systems has greaterproof-theoretic strength than the preceding one, in the sense thatthey prove theorems that are not provable in the preceding system:\(\WKL_0\) proves more theorems than \(\sfRCA_0\), \(\ACA_0\) provesmore than \(\WKL_0\), \(\ATR_0\) proves more than \(\ACA_0\), and\(\Pi^1_1\text{-}\CA_0\) proves more than \(\ATR_0\). Note that thisordering by inclusion is not the same as the consistency strengthordering: while most members of the Big Five prove the consistency ofthe preceding system, this does not hold in the case of \(\sfRCA_0\)and \(\WKL_0\), which are equiconsistent by the conservativity resultsdiscussed in§4.1.

The “0” subscript at the end of these systems’ namesmeans that the principle of induction is restricted. In the case of\(\ACA_0\) and stronger systems like \(\ATR_0\) and\(\Pi^1_1\text{-}\CA_0\), this restriction involves them containingonly the inductionaxiom (\ref{eq:ind_axiom}), not theinductionscheme (\ref{eq:ind_scheme}). They can thereforeonly prove instances of the induction scheme where they can prove thatthe corresponding set exists: for example, \(\ACA_0\) can prove anyinstance of the induction scheme where the formula involved isarithmetical (i.e., it does not contain any set quantifiers), while\(\Pi^1_1\text{-}\CA_0\) can prove any instance of the inductionscheme where the formula involved is \(\Pi^1_1\). In the case ofsystems weaker than \(\ACA_0\) like \(\sfRCA_0\) and \(\WKL_0\), theinduction axiom is too weak for the systems to be able to do muchmathematically. They are therefore augmented by the\(\Sigma^0_1\)induction scheme, which is the restriction of(\ref{eq:ind_scheme}) to \(\Sigma^0_1\) formulas, those of the form\(\exists{x}\theta(x)\) where \(x\) is a number variable, and\(\theta\) contains only bound number quantifiers and no setquantifiers, although it may contain free and bound number and setvariables.

In the next two sections we will take a closer look at the Big Fivesubsystems, including the mathematics that can be done in each of thembut not in a weaker subsystem, as well as some illuminating details oftheir model-theoretic and proof-theoretic properties. The closeconnections between reverse mathematics and computability theory meanthat it will sometimes be useful to refer to relevant sections of theentry onrecursive functions.

3. The Base Theory

3.1 Recursive comprehension

The subsystems of second-order arithmetic used in reverse mathematicsare typically defined by replacing the comprehension scheme(\ref{eq:full_comp_scheme}) with a weaker axiom. The most fundamentalof these subsystems is called \(\sfRCA_0\), where RCA stands for“recursive comprehension axiom” and the 0 subscriptindicates that its induction principle is restricted. The axioms of\(\sfRCA_0\) consist of the basic axioms; the recursive (or\(\Delta^0_1\)) comprehension scheme consisting of the universalclosures of all formulas of the form

where \(\varphi(n)\) is a \(\Sigma^0_1\)-formula and \(\psi(n)\) is a\(\Pi^0_1\)-formula, both of which may have additional free number andset variables; and the \(\Sigma^0_1\)-induction scheme, which is therestriction of the induction scheme (\ref{eq:ind_scheme}) to\(\Sigma^0_1\)-formulas. The name “recursivecomprehension” refers to the fact that the\(\Delta^0_1\)-definable subsets of \(\omega\) are exactly those whicharerecursive (in contemporary terminology,computable), or to use anotherextensionally equivalent characterization,Turing computable(this isPost’s theorem). \(\sfRCA_0\) is the base theory for most of reverse mathematics:given a theorem \(\tau\) which is provable in some subsystem ofsecond-order arithmeticS that extends \(\sfRCA_0\), we obtaina reversal from \(\tau\) toS when we show that the axioms ofS are provable from the axioms of \(\sfRCA_0 + \tau\).

The presence of \(\Sigma^0_1\) induction in the system allows one toderive many of the familiar algebraic properties of natural numbers:the associativity and commutativity of addition and multiplication,that 0 and 1 are the identity elements for addition and multiplicationrespectively, and the distributivity of multiplication over addition.These results can be summarized by saying that \(\sfRCA_0\) provesthat the system \((\bbN, +, \cdot, 0, 1, \lt)\) is a commutativeordered semiring with cancellation; full details can be found in lemmaII.2.1 of Simpson (2009: 65–66).

3.2 Pairing, sequences, and the basics of coding

All coding, however complex and multi-layered, is ultimately built onthe techniques that allow one to code an ordered pair \(\str{a, b}\)or a finite sequence \(\str{a_1, a_2, \dotsc, a_k}\) of naturalnumbers by a single natural number \(n\) in such a way that thecomponents \(a\) and \(b\) or elements \(a_1, \dotsc, a_k\) can berecovered from the code \(n\) in an effective manner. One simplecoding scheme defines the number \((a,b)\) coding the ordered pair ofnumbers \(\str{a,b}\) as the number \((a + b)^2 + a\), where \(m^2\)abbreviates \(m \times m\). Within \(\sfRCA_0\) we can verify that forany \(a,b,a',b' \in \bbN\), if \((a,b) = (a',b')\) then \(a = a'\) and\(b = b'\). With this pairing function in hand we can define binaryrelations and single argument functions on \(\bbN\): a binary relationis just a set \(X \subseteq \bbN\) such that for all \(n \in X\),there exist \(a, b \leq n\) such that \(n = (a,b)\), while a singleargument function \(f : \bbN\rightarrow \bbN\) is a binary relation on\(\bbN\) such that for all pairs \((a,b)\) and \((c,d) \in f\), if \(a= c\) then \(b = d\).

Coding sequences of arbitrary length requires a little moreartfulness, but can be accomplished by extending the idea used aboveto code pairs of numbers. This method uses Sunzi’s theorem tocode finite sequences of numbers by single natural numbers in such away that any finite sequence can be recovered from its numerical codein a computable fashion. The function \(\beta : \bbN\times \bbN\to\bbN\) that produces, for any code for a finite sequence together withan index, the value of the sequence at that index, is known asGödel’s \(\beta\) function. The set of all finitesequences of natural numbers is known as \(\Seq\), and can be provedto exist by recursive comprehension. The set of all \(s \in \Seq\)such that \(\lh{s} = k\) is denoted by \(\bbN^k\).

Once we have a coding scheme for finite sequences, we can represent\(n\)-ary relations and functions within \(\sfRCA_0\) for arbitrary\(n \in \bbN\). It also allows us to code finite sequences of\(n\)-ary functions \(\str{f_1, \dotsc, f_k}\) by a single function\(f : \bbN^n \to \bbN^k\), with \(f_i(x) = (f(x))(i)\). By combiningrecursive comprehension and \(\Sigma^0_1\) induction with the codingof finite sequences, the theory ofprimitive recursive functions can be developed within \(\sfRCA_0\). Finally, note that a countablesequence of sets \(\str{X_n : n \in \bbN}\) can be coded by a singleset \(X\) by letting

Since functions, relations, real numbers and so on are coded by sets,this technique also allows one to code countable sequences of suchobjects as single sets.

3.3 Integer, rational, and real numbers

The ability to code pairs of numbers by single numbers is all that isneeded in order to code integers and rational numbers by naturalnumbers. Integers are represented by pairs \((a,b) \in \bbN\times\bbN\) where the intended interpretation of the pair \((a,b)\) is as\(a - b\). We begin by defining the following operations of addition,subtraction, and multiplication on \(\bbN\times \bbN,\) together withthe relations of less-than and equality.

It is also useful to define the absolute value operation\(|n|_\bbZ\),

If we take these operations alone as defining the integers, theninfinitely many different pairs will define the same integers. Forexample, the integer \(-17\) is represented by the pairs \((0,17)\),\((17,34)\), \((124,141)\), and so on. We therefore define thesetof integers \(\bbZ\) as consisting of the \(\lt_\bbN\)-leastmembers of the equivalence class induced by the relation \(=_\bbZ\).\(\sfRCA_0\) is able to prove the existence of \(\bbZ\), and provethat the system \((\bbZ, +_\bbZ, \cdot_\bbZ, \lt_\bbZ, =_\bbZ, 0_\bbZ,1_\bbZ)\) is an ordered commutative ring.

Rational numbers are defined in a similar way, as pairs of (codes of)integers (and thus as pairs of pairs of natural numbers). We firstdefine the set of positive integers \(\bbZ^+ = \set{(m,n) : (m,n) \in\bbZ\wedge n \lt m}\). The operations of addition, subtraction, andmultiplication of rational numbers, together with the less-than andequality relations, can then be defined as follows:

For the sake of readability, we suppress the subscript“\(\bbZ\)” on the operations and relations on theright-hand-sides of the definitions. As with the integers, the set\(\bbQ\) ofrational numbers consists of the elements of\(\bbZ\times \bbZ^+\) which are the \(\lt_\bbN\)-least members oftheir equivalence class under the equivalence relation \(=_\bbQ\).\(\sfRCA_0\) can prove the existence of \(\bbQ\) as a set, and showthat the system \((\bbQ, +_\bbQ, \cdot_\bbQ, \lt_\bbQ, =_\bbQ, 0_\bbQ,1_\bbQ)\) is an ordered field.

One way to understand the coding schemes for integer and rationalnumbers just described is as defining bijective functions betweenthose number systems and subsets of the natural numbers. As Cantorshowed, there can be no such bijection between the irrational numbersand the natural numbers. In order to code irrational numbers, andhence the real numbers in general, it is therefore necessary to usesets of natural numbers. The following approach, using fast-convergingCauchy sequences, is the standard way to do this in reversemathematics. Asequence of rational numbers is a function \(f: \bbN\rightarrow \bbQ\), which we will typically denote by \(\str{x_k: k \in \bbN}\) with \(x_k = f(k)\). Areal number is asequence of rational numbers \(x\) obeying the following convergencecondition: for all \(n,m \in \bbN\), \(|x_n - x_{n+m}| \leq 2^{-n}\),where \({|(a,b)|}_\bbQ= (|a|, b)\) is the absolute value operation.Two reals \(x\) and \(y\) are said to beequal, \(x =_\bbRy\), if \(|x_n - y_n| \leq 2^{-n+1}\) for all \(n\). Note that\(=_\bbR\) is an equivalence relation on sets of natural numbers, notthe identity relation (\ref{eq:extensionality}) on sets. We cannotselect particular sets from the equivalence classes to represent realnumbers because the base theory is too weak, and the language itselfdoes not allow us to quantify over the equivalence classes themselves.Moreover, while reverse mathematicians often write things like“\(x \in \bbR\)”, strictly speaking this is an abuse ofnotation, because the set \(\bbR\) of all real numbers is athird-order object which is not directly represented in second-orderarithmetic. Expressions like “\(x \in \bbR\)” should beinterpreted as a convenient shorthand for “\(x\) is a realnumber”, where the property of being a real number is thatdescribed above, i.e., the arithmetically-definable property of codinga fast-converging Cauchy sequence of rational numbers.

The rational numbers can be embedded into the reals by representingthe rational number \(q\) with the constant sequence \(r_q = \str{q_n: n \in \bbN}\), where \(q_n = q\) for all \(n \in \bbN\). Addition,subtraction, and multiplication of (codes for) real numbers can bedone in terms of addition, subtraction, and multiplication ofrationals. Given real numbers \(x = \str{x_n : n \in \bbN}\) and \(y =\str{y_n : n \in \bbN}\),

for the least \(k\) such that \(|x_0| + |y_0| + 2 \leq 2^k\). Finally,we define the ordering \(\leq_\bbR\) by saying that \(x \leq_\bbR y\)if and only if for all \(k \in \bbN\), \(x_k \leq y_k + 2^{-k+1}\);\(x \lt_\bbR y\) if \(x \leq_\bbR y\) and \(x \neq_\bbR y\). Asbefore, to aid readability we suppress the “\(\bbQ\)”subscripts on the operations and relations in the definitions above,since it is clear from context when addition, subtraction,multiplication etc. are operations on rational numbers rather thanintegers or natural numbers. \(\sfRCA_0\) suffices to show that thesystem \((\bbR, +_\bbR, \cdot_\bbR, 0_\bbR, 1_\bbR, \lt_\bbR,=_\bbR)\) thus defined satisfies the axioms of an Archimedean orderedfield, although given the cardinality restrictions, the system itselfis not an object of the theory.

Countable sequences of real numbers can also be coded as sets ofnatural numbers. This is a very powerful device that allows theformalization of statements from real analysis like theHeine–Borel and Bolzano–Weierstraß theorems. Asequence of real numbers is a function \(f : \bbN\times\bbN\to \bbQ\) such that for each \(n \in \bbN\), the function \((f)_n: \bbN\to \bbQ\), where \((f)_n(k) = f(k,n)\), is a real number. Aswith sequences of rational numbers, we will often talk about sequencesof real numbers using notation like \(\str{x_n : n \in \bbN}\), where\(x_n = (f)_n\). A sequence of reals \(\str{x_n : n \in \bbN}\) issaid toconverge to a limit \(x\), \(x = \lim_n x_n\), if forall \(\varepsilon \gt 0\) there exists an \(n\) such that for all\(i\), \(|x - x_{n+i}| \lt \varepsilon\). Sequences where the limit\(\lim_n x_n\) exists are described asconvergent.

These notions can be used to formulate sequential versions of standardtheorems from analysis. For example, thesequential least upperbound axiom states that every bounded sequence of real numbershas a least upper bound. This principle is not provable in\(\sfRCA_0\), and in fact is equivalent to \(\ACA_0\). However, aweaker principle called nested interval completeness is provable in\(\sfRCA_0\), and can be used to prove a number of fundamental resultsincluding the intermediate value theorem, a version of Cantor’stheorem that the real numbers are uncountable, and a version of theBaire category theorem (Simpson 2009: 76–77).

3.4 \(\omega\)-models and computability

The recursive comprehension axiom scheme gets its name from the factthat the \(\Delta^0_1\)-definable sets of natural numbers areprecisely therecursive (that is, computable) sets of natural numbers. As such, the set

has a special role, as the second-order part of the \(\omega\)-model\(\calR\) of \(\sfRCA_0\) introduced in§2.2. This is one of a special class of \(\calL_2\)-structures known as\(\omega\)-models in which the first-order domain is alwaysthe standard natural numbers \(\omega\), and the \(+\), \(\times\),and \(\lt\) symbols are interpreted by the standard (computable)operations of addition and multiplication and the standard less-thanrelation. Since the first-order part is fixed, the only part of thesestructures that can vary is the range of the second-order quantifiers.The \(\omega\)-models of differents subsystems of second-orderarithmetic often have interesting computability-theoretic propertieswhich are bound up with the set existence axioms that differentiatethem. Since their first-order part is standard, all \(\omega\)-modelssatisfy the full induction scheme (\ref{eq:ind_scheme}).

The \(\omega\)-models of \(\sfRCA_0\) are exactly theTuringideals: subsets of \(\powset{\omega}\) which are closed underrecursive joins andrelative Turing computability. The smallest Turing ideal is \(\REC\), and as such, \(\REC\) is alsothe minimum \(\omega\)-model of \(\sfRCA_0\). We can think of \(\REC\)as, in some sense, the intended model of \(\sfRCA_0\): the axioms of\(\sfRCA_0\) only assert the existence of computable sets (or moreprecisely, the existence of sets which are computable in someparameter), and in \(\REC\) all sets are computable. The existence ofa minimum \(\omega\)-model of the system is a property that\(\sfRCA_0\) shares with other subsystems of second-order arithmeticwhose characteristic axioms are comprehension schemes. The minimum\(\omega\)-model of \(\ACA_0\) is the class \(\ARITH\) ofarithmetically definable sets, while the minimum \(\omega\)-model of\(\Delta^1_1\text{-}\CA_0\) is the class \(\HYP\) of hyperarithmeticalsets. \(\Pi^1_1\text{-}\CA_0\) does not have a minimum\(\omega\)-model, but it does have a minimum \(\beta\)-model, where\(\beta\)-models are \(\omega\)-models that satisfy the additionalcondition of satisfying all true \(\Sigma^1_1\) sentences, not justall true arithmetical sentences as \(\omega\)-models do.

If a statement \(\varphi\) in the language of second-order arithmeticholds in the \(\omega\)-model whose second-order part is \(\REC\),then we say that \(\varphi\) iscomputably true, since it isvalid when its set quantifiers are restricted so that they only rangeover computable sets (and thus over computable codes for othermathematical objects which we might think of as being computable).Since all of the axioms of \(\sfRCA_0\) are true in \(\REC\),\(\sfRCA_0\) is computably true, and can be thought of as a naturalaxiomatic system in which to formalize computable analysis, orcomputable mathematics more generally. In this respect \(\sfRCA_0\) issubstantially different from most other subsystems of second-orderarithmetic which are studied in reverse mathematics. Thecharacteristic axioms of systems like \(\WKL_0\), \(\ACA_0\),\(\ATR_0\) and \(\Pi^1_1\text{-}\CA_0\) can be understood incomputability-theoretic terms as asserting the existence of certainclasses of non-computable sets, and their \(\omega\)-models aretherefore guaranteed to contain non-computable sets of differentdegrees of complexity, measured in terms of hierarchies such as thearithmetical or analytical hierarchies, or in terms of theTuring degrees. In this sense reverse mathematics can be thought of as measuring thedegree of non-constructivity of classical mathematical theorems.

4. The Big Five

4.1 Weak König’s lemma

When we leave the base theory \(\sfRCA_0\) and climb up the reversemathematical hierarchy, the first major milestone we reach is thesystem \(\WKL_0\). This system is obtained by adding to the axioms of\(\sfRCA_0\) the nonconstructive set existence axiomweakKönig’s lemma, or WKL. The König infinity lemma,due to Dénes König (1927), states that every finitelybranching infinite tree has an infinite path through it. WKL isobtained by restricting König’s infinity lemma to countabletrees of binary sequences. To state it in more precise terms, we firstneed to give a more formal presentation of trees.

Let \(X \subseteq \bbN\) be a set of natural numbers. We denote theset of all finite sequences of elements of \(X\) by \(X^{\lt\bbN}\).Two important special cases are when \(X = 2 = \set{0,1}\), and\(2^{\lt\bbN}\) is thus the set of all finite binary sequences, andwhen \(X = \bbN\), and \(\bbN^{\lt\bbN} = \Seq\), the set of allfinite sequences of natural numbers. Atree \(T\) on \(X\) isa set of finite sequences of elements of \(X\) which is closed underpredecessors, so if \(\tau \in T \subseteq X^{\lt\bbN}\), then\(\tau\restr{n} \in T\) for every \(n \lt \lh{\tau}\). A tree \(T\) on\(X\) isfinitely branching if for every \(\tau \in T\),there are only finitely many \(x \in X\) such that \(\tau \concat\str{x} \in T\). Apath through \(T\) is a function \(f :\bbN\rightarrow X\) such that for all \(n \in \bbN\), the initialsequence \(f\restr{n} = \str{f(0), f(1), \dotsc, f(n - 1)} \in T\). Atree \(T\) isinfinite if it has infinitely many nodes, i.e.,for all \(n \in \bbN\) there exists \(\tau \in T\) such that \(\tau\gt n\) (where \(\tau\) is considered simply as a number, rather thanas a sequence). Weak König’s lemma (WKL) is the principlethat for every tree \(T \subseteq 2^{\lt\bbN}\), if \(T\) is infinitethen it has a path. \(\WKL_0\) is the system obtained by adding WKL tothe axioms of \(\sfRCA_0\).

Weak König’s lemma is equivalent over \(\sfRCA_0\) to avery large number of theorems, particularly in real and functionalanalysis, but also in logic and algebra. It is perhaps best understoodas a compactness principle, which can be seen by looking at weakKönig’s lemma itself, but also at the theorems it isequivalent to, such as the Heine–Borel covering theorem and thecompactness theorem for first-order logic. Other notable theorems thatare equivalent to WKL include Gödel’s completeness theoremfor first-order logic; the separable Hahn–Banach theorem;Brouwer’s fixed point theorem; the theorem that every countablecommutative ring has a prime ideal; and Peano’s existencetheorem for ordinary differential equations.

Perhaps surprisingly, adding weak König’s lemma to\(\sfRCA_0\) does not result in any increase in first-order strength.To explain this fact, we first need to introduce the notion ofconservativity. Informally, this is the idea that while atheory \(S\) may have more expressive resources than a theory \(T\)does (for example, \(S\) may have a more extensive vocabulary), in thepart of the language that the two theories have in common, \(S\) saysno more than \(T\) does. Formally, let \(S\) and \(T\) be theories inlanguages \(\calL_S\) and \(\calL_T\) respectively, and let \(\Gamma\)be a set of sentences in the language \(\calL_S \cap \calL_T\). \(S\)is\(\Gamma\)-conservative over \(T\) if for every \(\varphi\in \Gamma\), \(S \vdash \varphi\) iff \(T \vdash \varphi\). Where thelanguage of \(S\) is an extension of the language of \(T\), \(\calL_T\subseteq \calL_S\), we simply say that \(S\) isconservativeover \(T\). A common case is when \(S\) is a subsystem of second-orderarithmetic and \(T\) is a system of first-order arithmetic. In suchcases, if \(S\) is conservative over \(T\) then we say that thefirst-order part of \(S\) is \(T\).

Three key conservativity theorems connect \(\sfRCA_0\) and \(\WKL_0\),and explain their first-order strength. The first is that\(\rmI\Sigma_1\) is \(\Pi^0_2\)-conservative over \(\PRA\), where\(\rmI\Sigma_1\) is a subsystem of first-order Peano arithmetic\(\PA\) obtained by restricting the induction scheme to \(\Sigma_1\)formulas, and \(\PRA\) is the system of primitive recursive arithmeticdeveloped by Skolem (1923) and axiomatized by Hilbert & Bernays(1934). This result was proved by Parsons (1970) and is hence known asParsons’s theorem (Joosten 2002 [Other Internet Reseources]; Ferreira 2005). The second is that \(\rmI\Sigma_1\) is thefirst-order part of \(\sfRCA_0\). This is due to Friedman (1976);proofs can be found in Simpson (2009: IX.1) and Hirschfeldt (2014:129). The third is that \(\WKL_0\) is \(\Pi^1_1\)-conservative over\(\sfRCA_0\). This is an unpublished theorem of Harrington. Its proofwas made generally available by Simpson (2009: IX.2), and a somewhatmore detailed version can be found in Hirschfeldt (2014: 7.2).

Combining the first two results, we have that \(\sfRCA_0\) is\(\Pi^0_2\)-conservative over \(\PRA\). This has importantramifications for our understanding of finitism in the sense ofHilbert and Bernays, and the relationship of that program to theformal system \(\sfRCA_0\) (§5.2). With the addition of Harrington’s theorem we can see that thatthe first-order part of \(\WKL_0\) is \(\rmI\Sigma_1\), and that\(\WKL_0\) is \(\Pi^0_2\)-conservative over \(\PRA\). Sinceconsistency statements are \(\Pi^0_1\) sentences, it follows that \(\WKL_0\) isequiconsistent with \(\sfRCA_0\), \(\rmI\Sigma_1\), and \(\PRA\),since one can prove in \(\PRA\) that the consistency of any of thesetheories implies the consistency of the others. By the same token,\(\WKL_0\) has the sameproof-theoretic ordinal as \(\sfRCA_0\), \(\rmI\Sigma_1\), and \(\PRA\), namely\(\omega^\omega\).

Harrington’s proof is model-theoretic in character: it uses aforcing argument to show that every countable model of \(\sfRCA_0\)can be expanded to a countable model of \(\WKL_0\) while preservingthe truth values of \(\Pi^1_1\) formulas. Sieg (1985) subsequentlygave the theorem a more constructive treatment by constructing aprimitive recursive function \(f\) which transforms any proof \(p\) in\(\WKL_0\) of a a \(\Pi^0_2\) statement \(\varphi\) into a proof\(f(p)\) of \(\varphi\) in \(\PRA\). Although somewhat technical,these conservativity results inspired a debate in the foundations ofmathematics concerning the limits of the mathematics that could berecovered in a formal system which was finitist in the sense ofHilbert’s program (§5.3).

4.2 Arithmetical comprehension

The third member of the Big Five is \(\ACA_0\), where ACA stands for“arithmetical comprehension axiom”. A formula \(\varphi\)in the language of second-order arithmetic isarithmetical ifit contains no set quantifiers, although it may contain free setvariables. Thearithmetical comprehension scheme consists ofthe universal closures of all formulas of the form

where \(\varphi\) is arithmetical with \(X\) not free, although\(\varphi\) may contain other free set and number variables.\(\ACA_0\) is the system obtained by adding the arithmeticalcomprehension scheme to the axioms of \(\sfRCA_0\). \(\ACA_0\) provesthearithmetical induction scheme, that is, the restrictionof the induction scheme (\ref{eq:ind_scheme}) to arithmeticalformulas. This means that \(\ACA_0\) proves all of the axioms offirst-order Peano arithmetic \(\PA\). Via a conservativity result dueto Friedman (1976), a kind of converse of this result also holds:every sentence in the language of first-order arithmetic which isprovable in \(\ACA_0\) is also provable in \(\PA\). It follows fromthis result thatGentzen’s consistency proof for \(\PA\) also applies to \(\ACA_0\), and that \(\ACA_0\) has thesame proof-theoretic ordinal as \(\PA\), namely \(\varepsilon_0\).

\(\ACA_0\) is strictly stronger than both \(\sfRCA_0\) and \(\WKL_0\).Where the former is concerned, this can be easily seen from the factthat arithmetical comprehension is computably false, since it provesthat the halting problem \(K\) and many other non-computable setsexist, so the \(\omega\)-model \(\REC\) provides a counterexample: amodel in which \(\sfRCA_0\) is true but arithmetical comprehension isfalse. Proving that \(\WKL_0\) is strictly weaker than \(\ACA_0\)requires a more subtle computability-theoretic argument, using the lowbasis theorem of Jockusch & Soare (1972) to prove the existence ofa model of \(\WKL_0\) which does not contain \(K\), and therefore doesnot satisfy arithmetical comprehension.

Although many important analytical theorems can be proved in\(\WKL_0\), some fundamental results about the nature of the realnumbers can only be proved with the use of arithmetical comprehension.Many of these results concern the sequential completeness andcompactness of the real line, and assert the existence of limits ofvarious kinds of sequences. The most basic of these is a sequentialform of the least upper bound axiom, which states that every boundedsequence of real numbers has a least upper bound. Others are theBolzano–Weierstraß theorem, which states that everybounded sequence of real numbers contains a subsequence whichconverges to a limit; the monotone convergence theorem, which statesthat every monotone sequence of real numbers converges to a limit; andthe Cauchy convergence theorem, which states that every Cauchysequence of real numbers converges to a limit. All of these theoremsare provable in \(\ACA_0\), and when added to the base theory\(\sfRCA_0\), each of them imply arithmetical comprehension. Thiscollection of equivalences, due to Friedman (1975), can be seen of asa formalization of the informal equivalences proved in the lastchapter of Dedekind (1872), but for the sequential notion ofcompleteness of the real number line, rather than Dedekind’snotion of completeness for arbitrary bounded sets of real numbers.

Although these statements are only concerned with the real number line\(\bbR\), they can easily be extended to the Euclidean plane\(\bbR^2\), the three-dimensional Euclidean space \(\bbR^3\), or anyfinite-dimensional Euclidean space \(\bbR^n\). The correspondingsequential completeness theorems for those spaces are also provable in\(\ACA_0\), and thus equivalent to it over \(\sfRCA_0\), since theyimply the versions for \(\bbR\). More generally still, it is possibleto represent the notion of a complete separable metric space withinsecond-order arithmetic, and thus state versions of these theoremswhich hold for any such space. These theorems too are provable in\(\ACA_0\), as are stronger generalizations such as the Ascoli lemma.\(\ACA_0\) is also strong enough to prove that, in any completeseparable metric space which is also compact, every sequence of pointshas a convergent subsequence.

Although analysis is rich in theorems equivalent to arithmeticalcomprehension, other areas may be even more so, especially algebra.These theorems concern a wide variety of algebraic structuresincluding countable abelian groups, countable fields (includingordered and formally real fields), countable commutative rings, andcountable vector spaces. Some important examples include the theoremthat every countable field has a strong algebraic closure, and thatevery countable field has a strong real closure; that every countablecommutative ring has a maximal ideal; that every countable abeliangroup has a unique divisible closure; and that every countable vectorspace over a countable field has a basis.

Countable infinitary combinatorics also provides several importantequivalences to arithmetical comprehension. One is König’slemma that every infinite, finitely branching tree contains aninfinite path. This is an interesting case in which the precisestatement of the theorem matters a great deal. The restriction ofKönig’s lemma to trees in which the number of branchingsfrom any given node is bounded (bounded König’s lemma) isstrictly weaker than arithmetical comprehension, and in fact it isequivalent to weak König’s lemma. The unrestricted versionof König’s lemma, on the other hand, is equivalent toarithmetical comprehension.

Another example is Ramsey’s theorem. Given fixed natural numbers\(n \geq 1\) and \(k \geq 1\), the statement \(\RT^n_k\) asserts thatevery for every \(k\)-colouring of \(n\)-tuples of natural numbers,there exists an infinite monochromatic orhomogeneous subsetof those tuples. When \(n \geq 3\) and \(k \geq 2\), \(\RT^n_k\)implies arithmetical comprehension over \(\sfRCA_0\). The statement\(\RT^2_2\), however, holds a special place in reverse mathematics, asit lies outside the Big Five classification: it is not provable in\(\sfRCA_0\) (Specker 1971), not provable in \(\WKL_0\) (Jockusch1972), does not imply arithmetical comprehension (Seetapun &Slaman 1995), and does not imply weak König’s lemma either(Liu 2012). Discussing these results, their implications, and morerecent work on Ramsey’s theorem and the Reverse Mathematics Zoo [Other Internet Resources] which arose from its study would take us too far afield, but thereare now many good introductory references including Hirschfeldt (2014)and Dzhafarov & Mummert (2022: Chapter 8).

4.3 Arithmetical transfinite recursion

Arithmetical comprehension allows us to construct objects by applyingsome arithmetically-definable operation a finite number of times. Anatural generalization of this method of proof is to allow suchiterations to continue all the way to the first infinite ordinal\(\omega\), and off into the transfinite. Constructing mathematicalobjects by transfinite recursion is of course a standard part of settheory, licensed by the axiom scheme of replacement. The axiom schemeofarithmetical transfinite recursion is an arithmeticalanalogue, in which the operator \(\Phi(X)\) which one can apply mustbe arithmetically definable, and in which the well-orderings alongwhich the operator can be iterated must be countable. Despite theserestrictions, arithmetical transfinite recursion is quite powerful.Adding it to \(\sfRCA_0\) produces the system \(\ATR_0\), a muchstronger system than \(\ACA_0\) which can prove not merely theorems ofclassical analysis, but many results in descriptive set theoryconcerning Borel and analytic sets.

In order to define arithmetical transfinite recursion, we must firstunderstand what is meant in this setting by a well-ordering. A binaryrelation \(R \subseteq \bbN\times \bbN\) is said to bereflexive if for all \(x,y \in \bbN\), if \((x,y) \in R\)then \((x,x) \in R\) and \((y,y) \in R\). If \(R\) is a reflexiverelation then we define \(\mathrm{field}(R) = \set{x : (x,x) \in R}\).We also write \(x \leq_R y\) if and only if \((x,y) \in R\), and \(x\lt_R y\) if and only if \((x, y) \in R\) and \((y, x) \not\in R\). Acountable linear ordering is a reflexive relation which isalso transitive (if \(x \leq_R y\) and \(y \leq_R z\), then \(x \leq_Rz\)), antisymmetric (if \(x \leq_R y\) and \(y \leq_R x\), then \(x =y\)), and total (if \(x,y \in \mathrm{field}(R)\), then \(x \leq_R y\)or \(y \leq_R x\)). We write \(\mathrm{LO}(R)\) as an abbreviation forthe formula asserting that \(R\) is a countable linear ordering. If\(R\) is a reflexive relation, \(R\) iswell-founded if itcontains no infinite descending chain: for all \(f : \bbN\to\mathrm{field}(R)\) there exists \(n \in \bbN\) such that \(f(n+1)\not\lt_R f(n)\). We write \(\mathrm{WF}(R)\) as an abbreviation forthe formula asserting that \(R\) is well-founded. Acountablewell-ordering is a countable linear order \(R\) which is alsowell-founded. We write \(\mathrm{WO}(R)\) as an abbreviation for theformula asserting that \(R\) is a countable well-ordering, i.e., that\(\mathrm{LO}(R) \wedge \mathrm{WF}(R)\).

The next step in defining arithmetical transfinite recursion is thenotion of ahierarchy: a system of sets built up from someinitial set by the repeated application of an operator. Given aformula \(\varphi(n,Y)\), let \(\mathrm{H}_\varphi(X,Y)\) be theformula asserting that \(X\) is a countable linear ordering and that\(Y\) is the set of all pairs \((n,j)\) such that \(j \in\mathrm{field}(X)\) and \(\varphi(n, Y^j)\), where

The idea behind this definition is that \(Y\) is the hierarchy of setsthat result from iterating the operator defined by the formula\(\varphi\) along the ordering \(X\), and that \(Y^j\) is the setconstructed at level \(j\) of the iteration. Theaxiom scheme ofarithmetical transfinite recursion consists of the universalclosures of all instances of the scheme

where \(\varphi(n,Y)\) is arithmetical. The system \(\ATR_0\) consistsof the axioms of \(\sfRCA_0\) plus all instances of the axiom schemeof arithmetical transfinite recursion.

Given the nature of the axiom it is unsurprising that theoremsequivalent to ATR all have some explicit or implicit connection tocountable well-orderings. One of the most fundamental, partly due toits role in the proofs of many reversals, is the seemingly innocuousstatement CWO that any two countable well-orderings are comparable:one must always be isomorphic to an initial segment of the other.Ordinals have been bound up with the theory of point-sets (in the mostbasic case, sets of real numbers) since the inception of both in thework of Cantor in the early 1880s (Ferreirós 2007: Chapter VI).Cantor used countable ordinals in his proof of theCantor–Bendixson theorem that every closed set is the union of aperfect set and a countable set. This theorem is actually equivalentto \(\Pi^1_1\) comprehension (§4.4), but other theorems from descriptive set theory only requirearithmetical transfinite recursion. One such result is the perfect settheorem that every closed set contains a perfect subset. Another isLuzin’s separation theorem that any two disjoint analytic setscan be separated by a perfect set. This theorem is standardly used indescriptive set theory to prove Suslin’s theorem that the Borelsets are exactly those analytic sets whose complement is also analytic(Kechris 1995: 14). Suslin’s theorem can therefore also beproved in \(\ATR_0\), although it is not equivalent to it.

4.4 \(\Pi^1_1\) comprehension

The last of the Big Five systems is \(\Pi^1_1\text{-}\CA_0\), whosecharacteristic axiom is the \(\Pi^1_1\) comprehension scheme. Aformula \(\varphi\) in the language of second-order arithmetic is\(\Pi^1_1\) if it has the form \(\forall{X}\theta\), where \(X\) is aset variable and \(\theta\) is an arithmetical formula. A formula\(\varphi\) is \(\Sigma^1_1\) if it has the form \(\exists{X}\theta\),with \(\theta\) arithmetical and \(X\) a set variable. Every\(\Pi^1_1\) formula is equivalent to the negation of a \(\Sigma^1_1\)formula, and every \(\Sigma^1_1\) formula is equivalent to thenegation of a \(\Pi^1_1\) formula. The \(\Pi^1_1\) comprehensionscheme consists of the universal closures of all formulas of theform

where \(\varphi\) is \(\Pi^1_1\) with \(X\) not free, although\(\varphi\) may contain other free set and number variables. Theaxioms of \(\Pi^1_1\text{-}\CA_0\) are the axioms of \(\sfRCA_0\) plusall instances of the \(\Pi^1_1\) comprehension scheme. While one canalso define a corresponding \(\Sigma^1_1\) comprehension scheme, thisturns out to be unnecessary, since every instance of \(\Sigma^1_1\)comprehension is provably equivalent in \(\sfRCA_0\) to an instance of\(\Pi^1_1\) comprehension.

\(\Pi^1_1\) comprehension is needed in order to extend the results onperfect sets provable in \(\ATR_0\) (§4.3). The historically most notable such result is theCantor–Bendixson theorem, which states that every closed set isthe union of a perfect set and a countable set. Kreisel (1959) provedthe existence of computable closed sets of the form \(F = F_p \cupF_c\) such that \(F_p\) is perfect and \(F_c\) is countable, but the(codes of) \(F_p\) and \(F_c\) are \(\Pi^1_1\) but not \(\Delta^1_1\).This shows that \(\Pi^1_1\) comprehension is required in order toprove the Cantor–Bendixson theorem, and in fact theCantor–Bendixson theorem is provably equivalent over \(\ACA_0\)to \(\Pi^1_1\) comprehension (Simpson 2009: theorem VI.1.6, pp.219–220).

Other important results in descriptive set theory equivalent to\(\Pi^1_1\) comprehension include the Kondô–Addisontheorem that every coanalytic relation can be uniformized by acoanalytic function, Silver’s theorem that every coanalyticequivalence relation contains either countably many or\(2^{\aleph_0}\)-many equivalence classes, and the determinacy ofgames with a \(\Sigma^0_1 \wedge \Pi^0_1\) payoff set.\(\Pi^1_1\text{-}\CA\) is also needed for a number of results in grouptheory, involving the order types of countable ordered groups and thestructure theory of countable abelian groups. Solomon (2001) showedthat Mal’tsev’s theorem is equivalent over \(\sfRCA_0\) to\(\Pi^1_1\text{-}\CA\), while Friedman, Simpson, and Smith (1983)showed the same for the statement that every countable abelian groupis the direct sum of a divisible group and a reduced group.

\(\Pi^1_1\text{-}\CA_0\) is the strongest system standardly studied inreverse mathematics, although reversals to stronger systems have beenfound. One such example is the equivalence between \(\Pi^1_2\)comprehension and a statement from general topology concerningcountably based spaces of maximal filters (Mummert & Simpson2005). Other statements, for example determinacy axioms, are evenstronger (Montalbán & Shore 2012). Nevertheless, for mostmathematical statements studied in reverse mathematics, even\(\Pi^1_1\text{-}\CA_0\) is a much stronger system than is required inorder to prove them.

5. Foundational Programs and Reverse Mathematics

5.1 Computable mathematics, constructive mathematics, and \(\sfRCA_0\)

Mathematics in \(\sfRCA_0\) shares much with that in a number ofbroadly constructive approaches to mathematics, most notablyconstructive analysis in the tradition of Bishop, Russian constructivemathematics, and computable analysis (also known in older texts asrecursive analysis). However, there are also important differences,largely centred on the use of thelaw of excluded middle (LEM) which, as a theory formulated in classical logic, \(\sfRCA_0\)satisfies.

At the centre of the connection between the formal system \(\sfRCA_0\)and traditions in constructive mathematics is Church’s thesis.In the context of constructive mathematics, this states that everyconstructive function is extensionally equivalent to a recursivefunction, i.e., there exists a Turing machine which halts on everyinput and produces the same output as the constructive function. UsingKleene’sT predicate andU function we canformalize this as

As noted in§1.3, the interpretation of the notion of a construction in terms ofcomputable functions dates back to the early history of computabilitytheory in the 1940s. Since \ref{eq:CT} can be read as a formalstatement in the language of second-order arithmetic, we can considerits status in relation to classical subsystems of second-orderarithmetic. \ref{eq:CT} is consistent with \(\sfRCA_0\), since theaxioms of \(\sfRCA_0\) are satisfied in the \(\omega\)-model \(\REC\)consisting of all and only the computable sets (§3.4). However, it is inconsistent with stronger systems that imply theexistence of non-computable sets.

Russian constructive mathematics, working in the tradition of Markov,embraced the idea that constructive procedures were algorithmic ones,and thus built a version of Church’s thesis into their approach(Kushner 2006). Bishop’s constructive analysis followed adifferent path: one which rejected the law of excluded middle, butaccepted neither Brouwer’s new basis for analysis in hisCreating Subject arguments, nor the close association withcomputability theory of the Russian constructivists. As Bishop putsit, he develops analysis “with an absolute minimum ofphilosophical prejudice concerning the nature of constructivemathematics” (Bishop 1967: ix), going on to assert that“[t]here are no dogmas to which we must conform”.Bishop’s system is thus consistent with classical mathematics,with intuitionistic mathematics, and with Church’s thesis.

However, the system \(\sfRCA_0\) is not a faithful formalization ofany of these constructivist viewpoints: the classical logic it embedsis an insurmountable barrier. The intermediate value theorem providesa good example of why this is. While the intermediate value theorem isprovable in \(\sfRCA_0\), the proof essentially relies on a casedistinction made via the law of the excluded middle, and is thus notconstructively provable (Bridges & Richman 1987: 5). This limitsour ability to use provability in \(\sfRCA_0\) as a marker ofconstructive provability. Further complications are provided by thefact that in \(\sfRCA_0\), induction is restricted to \(\Sigma^0_1\)predicates, while constructivists tend to accept unrestrictedquantifier complexity in their uses of induction.

In some ways, computable analysis as presented in works like Aberth(1980) and Pour-El & Richards (1989) provides a better match with\(\sfRCA_0\) than constructive analysis, as Simpson (2010) suggests.This does have a foundational upshot of sorts, since as Beeson (1985)remarks,

there is a coherent philosophy of mathematics under which recursivemathematics represents the truth about the mathematical universe. Ifone takes this view, then the subject has a significance beyond themere production of counterexamples. [… ][T]he world underChurch’s thesis is an entertaining place, full of surprises(like any foreign country), but not by any means too chaotic tosupport life.

Thoroughgoing constructivists do not take the natural numbers to forma completed infinite totality, while in computable analysis thestandard machinery of computability theory (which does make thisassumption) is taken as fundamental (Pour-El & Richards 1989:VII). The use of classical logic in \(\sfRCA_0\) is thusunproblematic. Recursive comprehension, its characteristic axiom,seems tailor-made for computable mathematics. It is thus easier to saythat provability in \(\sfRCA_0\) implies truth in computable analysis,although the restriction on the induction principle does mean that asfar as computable mathematics is concerned, \(\sfRCA_0\) is aneedlessly restricted system. Moreover, recursive counterexamples (§1.3)—and thus reversals to set existence principles asserting the existence ofnon-computable sets—have a clear interpretation in the contextof computable mathematics, namely demonstrating that they are false.\(\Pi^1_1\) statements should, however, be excluded from thisanalysis, since any true \(\Pi^1_1\) statement will be true in the\(\omega\)-model \(\REC\), and thus computably true, regardless ofwhether or not it is provable in \(\sfRCA_0\). For further discussionof this point, see (Eastaugh 2019: 157, 171–172).

5.2 Finitism and \(\sfRCA_0\)

The formal system \(\sfRCA_0\) also has connections to anotherimportant foundational program, Hilbertian finitism.Hilbert’s program was to secure the status ofCantorian infinitary mathematics, by proving its consistency using purely finitary means. This reflectsHilbert’s two-tier epistemology in which finitary combinatorialstatements hold a special status, since unlike the abstract elementsof ideal, infinitary mathematics, they concern “extra-logicaldiscrete objects, which exist intuitively as immediate experiencebefore all thought” (Hilbert 1922: 163).

Thereal (finitary, contentual) propositions include, forHilbert, numerical equations, together with the more complexstatements that can be formed from equations via the propositionalconnectives (negation, conjunction, disjunction, implication).Moreover, the universal closures of such statements also have finitarymeaning, because we can think of them as a schema:\(\forall{x}\varphi(x)\), where \(\varphi\) is quantifier-free, meansthat for any given number \(\overline{n}\), we can verify in afinitary way that \(\varphi(\overline{n})\). It is anachronistic buttechnically helpful to refer to this class of statements as the\(\Pi^0_1\) sentences of the language of arithmetic. In contrast tothis,ideal statements do not have finitary meaning: they aremerely symbolic,

formulas that [ …] in themselves mean nothing but aremerely things that are governed by our rules and must be regarded astheideal objects of the theory. (Hilbert 1928 [1967: 470],emphasis in original)

According to Hilbert, these ideal objects are necessary in order torecover the general principles of logic, including the law of excludedmiddle, since he considered the development of analysis to beimpossible without them.

Hilbert thus undertook a program to vindicate ideal mathematics on afinitary basis. Since ideal mathematics could be formalized withinlogical calculi such as those developed in Whitehead andRussell’sPrincipia Mathematica, the aim of the Hilbert program became to prove the consistency of theformalized mathematical theories of analysis and set theory. To thisend, Hilbert and his collaborators developed the tools of prooftheory, including the\(\varepsilon\)-calculus. On the conceptual side, the real propositions were intended asanalogous to experimental observations in physics, which can confirmor refute a theory. In this analogy, ideal mathematics is like aphysical theory that gives general laws, only individual instances ofwhich can be verified. Ideal mathematics should thus be conservativeover real mathematics: any real proposition which can be proved viaideal methods should also be provable in a finitary way.

In light of Tait’s (1981) analysis of finitistic reasoning asprimitive recursive reasoning, the \(\Pi^0_2\)-conservativity of\(\sfRCA_0\) over \(\PRA\) (§4.1) takes on a philosophical dimension related to Hilbert’sconservativity program. Tait argues for two claims, now commonlyreferred to asTait’s theses. The first is that thefinitist functions \(f : \bbN\rightarrow \bbN\) are exactly theprimitive recursive functions. The second is that the finitisticallyprovable \(\Pi^0_1\) (i.e., real) sentences are exactly those provablein the formal system \(\PRA\). By the conservativity theorem statedabove, these are also exactly the \(\Pi^0_1\) sentences provable in\(\sfRCA_0\), and moreover the computable functions which \(\sfRCA_0\)can prove are total are precisely the primitive recursive ones.Although \(\sfRCA_0\) is evidently in some sense an infinitary systemin which substantial mathematical reasoning about infinitary objectscan be carried out, in virtue of the conservativity theorem and itsconsequences it also has some claim to being reducible to a finitarysystem, and thus perhaps in some instrumental way acceptable to thefinitist. This kind of finitistic reductionism is discussed further in§5.3.

Tait’s theses have been widely discussed and become broadlyaccepted, although not without their share of criticism along the way.These criticisms can be broken down into two rough types, historicaland conceptual, although these are sometimes intertwined. On theconceptual side, there are two groups of complainants: those whoconsider Tait’s analysis too liberal, such as Ganea (2010), andthose who consider it too conservative. Kreisel (1958, 1970) is aprominent example of the latter, arguing that finitist provabilityshould instead be identified with provability in \(\PA\). Central tothe disagreement between Kreisel and Tait is the status of functions\(f : \bbN\to \bbN\) which are computable but not primitive recursive,and thus while arguably finitary in nature, nonetheless transgresswhat Tait considers the boundaries of finitism.

The quintessential example of such a function is theAckermann–Péter function. Discovered in 1928 by Wilhelm Ackermann, a member of the Hilbertschool whose dissertation provided the first substantive example of afinitistic consistency proof, it was subsequently simplified byPéter (1935), and then further simplified by Robinson (1948).The Ackermann–Péter function is defined, by adoubly-recursive definition, as

Contemporary views differ as to whether theAckermann–Péter function is finitary in nature, and evenon whether Hilbert considered it to be so. In the course of defendingthe view that finitistic provability coincides with provability in\(\PA\), Kreisel (1970) points to Hilbert’s explicit discussionof Ackermann’s function in Hilbert 1926 as evidence that Hilbertconsidered the function to be finitary in nature. Taking the oppositeposition, Tait (1981) argues that Kreisel’s view is based on amisreading of Hilbert, and that Hilbert himself did not considerAckermann’s function to be finitarysimpliciter, butfinitary relative to a system of non-finitary types. More recently,Zach (1998) concluded that while in the early 1920s Hilbert did notconceive of his finitism as going beyond primitive recursion, thereare reasons to believe that the later Hilbert, and especially hiscollaborator Bernays, took a different view and considered theAckermann–Péter function, along with other functionsdefined by means of higher-type recursions, to be finitary in nature.For further discussions of these issues see Tait 2002; Zach 2003; andDean 2015.

5.3 Finitistic reductionism and \(\WKL_0\)

According to the two theses advanced by Tait (1981) and which thediscussion of \(\sfRCA_0\) and finitism in§5.2 centred on, the finitist functions are precisely the primitiverecursive functions, while the finitist theorems are precisely the\(\Pi^0_1\) sentences provable in \(\PRA\). Assuming that one grantsthe correctness of Tait’s theses in terms of determining theextent and limits of finitist mathematics, and that Gödel’sincompleteness theorems pose an insurmountable barrier to a genuinerealization of the Hilbertian dream of reducing all infinitarymathematics to finitary mathematics, questions still remain concerningthe extent to which ideal mathematics could be recovered by aHilbertian reduction. Simpson (1988) proposed what he called a partialrealization of Hilbert’s program. Simpson’s ideas followthose of Hilbert from the mid-1920s onwards, in which the program ofgiving a finitary proof of the consistency of infinitary mathematicswas replaced by the program of demonstrating the conservativity ofinfinitary mathematics over real mathematics: that is, showing that ifa finitistically-meaningful statement admits of an ideal proof, thenit is also finitistically true.

Gödel’s incompleteness theorems seem to show that thisconservativity program cannot succeed, at least if we accept that allfinitary reasoning can be formalized within a fixed axiomatic systemT such as \(\PRA\). Wherever we draw the line between finitaryand infinitary mathematics, finitary mathematics cannot prove its ownconsistency, let alone that of infinitary mathematics. Simpson acceptsthis piece of received wisdom about the impact of the incompletenesstheorems on Hilbert’s program, but argues that we cannonetheless achieve a partial realization of Hilbert’s program.The program of finitistic reductionism which Simpson proposes leans onthe \(\Pi^0_2\)-conservativity of \(\WKL_0\) over \(\PRA\) (§4.1). The idea is that any finitistically meaningful (i.e., \(\Pi^0_1\))sentence \(\varphi\) that can be proved in the ideal, infinitarysystem \(\WKL_0\) is also provable in \(\PRA\), and thus byTait’s thesis is finitistically provable.

The mathematics that can be developed in \(\WKL_0\) is extensive, andprima facie this lends a good deal of substance to Simpson’sposition. However, the view has attracted its share of criticism. Notefirst that one might reject the conservativity constraint altogether,as Detlefsen (1990) does. We shall pass over criticisms of this kindsince addressing them would take us too far afield. The second type ofcriticism, typified by Sieg (1990), takes Simpson to task for beinginsufficiently faithful to the historical Hilbert program. Giving thisclaim the attention it deserves would, similar to the first type ofobjection, require a more detailed study than this entry is able to,but readers are directed to the entry onHilbert’s program for starting points from which to investigate this issue. Critics ofthe third type point out that despite the strength of \(\WKL_0\),substantial parts of mathematics—even if we restrict ourselvesto so-called “ordinary mathematics”—require strongeraxioms, as the results in§4.2–§4.4 attest. This is, of course, a fair criticism of the extent of themathematics that can be recovered within Simpson’s finitisticreductionism, but it is also in some sense misplaced, since as Simpsonemphasizes, his program is only intended as a partial realization ofHilbert’s, not a complete one. Moreover, as Simpson points out,finitistic reductionism is not limited to \(\WKL_0\), since there arestrict extensions of \(\WKL_0\) that are still\(\Pi^0_2\)-conservative over \(\PRA\), including the system\(\WKL^+_0\) introduced by Brown & Simpson (1993), and even\(\WKL_0 + \mathsf{RT}^2_2\) (Patey & Yokoyama 2018).

A more incisive and subtle line of argument stems from the status ofthe conservativity theorem itself. The mere fact that \(\WKL_0\) is\(\Pi^0_2\)- conservative over \(\PRA\) is not sufficient to establisha genuinely finitistic reduction, since in order to appeal to it, theconservativity result must be provable from the finitary standpoint.This objection can be partially rebutted by appealing to Sieg’s(1985) theorem that there exists a primitive recursive prooftransformation that will transform any \(\WKL_0\) proof of a\(\Pi^0_2\) sentence into a \(\PRA\) proof of that same sentence. Ifwe accept Tait’s theses, then the proof transformation is afinitary procedure for producing finitary proofs from infinitary ones,just as Hilbert (1928) anticipated.

However, the initial objection can be spelled out in a more damagingway, drawing on a point already made by Tait (1981), namely that histheses provide an external analysis of finitism rather than aninternal one which is accessible from the finitary standpoint. Thisbeing the case, the finitist is not in a position to evaluateTait’s theses, since their very characterizations involveinfinitary notions such as that of an arbitrary function \(f : \bbN\to\bbN\) which the finitist neither understands nor accepts. Burgess(2010) argues that because of this, the finitist cannot understandSieg’s conservativity proof as giving a method of transformingproofs in a formal system for ideal mathematics, \(\WKL_0\), intoproofs in a contentual finitary system. Instead, they can onlyunderstand it as a mechanism for transforming proofs in one formalsystem into proofs in another. They can then laboriously verify thateach \(\PRA\) proof obtained by applying the proof transformation isindeed a finitary proof. However, they cannot accept the general claimthat all such proofs are finitary proofs, since this would amount toaccepting the reflection principle for \(\PRA\), which implies theconsistency of \(\PRA\)—a statement which, by Tait’ssecond thesis and Gödel’s second incompleteness theorem, isnot finitistically provable (Giaquinto 1983; Dean 2015).

5.4 Arithmetical definability and predicativity

Arithmetical definability has been linked to predicative approaches tothe foundations of mathematics sinceHermann Weyl’s monographDas Kontinuum (Weyl 1918). Weyl argued that thecontemporary set-theoretic construction of the real numbers and theassociated theory of analysis was a “house [ …] toa large degree built on sand” (Weyl 1994: 1). The task he setfor himself was to develop a theory of analysis based on which did notfall foul ofRussell’s paradox, and which embodied a mathematically more natural approach thanRussell’s theory of types. As Weyl himself noted, the ideas ofDas Kontinuum have muchin common with the approaches of Russell and Poincaré. Theyagree in their rejection of impredicative comprehension, andWeyl’s system of levels corresponds to Russell’s theory oftypes (Russell 1908; Whitehead & Russell 1910). As such,Weyl’s views have justly been calledpredicative.Despite these commonalities, Weyl was critical about what he saw asthe imprecision of Poincaré’s account, and he stronglydisagreed with several pillars of the Russellian approach. Inparticular, he rejected some of the reductionist aspects ofRussell’s logicism, which defined natural numbers by means ofequivalence classes, while Weyl took them to be fundamental. Weyl alsorejected Russell’s axiom of reducibility and took theirpositions to be “separated by a veritable abyss” (Weyl1994: 47).

In developing his system Weyl was guided by two key views. Firstly, heagreed with Poincaré about the fundamentality to mathematicalthought of the idea of iteration, as embodied by the infinite sequenceof natural numbers. Secondly, he did not merely reject naivecomprehension and the idea that every concept (however preciselydefined) has an associated extension. Instead he proposed axioms, orprinciples of definition, on which only what we now recognizeas first-order definable properties can be unproblematically taken tohave extensions. Weyl accepted that the use of his system would leadto the loss of some mathematical principles that were accepted underthe set-theoretic orthodoxy of Cantor and Dedekind. One such casualtywas the least upper bound axiom, the principle that every bounded setof real numbers has a least upper bound. Nevertheless, many importantconsequences of the least upper bound axiom still hold in Weyl’ssystem, such as the monotone convergence theorem and a sequential formof the Heine–Borel theorem.

After the publication ofDas Kontinuum, Weyl took an evenmore radical step away from the set-theoretic view of analysis andembraced Brouwer’sintuitionism. The subject of predicative analysis was not taken up again until the1950s, when Grzegorczyk (1955) revisited Weyl’s ideas using thenew tools of computability and definability theory. Grzegorczykidentified Weyl’s analysis with what he called, in common withmany at the time,elementary analysis, meaning that everyreal number must be given by an elementary (that is to say,first-order) definition. This amounted to studying analysisconstrained to the minimum \(\omega\)-model of \(\ACA_0\), the class\(\ARITH\) of arithmetical sets. Kondô (1958) and Mostowski(1959) pursued similar approaches to elementary or arithmeticalanalysis. All three were influenced by the developments in hierarchytheory and its relationship to descriptive set theory, whichclassifies sets of real numbers in terms of their descriptivecomplexity. Kondô in particular seems to have been influenced bythe French analysts and “semi-intuitionists” Borel, Baire,and Lebesgue, who first developed what we now call descriptive settheory in the early twentieth century. They used the tools ofCantorian set theory to define hierarchies of sets and functions interms of the complexity of their construction (Kanamori 1995), butwere skeptical about many aspects of the Cantorian picture, includingthe axiom of choice (Moore 1982).

Both Grzegorczyk and Mostowski offer axiomatizations of their approachto arithmetical analysis which are closely related to \(\ACA_0\).Grzegorczyk’s axioms (Grzegorczyk 1955: 337–338) are thosefor Peano arithmetic, formulated in the simple theory of types, butwith comprehension restricted to formulas in which the onlyquantifiers are those of the lowest type, that of natural numbers.This restricted comprehension principle is thus a form of arithmeticalcomprehension, albeit for higher types as well as for sets of naturalnumbers. Mostowski, on the other hand, provides an axiomatizationderived from Gödel–Bernays set theory \(\mathrm{GB}\)(Mostowski 1959: 184–185). \(\mathrm{GB}\) is a two-sortedtheory in which the first sort of variables range over sets, and thesecond sort over classes. In Mostowski’s system, the first sortof variables range over natural numbers and the second sort range oversets of natural numbers. This produces an axiomatic system close to\(\ACA_0\) whose minimum \(\omega\)-model is \(\ARITH\).

As Feferman (1988) explores, there are several ways in which\(\ACA_0\) does not completely correspond to Weyl’s system. Tobegin with, it is unclear whether Weyl would have accepted the fullinduction scheme (\ref{eq:ind_scheme}), or just the induction axiom(\ref{eq:ind_axiom}). \(\ACA_0\) only has the latter, and adding theformer produces the proof-theoretically stronger system \(\ACA\). Weylalso admits an iteration principle (principle 8) that is notfirst-order definable, although this discrepancy in his approach wasnot known to him (Feferman 1998: 265). Nevertheless, the axioms of\(\ACA_0\) can be justified on the predicative grounds given inDas Kontinuum, and its substantial mathematical strengthshows that Weyl was right to think that systems in which onlyfirst-order comprehension is admissible suffice for many applications.For further reading on predicativity and its historical development,see Feferman (2005). §2.2 of Dean & Walsh (2017) provides amore complete account of the development of arithmetical analysis byGrzegorczyk, Kondô, and Mostowski.

5.5 Arithmetical transfinite recursion and the limits of predicativity

The renewed interest in predicative mathematics that materialized inthe 1950s following the discovery of the computability-theoretichierarchies (§5.4) led to a series of conceptual and technical developments thatextended and refined the notions of predicative definability andpredicative provability, as well as offering sophisticated analyses ofthese notions in terms of both computability theory and proof theory.Following Grzegorczyk, Mostowski, and Kondô’s arithmeticalanalysis of Weyl’s predicativism (§5.4), Kreisel (1960) suggested that sets of natural numbers werepredicative if they appeared in the hyperarithmetical hierarchy. Onthe proof-theoretic side, this led to the identification of systemslike \(\Delta^1_1\text{-}\CA_0\) and\(\Sigma^1_1\text{-}\mathsf{AC}_0\) as predicative (Kreisel 1962),since the class of hyperarithmetical sets \(\HYP\) is an\(\omega\)-model of both systems.

Nevertheless, Kreisel’s proposal still appeared to contain animpredicative component. Any hyperarithmetical well-ordering ispredicatively definable, as a subset of the natural numbers, since bya result of Spector (1955) such a well-ordering will in fact becomputable. However, the fact that the ordering is in fact awell-ordering is not in general something that can be predicativelydetermined: being a well-ordering is a \(\Pi^1_1\) property, since itinvolves quantifying over all possible infinite descending sequencesin the ordering, or equivalently, over all subsets of the ordering.Indeed, the set of all codes for computable well-orderings,Kleene’s \(\mathcal{O}\), is \(\Pi^1_1\)-complete and thus aquintessentially impredicative object (Kleene 1955: 207). This worryhad already been noted by Kreisel (1960: 27), and the resulting ideaof examining which computable linear orderings could be predicativelyproved to be well-orderings led to a series of advances in the1960s.

Embodied in the hyperarithmetical hierarchy is the notion oframification: splitting the sets in \(\powset{\omega}\) intolevels which are built up via a transfinite iteration. This idea hadalready appeared in several forms in Russell’s attempts toovercome the set-theoretic paradoxes and found mathematics on alogicist basis. In the context of analysis and the predicative theoryof sets of natural numbers, theramified analytical hierarchyis a transfinite hierarchy of sets of natural numbers, defined by theconditions

where \(D^*\) is the set obtained from \(D \subseteq \powset{\omega}\)by putting \(X \in D^*\) iff there is an \(\calL_2\)-formula\(\varphi\) such that for all \(n \in \bbN\), \(n \in X\leftrightarrow \varphi(n)\) when all the second-order quantifiers in\(\varphi\) are restricted to range over \(D\). The connection topredicativity lies in the fact that second-order quantification isadmissible only if the range of quantification has already been shownto exist, at some earlier stage in the construction of the hierarchy.The hyperarithmetical sets were shown by Kleene (1959) to be exactlythose which appear in the ramified analytical hierarchy before stage\(\wck\), i.e., \(\HYP= R_{\wck}\).

Once provability is in the picture as a condition on the ordinals\(\alpha\) which are to be considered predicative, one needs formalsystems in which such \(\alpha\) controls the length of the permittediteration of predicative definability. This gave rise to thedevelopment of transfinite progressions of formal systems oframified analysis. The system \(\mathbf{RA}_\alpha\)associated with an ordinal \(\alpha\) has variables\(X_1^\beta,X_2^\beta,\dotsc\) for each \(\beta \leq \alpha\), andaxioms asserting that the sets of the \(\beta\)-th level of theramified analytical hierarchy exists for all \(\beta \leq\alpha\).

The predicative ordinals can then be defined within this setting asfollows. If \(\alpha\) is a predicative ordinal, \(\prec\) is (a setcoding a) linear ordering, and \(\beta\) is the order-type of\(\prec\), then \(\beta\) is predicative if \(\mathrm{RA}_\alpha\vdash \mathrm{WO}(\prec)\). This is sometimes called theautonomy condition. The predicative ordinals are thusgenerated by starting from 0 and proving that larger and largerordinals are predicative, within stronger and stronger formal systems\(\mathbf{RA}_\alpha\), where \(\alpha\) has been shown to bepredicative within some weaker system \(\mathbf{RA}_\beta\) for\(\beta \lt \alpha\). Feferman (1964) and Schütte (1965b, 1965a)independently proved that the least impredicative ordinal is\(\Gamma_0\), now known as the Feferman–Schütte ordinal orthe ordinal of predicativity. Thus we can characterize thepredicatively provable statements as those which can be proved in some\(\mathbf{RA}_\alpha\) for \(\alpha \lt \Gamma_0\).

The proof-theoretic ordinal of \(\ATR_0\) is also \(\Gamma_0\), justlike the union of all predicative systems of ramified analysis\(\mathbf{RA}_{\lt\Gamma_0} = \bigcup_{\alpha \lt \Gamma_0}\mathbf{RA}_\alpha\). Moreover, \(\ATR_0\) is \(\Pi^1_1\)-conservativeover \(\mathbf{RA}_{\lt\Gamma_0}\), so any \(\Pi^1_1\) sentence\(\varphi\) provable in \(\ATR_0\) will also be provable within some\(\mathbf{RA}_\alpha\) for \(\alpha \lt \Gamma_0\)—in orderwords, \(\varphi\) will have a predicative proof. In line with thereductive program in proof theory, systems which are proof-theoretically reducible to a system\(\mathbf{RA}_\alpha\) for \(\alpha \lt \Gamma_0\) are calledpredicatively reducible. \(\ATR_0\) cannot be predicativelyreducible, since it is proof-theoretically reducible only to the unionof all predicative subsystems of ramified analysis, and can prove theconsistency of any individual \(\mathbf{RA}_\alpha\) for \(\alpha \lt\Gamma_0\). However, because of the conservativity result above,\(\ATR_0\) is consideredlocally predicatively reducible, inthe sense that any \(\Pi^1_1\) consequence of \(\ATR_0\) can berecovered within a predicative subsystem of ramified analysis.

This property led Simpson (1985) to propose that \(\ATR_0\) could playan important role in a program ofpredicative reductionismanalogous to the program of finitistic reductionism (§5.3). The value of such a program would lie in the fact that whilearithmetical transfinite recursion is equivalent to many mathematicaltheorems that cannot be recovered in the more obviously predicativesystem \(\ACA_0\), few results have been found in the gap between\(\ACA_0\) and \(\ATR_0\). This situation had already been noted inthe 1960s by Kreisel, who remarked that

in the portions of analysis developed by working mathematicians, atheorem is either derivable by means of the arithmetic comprehensionaxiom or else not predicative at all (not even true when relativizedto \(\HYP\) functions). (Kreisel 1962: 316)

\(\ATR_0\), by contrast, proves many theorems in descriptive settheory, algebra, and other areas of mathematics that cannot be provedwithin individual predicative systems. The idea that it can be usedinstrumentally by the predicativist to prove \(\Pi^1_1\) theoremswhich are then, by the conservativity theorem, anointed aspredicatively legitimate, is one which holds some appeal.

Nevertheless, this view is vulnerable to a version of the samecriticism advanced by Burgess (2010) against finitistic reductionism.Although the predicativist will be able to prove the conservativitytheorem, and see that any \(\Pi^1_1\) theorem will be provable in some\(\mathbf{RA}_\alpha\), this does not by itself give them a warrantfor the predicative provability of that theorem, since theidentification of predicative provability with provability in\(\mathbf{RA}_{\lt\Gamma_0}\) is an external analysis predicated on,amongst other things, the fact that \(\Gamma_0\) is a well-definedobject—something the predicativist is, if theFeferman–Schütte analysis is correct, incapable of agreeingto. They must instead verify that the proof given by the reduction isindeed predicatively acceptable, and in the process check that therelevant \(\alpha\) is a predicative ordinal. The advantage of thereductionist approach must therefore lie, as Burgess points out, notin a shortcut to predicative provability, but in some conceptualadvantage obtained by reasoning via the axiom scheme of arithmeticaltransfinite recursion. Moreover, the very reverse mathematical resultsthat appear to make predicative reductionism an attractive prospectalso present a problem of sorts. Since statements like the perfect settheorem are not merely provable in \(\ATR_0\), but actually equivalentto its characteristic axiom, they themselves are strictly speakingimpredicative. It is therefore only their \(\Pi^1_1\) consequenceswhich can be obtained via the reduction, not the theoremsthemselves.

6. Further Reading

The primary reference work on reverse mathematics and the Big Five isStephen Simpson’sSubsystems of Second Order Arithmetic(Simpson 2009). Denis Hirschfeldt’s monographSlicing theTruth (2014) is an introductory textbook aimed at graduatestudents in mathematical logic. Its focus is combinatorial principlessuch as \(\mathsf{RT}^2_2\) which are not covered in detail by Simpson(2009). Damir Dzhafarov and Carl Mummert’sReverseMathematics: Problems, Reductions, and Proofs (Dzhafarov &Mummert 2022) is a comprehensive introduction to contemporary reversemathematics which presents \(\sfRCA_0\)-provable entailment as justone amongst many notions of reduction, and which also provides anup-to-date treatment of many areas of importance in contemporaryreverse mathematics not covered by Simpson, especially combinatorialprinciples and the Reverse Mathematics Zoo. John Stillwell’sReverse Mathematics: Proofs from the Inside Out (Stillwell2018) is an introductory book aimed at those with at least anundergraduate-level education in mathematics and an interest in thefoundations of mathematics. Reverse mathematics is a relatively youngfield within mathematical logic, and as such there is no definitivehistory. Its origins and those of the main subsystems are traced inDean & Walsh (2017), which also provides compendious references tokey historical sources.

A general survey of the motivations, methods, techniques, and problemsof reverse mathematics is Shore (2010). Montalbán (2011)provides a list of open problems in reverse mathematics, although thereader should be aware that many of them have now been solved, andthat the direction of research in reverse mathematics has shiftedsomewhat since the publications of both (Montalbán 2011) and(Shore 2010). Two areas of particular note are underrepresented inthese surveys. The first is more fine-grained reducibility notions for\(\Pi^1_2\) sentences, such as Weihrauch reducibility. A recent surveyof Weihrauch reducibility and computable analysis is Brattka,Gherardi, & Pauly (2021), while a more general discussion ofreducibility notions for \(\Pi^1_2\) sentences can be found inHirschfeldt & Jockusch (2016). The second ishigher-orderreverse mathematics, which modifies the formal framework ofsecond-order arithmetic to include third- and higher-order entities,thereby allowing more direct formal representations of manymathematical objects in analysis, topology, and the like. Shore (2010,2013) proposes an approach to higher-order reverse mathematics usinghigher recursion theory, but more influential has beenKohlenbach’s approach using higher-order arithmetic (Kohlenbach2002, 2005). Some striking results have been proved in this framework.For example, Normann & Sanders (2019a) showed that third-orderformalizations of Cousin’s and Lindelöf’s lemmas bothimply full second-order arithmetic. Other recent work in higher-orderreverse mathematics studies transfinite recursion (Schweber 2015), thestrength of theorems of analysis such as Cousin’s lemma andproperties of the gauge integral (Normann & Sanders 2019b),theorems about open sets (Normann & Sanders 2020), and topologicalnotions like dimension and paracompactness (Sanders 2020).

Finally, although issues relating to constructive and intuitionisticmathematics have been addressed at several points, this entry focusesalmost exclusively on reverse mathematics in the setting of classicallogic. This leaves out the various approaches to reverse mathematicsin a constructive or intuitionistic setting. Contemporary forms ofconstructive reverse mathematics were explicitly initiated by Ishihara(2005, 2006) and Veldman (2009, 2014), but researchers in the fieldoften view Julian & Richman (1984) as having proved the firstresult in constructive reverse mathematics. Another notable earlyexample is Mandelkern (1988).Section 5 of the entry on constructive mathematics provides an introduction to constructive reverse mathematics, carriedout from within an informal base theory corresponding toBishop’s constructivism. Diener (2020 [Other Internet Resources]) gives a compendious technical overview of results in the field, whileLoeb (2012) offers a critical appraisal of the program.

Bibliography

• Aberth, Oliver, 1980,ComputableAnalysis, New York: McGraw-Hill.
• Ackermann, Wilhelm, 1928, “ZumHilbertschen Aufbau der reellen Zahlen”,MathematischeAnnalen, 99(1): 118–133. doi:10.1007/BF01459088
• Arana, Andrew, 2008, “Logical andSemantic Purity”,ProtoSociology, 25: 36–48.doi:10.5840/protosociology2008253
• Arana, Andrew and Paolo Mancosu, 2012,“On the Relationship between Plane and Solid Geometry”,The Review of Symbolic Logic, 5(2): 294–353.doi:10.1017/S1755020312000020
• Baldwin, John T., 2013, “Formalization,Primitive Concepts, and Purity”,The Review of SymbolicLogic, 6(1): 87–128. doi:10.1017/S1755020312000263
• Beeson, Michael J., 1985,Foundations ofConstructive Mathematics, Berlin, Heidelberg: Springer BerlinHeidelberg. doi:10.1007/978-3-642-68952-9
• Bernays, P., 1935, “Sur le platonismedans les mathématiques”,L’EnseignementMathématique, 34: 52–69.doi:10.5169/seals-26602
• Bishop, Errett, 1967,Foundations ofConstructive Analysis, New York: McGraw-Hill.
• Bonola, Roberto, 1912,Non-EuclideanGeometry: A Critical and Historical Study of Its Development,Chicago: Open Court.
• Brattka, Vasco, Guido Gherardi,and Arno Pauly, 2021, “Weihrauch Complexity in ComputableAnalysis”, inHandbook of Computability and Complexity inAnalysis (Theory and Applications of Computability), VascoBrattka and Peter Hertling (eds.), Cham: Springer, 367–417.doi:10.1007/978-3-030-59234-9_11
• Bridges, Douglas and Fred Richman,1987,Varieties of Constructive Mathematics (LondonMathematical Society Lecture Note Series), Cambridge: CambridgeUniversity Press. doi:10.1017/CBO9780511565663
• Brown, Douglas K. and Stephen G.Simpson, 1986, “Which Set Existence Axioms are Needed to Provethe Separable Hahn-Banach Theorem?”,Annals of Pure andApplied Logic, 31: 123–144.doi:10.1016/0168-0072(86)90066-7
• –––, 1993, “TheBaire Category Theorem in Weak Subsystems of Second-OrderArithmetic”,Journal of Symbolic Logic, 58(2):557–578. doi:10.2307/2275219
• Burgess, John P., 2010, “On the OutsideLooking in: A Caution about Conservativeness”, inKurtGödel, Essays for His Centennial (Lecture Notes in Logic),Solomon Feferman, Charles Parsons, and Stephen G. Simpson (eds.),Cambridge/New York: Cambridge University Press, 128–142.doi:10.1017/CBO9780511750762.009
• Cantor, Georg, 1872, “Ueber dieAusdehnung eines Satzes aus der Theorie der trigonometrischenReihen”,Mathematische Annalen, 5(1): 123–132.doi:10.1007/BF01446327
• –––, 1883, “Sur lesensembles infinis et linéaires de points”,ActaMathematica, 2(1): 349–380. doi:10.1007/BF02612169
• Dean, Walter, 2015, “ArithmeticalReflection and the Provability of Soundness”,PhilosophiaMathematica, 23(1): 31–64. doi:10.1093/philmat/nku026
• –––, 2021, “OnConsistency and Existence in Mathematics”,Proceedings ofthe Aristotelian Society, 120(3): 349–393.doi:10.1093/arisoc/aoaa017
• Dean, Walter and Sean Walsh, 2017,“The Prehistory of the Subsystems of Second-OrderArithmetic”,The Review of Symbolic Logic, 10(2):357–396. doi:10.1017/S1755020316000411
• Dedekind, Richard, 1872,Stetigkeit undirrationale zahlen, Braunschweig: Vieweg.
• Detlefsen, Michael, 1990, “On anAlleged Refutation of Hilbert’s Program Using Gödel’sFirst Incompleteness Theorem”,Journal of PhilosophicalLogic, 19(4): 343–377. doi:10.1007/BF00263316
• Dzhafarov, Damir D. and CarlMummert, 2022,Reverse Mathematics: Problems, Reductions, andProofs (Theory and Applications of Computability), Cham:Springer International Publishing. doi:10.1007/978-3-031-11367-3
• Eastaugh, Benedict, 2019, “SetExistence Principles and Closure Conditions: Unravelling the StandardView of Reverse Mathematics”,Philosophia Mathematica,27(2): 153–176. doi:10.1093/philmat/nky010
• Ewald, William Bragg and Wilfried Sieg(eds.), 2013,David Hilbert’s Lectures on the Foundations ofArithmetic and Logic 1917–1933, Berlin/Heidelberg: SpringerBerlin Heidelberg. doi:10.1007/978-3-540-69444-1
• Feferman, Solomon, 1964, “Systems ofPredicative Analysis”,The Journal of Symbolic Logic,29(1): 1–30. doi:10.2307/2269764
• –––, 1988, “WeylVindicated:Das Kontinuum Seventy Years Later”, inTermi e Prospettive Della Logica e Della Filosofia Della ScienzaContemporanee, Vol. 1, pp. 59–93, CLUEB.
• –––, 1998,In theLight of Logic, New York/Oxford: Oxford University Press.
• –––, 2005,“Predicativity”, inThe Oxford Handbook of Philosophyof Mathematics and Logic, Stewart Shapiro (ed.), Oxford: OxfordUniversity Press, 590–624. doi:10.1093/0195148770.003.0019
• Ferreira, Fernando, 2005, “A SimpleProof of Parsons’ Theorem”,Notre Dame Journal ofFormal Logic, 46(1): 83–91.doi:10.1305/ndjfl/1107220675
• Ferreirós, José, 2007,Labyrinth of Thought: A History of Set Theory and Its Role inModern Mathematics, second edition, Basel/Boston:Birkhäuser.
• Friedman, Harvey, 1975, “Some Systemsof Second Order Arithmetic and Their Use”, inProceedings ofthe 17th International Congress of Mathematicians, Vancouver1974, Vol. 1, Ralph D. James (ed.), International MathematicalUnion, 235–242.
• –––, 1976, “Systemsof Second Order Arithmetic with Restricted Induction. I, II”,The Journal of Symbolic Logic, 41(2): 557–559.Abstracts from the Meeting of the Association for Symbolic Logic,Chicago, 1975.
• Friedman, Harvey M., Stephen G.Simpson, and Rick L. Smith, 1983, “Countable Algebra and SetExistence Axioms”,Annals of Pure and Applied Logic,25(2): 141–181. doi:10.1016/0168-0072(83)90012-X
• Ganea, Mihai, 2010, “Two (or Three)Notions of Finitism”,The Review of Symbolic Logic,3(1): 119–144. doi:10.1017/S1755020309990323
• Giaquinto, Marcus, 1983,“Hilbert’s Philosophy of Mathematics”,TheBritish Journal for the Philosophy of Science, 34(2):119–132. doi:10.1093/bjps/34.2.119
• Grzegorczyk, Andrzej, 1955,“Elementarily Definable Analysis”,FundamentaMathematicae, 41(2): 311–338.doi:10.4064/fm-41-2-311-338
• Grzegorczyk,Andrzej, Andrzej Mostowski, and Czesław Ryll-Nardzewski, 1958,“The Classical and the \(\omega\)-Complete Arithmetic”,The Journal of Symbolic Logic, 23(2): 188–206.doi:10.2307/2964398
• Hartshorne, Robin, 2000,Geometry:Euclid and Beyond (Undergraduate Texts in Mathematics), NewYork: Springer New York. doi:10.1007/978-0-387-22676-7
• Hilbert, David, 1899,Grundlagen dergeometrie (Festschrift zur feier der enthüllung desGauss-Weber-denkmals in Göttingen 1), Leipzig: B.G. Teubner.
• –––, 1922,“Neubegründung der mathematik: Erste mitteilung”,Abhandlungen aus dem Seminar der HamburgischenUniversität, 1: 157–177. doi:10.1007/BF02940589
• –––, 1926, “Überdas Unendliche”,Mathematische Annalen, 95:161–190. doi:10.1007/BF01206605
• –––, 1928 [1967],“Die grundlagen der mathematik: Vortrag, gehalten auf Einladungdes Mathematischen Seminars im Juli 1927 in Hamburg”,Abhandlungen aus dem Mathematischen Seminar der UniversitätHamburg, 6: 65–85. Translated in Hilbert 1967.doi:10.1007/BF02940602
• –––, 1967, “TheFoundations of Mathematics”, in van Heijenoort 1967:464–479. Translation of Hilbert 1928.
• Hilbert, David and Paul Bernays, 1934,Grundlagen der Mathematik, Vol. 1, Berlin: Springer.
• –––, 1939,Grundlagen der Mathematik, Vol. 2, Berlin: Springer.
• –––, 1968,Grundlagen der Mathematik, second edition, Vol. I,Berlin/Heidelberg/New York: Springer-Verlag.
• –––, 1970,Grundlagen Der Mathematik, second edition, Vol. II,Berlin/Heidelberg/New York: Springer-Verlag.
• Hirschfeldt, Denis R., 2014,Slicingthe Truth: On the Computable and Reverse Mathematics of CombinatorialPrinciples (Lecture Notes Series, Institute for MathematicalSciences, National University of Singapore 28), Chitat Chong, Qi Feng,Theodore A Slaman, W Hugh Woodin, and Yue Yang (eds.),Singapore/Hackensack, NJ: World Scientific. doi:10.1142/9208
• Hirschfeldt, Denis R. and Carl G.Jockusch, 2016, “On Notions of Computability-Theoretic ReductionBetween \(\Pi^1_2\) Principles”,Journal of MathematicalLogic, 16(1): 1650002. doi:10.1142/S0219061316500021
• Howard, Paul and Jean E. Rubin, 1998,Consequences of the Axiom of Choice, Providence, RI: AmericanMathematical Society. doi:10.1090/surv/059
• Ishihara, Hajime, 2005, “ConstructiveReverse Mathematics: Compactness Properties”, inFrom Setsand Types to Topology and Analysis: Towards Practicable Foundationsfor Constructive Mathematics (Oxford Logic Guides 48), LauraCrosilla and Peter Schuster (eds.), Oxford: Clarendon Press,245–267. doi:10.1093/acprof:oso/9780198566519.003.0016
• –––, 2006, “ReverseMathematics in Bishop’s Constructive Mathematics”,Philosophia Scientae, CS 6: 43–59.doi:10.4000/philosophiascientiae.406
• Jech, Thomas J., 1973,The Axiom ofChoice (Studies in Logic and the Foundations of Mathematics 75),Amsterdam: North-Holland.
• Jockusch, Carl G., 1972,“Ramsey’s Theorem and Recursion Theory”,TheJournal of Symbolic Logic, 37(2): 268–280.doi:10.2307/2272972
• Jockusch, Carl G. and Robert I. Soare,1972, “\(\Pi^0_1\) Classes and Degrees of Theories”,Transactions of the American Mathematical Society, 361:5805–5837. doi:10.1090/S0002-9947-1972-0316227-0
• Julian, William H. and Fred Richman,1984, “A Uniformly Continuous Function on [0, 1] That IsEverywhere Different from Its Infimum”,Pacific Journal ofMathematics, 111(2): 333–340.doi:10.2140/pjm.1984.111.333
• Kanamori, Akihiro, 1995, “TheEmergence of Descriptive Set Theory”, inFrom Dedekind toGödel, Jaakko Hintikka (ed.), (Synthese Library 251),Dordrecht: Kluwer Academic Publishing, 241–262.doi:10.1007/978-94-015-8478-4_10
• Kechris, Alexander S., 1995,ClassicalDescriptive Set Theory (Graduate Texts in Mathematics, 156), NewYork: Springer-Verlag. doi:10.1007/978-1-4612-4190-4
• Kino, A., John Myhill, and R. E. Vesley (eds.), 1970,Intuitionism and Proof Theory. Proceedings of the SummerConference at Buffalo, N.Y., 1968 (Studies in Logic and theFoundations of Mathematics 60), Amsterdam: North-Holland.
• Kleene, Stephen C., 1945, “On theInterpretation of Intuitionistic Number Theory”,The Journalof Symbolic Logic, 10(4): 109–124. doi:10.2307/2269016
• –––, 1952, “RecursiveFunctions and Intuitionistic Mathematics”, inProceedings ofthe International Congress of Mathematicians, 1950, Vol. 1,Lawrence M. Graves, Einar Hille, Paul A. Smith, & Oscar Zariski(eds.), Providence, RI: American Mathematical Society,679–685.
• –––, 1955,“Hierarchies of Number-Theoretic Predicates”,Bulletinof the American Mathematical Society, 61(3): 193–213.doi:10.1090/S0002-9904-1955-09896-3
• –––, 1959,“Quantification of Number-Theoretic Functions”,Compositio Mathematica, 14: 23–40. [Kleene 1959 available online]
• Kohlenbach, Ulrich, 2002,“Foundational and Mathematical Uses of Higher Types”, inSieg, Sommer, and Talcott 2002: 92–116.doi:10.1017/9781316755983.005
• –––, 2005, “HigherOrder Reverse Mathematics”, inReverse Mathematics 2001(Lecture Notes in Logic 21), Stephen G. Simpson (ed.), Natick, MA:A. K. Peters, 281–295. doi:10.1017/9781316755846.018
• Kondô, Motokiti, 1958, “Sur lesensembles nommables et le fondement de l’analysemathématique, I”,Japanese Journal ofMathematics, 28: 1–116. doi:10.4099/jjm1924.28.0_1
• König, Dénes, 1927,“Über eine Schlussweise aus dem Endlichen insUnendliche”,Acta Litterarum Ac Scientiarum RagiaeUniversitatis Hungaricae Francisco-Josephinae, 3:121–130.
• Kreisel, Georg, 1958, “MathematicalSignificance of Consistency Proofs”,The Journal of SymbolicLogic, 23(2): 155–182. doi:10.2307/2964396
• –––, 1959, “Analysisof the Cantor–Bendixson Theorem by Means of the AnalyticHierarchy”,Bulletin de l’Académie Polonaisedes Sciences. Série des Sciences Mathématiques,Astronomiques et Physiques, 7: 621–626.
• –––, 1960, “LaPredicativité”,Bulletin de La SociétéMathématiques de France, 88: 371–391.
• –––, 1962, “The Axiomof Choice and the Class of Hyperarithmetic Functions”,Indagationes Mathematicae (Proceedings), 65: 307–319.doi:10.1016/S1385-7258(62)50029-2
• –––, 1970,“Principles of Proof and Ordinals Implicit in GivenConcepts”, in Kino, Myhill, and Vesley 1970: 489–516.
• Kushner, Boris A., 2006, “TheConstructive Mathematics of A. A. Markov”,The AmericanMathematical Monthly, 113(6): 559–566.doi:10.2307/27641983
• Lewis, Florence P., 1920, “History of theParallel Postulate”,The American Mathematical Monthly,27(1): 16–23. doi:10.2307/2973238
• Liu, Jiayi, 2012, “\(\mathsf{RT}^2_2\) doesnot imply \(\WKL_0\)”,The Journal of Symbolic Logic,77(2): 609–620. doi:10.2178/jsl/1333566640
• Loeb, Iris, 2012, “QuestioningConstructive Reverse Mathematics”,ConstructivistFoundations, 7(2): 131–140. [Loeb 2012 available online]
• Mandelkern, Mark, 1988, “LimitedOmniscience and the Bolzano–Weierstrass Principle”,Bulletin of the London Mathematical Society, 20(4):319–320. doi:10.1112/blms/20.4.319
• –––, 1989,“Brouwerian Counterexamples”,MathematicsMagazine, 62(1): 3–27.doi:10.1080/0025570X.1989.11977404
• Metakides, George, Anil Nerode,and Richard A. Shore, 1985, “Recursive Limits on theHahn–Banach Theorem”, inErrett Bishop: Reflections onHim and His Research (Contemporary Mathematics 39), MurrayRosenblatt (ed.), Providence, RI: American Mathematical Society,85–91.
• Montalbán, Antonio, 2011,“Open Questions in Reverse Mathematics”,The Bulletinof Symbolic Logic, 17(3): 431–454.doi:10.2178/bsl/1309952320
• Montalbán, Antonio and RichardA. Shore, 2012, “The Limits of Determinacy in Second-OrderArithmetic”,Proceedings of the London MathematicalSociety, 104(2): 223–252. doi:10.1112/plms/pdr022
• Moore, Gregory H., 1982,Zermelo’sAxiom of Choice: Its Origins, Development, and Influence(Studies in the History of Mathematics and Physical Sciences 8), NewYork: Springer-Verlag. doi:10.1007/978-1-4613-9478-5
• Moschovakis, Joan Rand, to appear,“Markov’s Principle, Markov’s Rule and the Notion ofConstructive Proof”, inIntuitionism, Computation and Proof:Selected themes from the research of G. Kreisel, M. AntonuttiMarfori and M. Petrolo (eds.). [Moschovakis to appear available online]
• Mostowski, Andrzej, 1959, “On VariousDegrees of Constructivism”, inConstructivity inMathematics. Proceedings of the Colloquium Held at Amsterdam,1957, Arend Heyting (ed.), Amsterdam: North-Holland,178–194. Collected inFoundational Studies: Selected Works.Volume 2 (Studies in Logic and the Foundations of Mathematics93, Part B), Amsterdam: North-Holland, 359–375.doi:10.1016/S0049-237X(09)70270-8
• Mummert, Carl and Stephen G. Simpson,2005, “Reverse Mathematics and \(\Pi^1_2\) Comprehension”,The Bulletin of Symbolic Logic, 11(4): 526–533.doi:10.2178/bsl/1130335208
• Nagorny, N. M., 1994, “Andrei Markovand Mathematical Constructivism”, inLogic, Methodology andPhilosophy of Science IX: Proceedings of the Ninth InternationalCongress of Logic, Methodology and Philosophy of Science (Studiesin Logic and the Foundations of Mathematics 134), Dag Prawitz, BrianSkyrms, and Dag Westerståhl (eds.), Amsterdam: North-Holland,467–479. doi:10.1016/S0049-237X(06)80057-1
• Normann, Dag and Sam Sanders, 2019a,“The Strength of Compactness in Computability Theory andNonstandard Analysis”,Annals of Pure and AppliedLogic, 170(11): 102710. doi:10.1016/j.apal.2019.05.007
• –––, 2019b,“On the Mathematical and Foundational Significance of theUncountable”,Journal of Mathematical Logic, 19(1):1950001. doi:10.1142/S0219061319500016
• –––, 2020,“Open Sets in Computability Theory and ReverseMathematics”,Journal of Logic and Computation, 30(8):1639–1679. doi:10.1093/logcom/exaa049
• Pambuccian, Victor, 1996, “Splittingthe Pasch Axiom”,Journal of Geometry, 56(1–2):126–130. doi:10.1007/BF01222689
• –––, 2001,“Fragments of Euclidean and Hyperbolic Geometry”,Scientiae Mathematicae Japonicae, 53(2): 361–400.
• –––, 2006,“Axiomatizations of Hyperbolic and Absolute Geometries”,inNon-Euclidean Geometries: János Bolyai MemorialVolume (Mathematics and Its Applications 581), AndrásPrékopa and Emil Molnár (eds.), Boston, MA: Springer,119–153. doi:10.1007/0-387-29555-0_7
• –––, 2009, “AReverse Analysis of the Sylvester–Gallai Theorem”,Notre Dame Journal of Formal Logic, 50(3): 245–260.doi:10.1215/00294527-2009-010
• –––, 2019,“Prolegomena to Any Theory of Proof Simplicity”,Philosophical Transactions of the Royal Society A, 377(2140):20180035. doi:10.1098/rsta.2018.0035
• Pambuccian, Victor and Celia Schacht,2021, “The Case for the Irreducibility of Geometry toAlgebra”,Philosophia Mathematica, 30(1): 1–31.doi:10.1093/philmat/nkab022
• Parsons, Charles, 1970, “On aNumber-Theoretic Choice Schema and Its Relation to Induction”,in Kino, Myhill, and Vesley 1970: 459–473.doi:10.1016/S0049-237X(08)70771-7
• Patey, Ludovic and Keita Yokoyama,2018, “The Proof-Theoretic Strength of Ramsey’s Theoremfor Pairs and Two Colors”,Advances in Mathematics,330: 1034–1070. doi:10.1016/j.aim.2018.03.035
• Péter, Rósza, 1935,“Konstruktion nichtrekursiver funktionen”,Mathematische Annalen, 111(1): 42–60.doi:10.1007/BF01472200
• Pour-El, Marian B. and J. IanRichards, 1989,Computability in Analysis and Physics(Perspectives in Mathematical Logic), Berlin/New York: SpringerVerlag.
• Robinson, Raphael M., 1948, “Recursionand Double Recursion”,Bulletin of the American MathematicalSociety, 54(10): 987–993.doi:10.1090/S0002-9904-1948-09121-2
• Rosenfeld, B. A., 1976 [1988],lstoriya Neevklidovoi Geometrii: Razvitie ponyatiya ogeometriceskom prostranslve, Moscow: Nauka; translated asAHistory of Non-Euclidean Geometry: Evolution of the Concept of aGeometric Space (Studies in the History of Mathematics andPhysical Sciences 12), Abe Shenitzer (trans.), New York:Springer-Verlag. doi:10.1007/978-1-4419-8680-1
• Rubin, Herman and Jean E. Rubin, 1963,Equivalents of the Axiom of Choice, Amsterdam:North-Holland.
• –––, 1985,Equivalents of the Axiom of Choice, II (Studies in Logic andthe Foundations of Mathematics 116), Amsterdam/New York:North-Holland.
• Russell, Bertrand, 1908, “MathematicalLogic as Based on the Theory of Types”,American Journal ofMathematics, 30(3): 222–262. doi:10.2307/2369948
• Sanders, Sam, 2020, “ReverseMathematics of Topology: Dimension, Paracompactness, andSplittings”,Notre Dame Journal of Formal Logic, 61(4):537–559. doi:10.1215/00294527-2020-0021
• –––, 2022, “LiftingProofs from Countable to Uncountable Mathematics”,Information and Computation, 287: 104762.doi:10.1016/j.ic.2021.104762
• Schütte, Kurt, 1965a, “EineGrenze Für die Beweisbarkeit der Transfiniten Induktion in derVerzweigten Typenlogik”,Archiv für Mathematische Logikund Grundlagenforschung, 7(1–2): 45–60.doi:10.1007/BF01972460
• –––, 1965b,“Predicative Well-Orderings”, inFormal Systems andRecursive Functions: Proceedings of the Eighth Logic Colloquium,Oxford, July 1963 (Studies in Logic and the Foundations ofMathematics 40), J. N. Crossley and Michael Dummett (eds.), Amsterdam:North-Holland, 280–303. doi:10.1016/S0049-237X(08)71694-X
• Schweber, Noah, 2015, “TransfiniteRecursion in Higher Reverse Mathematics”,The Journal ofSymbolic Logic, 80(3): 940–969. doi:10.1017/jsl.2015.2
• Seetapun, David and Theodore A.Slaman, 1995, “On the Strength of Ramsey’s Theorem”,Notre Dame Journal of Formal Logic, 36(4): 570–582.doi:10.1305/ndjfl/1040136917
• Shore, Richard A., 2010, “ReverseMathematics: The Playground of Logic”,The Bulletin ofSymbolic Logic, 16(3): 378–402.doi:10.2178/bsl/1286284559
• –––, 2013, “ReverseMathematics, Countable and Uncountable: A ComputationalApproach”, inEffective Mathematics of the Uncountable(Lecture Notes in Logic), Denis R. Hirschfeldt, Noam Greenberg, JoelDavid Hamkins, and Russell Miller (eds.), Cambridge: ASL and CambridgeUniversity Press, 150–163. doi:10.1017/CBO9781139028592.009
• Sieg, Wilfried, 1984, “Foundations forAnalysis and Proof Theory”,Synthese, 60(2):159–200. doi:10.1007/BF00485460
• –––, 1985, “Fragments ofArithmetic”,Annals of Pure and Applied Logic, 28:33–71. doi:10.1016/0168-0072(85)90030-2
• –––, 1988,“Hilbert’s Program Sixty Years Later”,TheJournal of Symbolic Logic, 53(2): 338–348.doi:10.1017/S0022481200028292
• –––, 1990, “Review of‘Friedman’s Research on Subsystems of Second OrderArithmetic’, by Stephen G. Simpson (Simpson 1985)”,The Journal of Symbolic Logic, 55(2): 870–874.doi:10.2307/2274673
• –––, 2020,“Methodological Frames: Paul Bernays, MathematicalStructuralism, and Proof Theory”, inThe Prehistory ofMathematical Structuralism (Logic and Computation in Philosophy),Erich H. Reck and Georg Schiemer (eds.), New York: Oxford UniversityPress, 352–382. doi:10.1093/oso/9780190641221.003.0014
• Sieg, Wilfried and Mark Ravaglia, 2005,“David Hilbert and Paul Bernays,Grundlagen dermathematik, First Edition (1934, 1939)”, inLandmarkWritings in Western Mathematics 1640–1940, IvorGrattan-Guinness, Roger Cooke, Leo Corry, Pierre Crépel, andNiccolo Guicciardini (eds.), Amsterdam: Elsevier, 981–999.doi:10.1016/B978-044450871-3/50158-3
• Sieg, Wilfried, Richard Sommer, and Carolyn L. Talcott (eds.),2002,Reflections on the Foundations of Mathematics: Essays inHonor of Solomon Feferman (Lecture Notes in Logic 15), Natick,MA: Association for Symbolic Logic and A. K. Peters.doi:10.1017/9781316755983
• Simpson, Stephen G., 1984, “Which setexistence axioms are needed to prove the Cauchy/Peano theorem forordinary differential equations?”,The Journal of SymbolicLogic, 49(3): 783–802. doi:10.2307/2274131
• –––, 1985,“Friedman’s Research on Subsystems of Second OrderArithmetic”, inHarvey Friedman’s Research on theFoundations of Mathematics (Studies in Logic and the Foundationsof Mathematics 117), Leo A. Harrington, Michael D. Morley, AndreScedrov, and Stephen G. Simpson (eds.), Amsterdam: North-Holland,137–159. doi:10.1016/S0049-237X(09)70158-2
• –––, 1988, “PartialRealizations of Hilbert’s Program”,The Journal ofSymbolic Logic, 53(2): 349–363.doi:10.1017/S0022481200028309
• –––, 1999,Subsystemsof Second Order Arithmetic (Perspectives in Mathematical Logic),Berlin/New York: Springer.
• –––, 2009,Subsystemsof Second Order Arithmetic (Perspectives in Logic), secondedition, Cambridge: Association for Symbolic Logic and CambridgeUniversity Press. doi:10.1017/cbo9780511581007
• –––, 2010, “TheGödel Hierarchy and Reverse Mathematics”, inKurtGödel, Essays for His Centennial (Lecture Notes in Logic33), Solomon Feferman, Charles Parsons, and Stephen G. Simpson (eds.),Cambridge: ASL and Cambridge University Press, 109–127.doi:10.1017/CBO9780511750762.008
• Skolem, Thoralf Albert, 1923,Begründung der elementaren arithmetik durch die rekurierendeDenkweise ohne anwendung scheinbarer veränderlichen mitunendlichem ausdehnungsbereich (Videnskabs-selskabet iChristiania. Skrifter. I. Mathematisk-naturvidenskabelig klasse 1923,no. 6), Kristiania: in kommision bei J. Dybwad.
• Solomon, Reed, 2001,“\(\Pi^1_1\text{-}\CA_0\) and Order Types of Countable OrderedGroups”,Journal of Symbolic Logic, 66(1):192–206. doi:10.2307/2694917
• Specker, Ernst, 1949, “Nichtkonstruktiv beweisbare Sätze der Analysis”,The Journalof Symbolic Logic, 14(3): 145–158. doi:10.2307/2267043
• –––, 1971,“Ramsey’s Theorem Does Not Hold in Recursive SetTheory”, inLogic Colloquium ’69. Proceedings of theSummer School and Colloquium in Mathematical Logic, Manchester, August1969 (Studies in Logic and the Foundations of Mathematics 61),Robin O. Gandy and C. M. E. Yates (eds.), Amsterdam: North-Holland,439–442. doi:10.1016/S0049-237X(08)71242-4
• Spector, Clifford, 1955, “RecursiveWell-Orderings”,The Journal of Symbolic Logic, 20(2):151–163. doi:10.2307/2266902
• Stillwell, John, 2018,ReverseMathematics: Proofs from the inside Out, Princeton/Oxford:Princeton University Press.
• Tait, William W., 1981, “Finitism”,The Journal of Philosophy, 78(9): 524–546.doi:10.2307/2026089
• –––, 2002, “Remarks onFinitism”, in Sieg, Sommer, and Talcott 2002: 410–419.doi:10.1017/9781316755983.020.
• Van Heijenoort, Jean (ed.), 1967,From Frege to Gödel: ASource Book in Mathematical Logic, 1879–1931 (Source Books inthe History of the Sciences), Cambridge, MA: Harvard UniversityPress.
• Veldman, Wim, 2009, “Brouwer’sApproximate Fixed-Point Theorem Is Equivalent to Brouwer’s FanTheorem”, inLogicism, Intuitionism, and Formalism: What HasBecome of Them? (Synthese Library: Volume 341), StenLindström, Erik Palmgren, Krister Segerberg, and ViggoStoltenberg-Hansen (eds.), Dordrecht: Springer, 277–299.doi:10.1007/978-1-4020-8926-8_14
• Veldman, Wim, 2014, “Brouwer’sFan Theorem as an Axiom and as a Contrast to Kleene’sAlternative”,Archive for Mathematical Logic,53(5–6): 621–693. doi:10.1007/s00153-014-0384-9
• Weyl, Hermann, 1918,Das Kontinuum:Kritische Untersuchungen über die Grundlagen der Analysis,Leipzig: Verlag von Veit.
• –––, 1987 [1994],TheContinuum: A Critical Examination of the Foundation of Analysis,Stephen Pollard and Thomas Bole (trans.), Kirksville, MO: ThomasJefferson University Press; reprinted with corrections Mineola, NY:Dover, 1994.
• Whitehead, Alfred North and BertrandRussell, 1910,Principia Mathematica, volume 1, Cambridge:Cambridge University Press.
• Zach, Richard, 1998, “Numbers andFunctions in Hilbert’s Finitism”,Taiwanese Journalfor Philosophy and History of Science, 10: 33–60.
• Zach, Richard, 2003, “The Practice ofFinitism: Epsilon Calculus and Consistency Proofs in Hilbert’sProgram”,Synthese, 137(1/2): 211–259.doi:10.1023/A:1026247421383
• Zermelo, Ernst, 1904, “Beweis,daß jede Menge wohlordnung werden kann (Aus einem an HerrnHilbert gerichteten Briefe)”,Mathematische Annalen,59(4): 514–516. doi:10.1007/BF01445300
• –––, 1908, “NeuerBeweis für die Möglichkeit einer Wohlordnung”,Mathematische Annalen, 65(1): 107–128. Translated inZermelo 1967. doi:10.1007/BF01450054
• –––, 1967, “A NewProof of the Possibility of a Well-Ordering”, in van Heijenoort1967: 183–198.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

• Diener, Hannes, 2020,Constructive Reverse Mathematics, unpublished manuscript, version of 4 April 2020, arXiv:1804.05495.
• The Reverse Mathematics Zoo, University of Connecticut
• Joosten, Joost, 2002,“Two Proofs of Parsons’ Theorem”, unpublished manuscript.
• Computability.org – A resource for computability theorists.

Related Entries

choice, axiom of |Church-Turing Thesis |computability and complexity |Dedekind, Richard: contributions to the foundations of mathematics |epsilon calculus |Frege, Gottlob: controversy with Hilbert |geometry: in the 19th century |Gödel, Kurt |Gödel, Kurt: incompleteness theorems |Hilbert, David: program in the foundations of mathematics |Leśniewski, Stanisław |logic, history of: intuitionistic logic |logic: classical |logic: intuitionistic |logic: second-order and higher-order |logicism and neologicism |mathematics, philosophy of: indispensability arguments in the |mathematics, philosophy of: intuitionism |mathematics, philosophy of: Platonism |mathematics, philosophy of: structuralism |mathematics: constructive |model theory: first-order |Poincaré, Henri |Principia Mathematica |Principia Mathematica: notation in |proof theory |proof theory: development of |recursive functions |Russell’s paradox |set theory |set theory: early development |type theory |Weyl, Hermann

Acknowledgments

The writing of this entry was informed by many valuable discussionswith Marianna Antonutti Marfori, Andy Arana, Walter Dean, MicDetlefsen, Damir Dzhafarov, Marta Fiori Carones, Martin Fischer,Volker Halbach, Leon Horsten, Hannes Leitgeb, Øystein Linnebo,Colin McLarty, Toby Meadows, Antonio Montalbán, Alberto Naibo,Carlo Nicolai, Marco Panza, Richard Pettigrew, Marcus Rossberg, SamSanders, Reed Solomon, Wilfried Sieg, Steve Simpson, Sean Walsh, andPhilip Welch. Particular thanks are due to Marianna Antonutti Marfori,Walter Dean, and an anonymous referee for their comments on earlierdrafts, along with the team at the Stanford Encyclopedia of Philosophyfor their inexhaustible patience and wonderful editorial support.