{"history":[],"article":{"id":"fb8743ad-f298-485e-9f43-f437689cad02","title":"Second-order arithmetic","slug":"second-order-arithmetic","content":":::summary\n:::\n\n# \nIn [mathematical logic](https://bliptext.com/articles/mathematical-logic), **second-order arithmetic** is a collection of [axiomatic](https://bliptext.com/articles/axiom) systems that formalize the [natural numbers](https://bliptext.com/articles/natural-number) and their [subsets](https://bliptext.com/articles/subset).\nIt is an alternative to [axiomatic set theory](https://bliptext.com/articles/axiomatic-set-theory) as a [foundation](https://bliptext.com/articles/foundation-of-mathematics) for much, but not all, of mathematics.\nA precursor to second-order arithmetic that involves third-order parameters was introduced by [David Hilbert](https://bliptext.com/articles/david-hilbert) and [Paul Bernays](https://bliptext.com/articles/paul-bernays) in their book [Grundlagen der Mathematik](https://bliptext.com/articles/grundlagen-der-mathematik).\nThe standard axiomatization of second-order arithmetic is denoted by **Z2**.\nSecond-order arithmetic includes, but is significantly stronger than, its [first-order](https://bliptext.com/articles/first-order-logic) counterpart [Peano arithmetic](https://bliptext.com/articles/peano-axioms).\nUnlike Peano arithmetic, second-order arithmetic allows [quantification](https://bliptext.com/articles/quantification-logic) over sets of natural numbers as well as numbers themselves.\nBecause [real numbers](https://bliptext.com/articles/real-number) can be represented as ([infinite](https://bliptext.com/articles/infinite-set)) sets of natural numbers in well-known ways, and because second-order arithmetic allows quantification over such sets, it is possible to formalize the [real numbers](https://bliptext.com/articles/real-number) in second-order arithmetic.\nFor this reason, second-order arithmetic is sometimes called \"[analysis](https://bliptext.com/articles/mathematical-analysis)\".\nSecond-order arithmetic can also be seen as a weak version of [set theory](https://bliptext.com/articles/set-theory) in which every element is either a natural number or a set of natural numbers.\nAlthough it is much weaker than [Zermelo–Fraenkel set theory](https://bliptext.com/articles/zermelo-fraenkel-set-theory), second-order arithmetic can prove essentially all of the results of classical mathematics expressible in its language.\nA **subsystem of second-order arithmetic** is a [theory](https://bliptext.com/articles/theory-logic) in the language of second-order arithmetic each axiom of which is a theorem of full second-order arithmetic (Z2).\nSuch subsystems are essential to [reverse mathematics](https://bliptext.com/articles/reverse-mathematics), a research program investigating how much of classical mathematics can be derived in certain weak subsystems of varying strength.\nMuch of core mathematics can be formalized in these weak subsystems, some of which are defined below.\nReverse mathematics also clarifies the extent and manner in which classical mathematics is [nonconstructive](https://bliptext.com/articles/nonconstructive).\n\n# Definition\n\n## Syntax\nThe language of second-order arithmetic is [two-sorted](https://bliptext.com/articles/many-sorted-logic).\nThe first sort of [terms](https://bliptext.com/articles/term-logic) and in particular [variables](https://bliptext.com/articles/variable-mathematics), usually denoted by lower case letters, consists of [individuals](https://bliptext.com/articles/individual), whose intended interpretation is as natural numbers.\nThe other sort of variables, variously called \"set variables\", \"class variables\", or even \"predicates\" are usually denoted by upper-case letters.\nThey refer to classes/predicates/properties of individuals, and so can be thought of as sets of natural numbers.\nBoth individuals and set variables can be quantified [universally](https://bliptext.com/articles/universal-quantification) or [existentially](https://bliptext.com/articles/existential-quantification).\nA formula with no [bound](https://bliptext.com/articles/bound-variable) set variables (that is, no quantifiers over set variables) is called **arithmetical**.\nAn arithmetical formula may have free set variables and bound individual variables.\nIndividual terms are formed from the constant 0, the unary function S (the [successor function](https://bliptext.com/articles/successor-function)), and the binary operations + and \\cdot (addition and multiplication).\nThe successor function adds 1 to its input.\nThe relations = (equality) and < (comparison of natural numbers) relate two individuals, whereas the relation ∈ (membership) relates an individual and a set (or class).\nThus in notation the language of second-order arithmetic is given by the signature.\nFor example,, is a [well-formed formula](https://bliptext.com/articles/well-formed-formula) of second-order arithmetic that is arithmetical, has one free set variable X and one bound individual variable n (but no bound set variables, as is required of an arithmetical formula)—whereas is a [well-formed formula](https://bliptext.com/articles/well-formed-formula) that is not arithmetical, having one bound set variable X and one bound individual variable n.\n\n## Semantics\nSeveral different interpretations of the quantifiers are possible.\nIf second-order arithmetic is studied using the full semantics of [second-order logic](https://bliptext.com/articles/second-order-logic) then the set quantifiers range over all subsets of the range of the individual variables.\nIf second-order arithmetic is formalized using the semantics of [first-order logic](https://bliptext.com/articles/first-order-logic) ([Henkin semantics](https://bliptext.com/articles/henkin-semantics)) then any model includes a domain for the set variables to range over, and this domain may be a proper subset of the full [powerset](https://bliptext.com/articles/powerset) of the domain of individual variables.\n\n## Axioms\n\n### Basic\nThe following axioms are known as the basic axioms, or sometimes the Robinson axioms. The resulting [first-order theory](https://bliptext.com/articles/first-order-theory), known as [Robinson arithmetic](https://bliptext.com/articles/robinson-arithmetic), is essentially [Peano arithmetic](https://bliptext.com/articles/peano-axioms) without induction.\nThe [domain of discourse](https://bliptext.com/articles/domain-of-discourse) for the [quantified variables](https://bliptext.com/articles/quantification-logic) is the [natural numbers](https://bliptext.com/articles/natural-number), collectively denoted by **N**, and including the distinguished member 0, called \"[zero](https://bliptext.com/articles/zero).\"\nThe primitive functions are the unary [successor function](https://bliptext.com/articles/successor-function), denoted by [prefix](https://bliptext.com/articles/prefix) S, and two [binary operations](https://bliptext.com/articles/binary-operation), [addition](https://bliptext.com/articles/addition) and [multiplication](https://bliptext.com/articles/multiplication), denoted by the [infix operator](https://bliptext.com/articles/infix-operator) \"+\" and \"\\cdot\", respectively.\nThere is also a primitive [binary relation](https://bliptext.com/articles/binary-relation) called [order](https://bliptext.com/articles/order-relation), denoted by the infix operator \"<\".\nAxioms governing the [successor function](https://bliptext.com/articles/successor-function) and [zero](https://bliptext.com/articles/zero):\n[Addition](https://bliptext.com/articles/addition) defined [recursively](https://bliptext.com/articles/recursion):\n[Multiplication](https://bliptext.com/articles/multiplication) defined recursively:\nAxioms governing the [order relation](https://bliptext.com/articles/order-relation) \"<\":\nThese axioms are all [first-order statements](https://bliptext.com/articles/first-order-logic).\nThat is, all variables range over the [natural numbers](https://bliptext.com/articles/natural-number) and not [sets](https://bliptext.com/articles/set-theory) thereof, a fact even stronger than their being arithmetical.\nMoreover, there is but one [existential quantifier](https://bliptext.com/articles/existential-quantifier), in Axiom 3.\nAxioms 1 and 2, together with an [axiom schema of induction](https://bliptext.com/articles/peano-axioms) make up the usual [Peano–Dedekind](https://bliptext.com/articles/peano-axioms) definition of **N**.\nAdding to these axioms any sort of [axiom schema of induction](https://bliptext.com/articles/peano-axioms) makes redundant the axioms 3, 10, and 11.\n\n### Induction and comprehension schema\nIf φ(n) is a formula of second-order arithmetic with a free individual variable n and possibly other free individual or set variables (written m1,...,mk and X1,...,Xl), the **induction axiom** for φ is the axiom:\nThe (**full**) **second-order induction scheme** consists of all instances of this axiom, over all second-order formulas.\nOne particularly important instance of the induction scheme is when φ is the formula \"n \\in X\" expressing the fact that n is a member of X (X being a free set variable): in this case, the induction axiom for φ is This sentence is called the **second-order induction axiom**.\nIf φ(n) is a formula with a free variable n and possibly other free variables, but not the variable Z, the **[comprehension axiom](https://bliptext.com/articles/comprehension-axiom)** for φ is the formula\nThis axiom makes it possible to form the set of natural numbers satisfying φ(n).\nThere is a technical restriction that the formula φ may not contain the variable Z, for otherwise the formula would lead to the comprehension axiom\nwhich is inconsistent.\nThis convention is assumed in the remainder of this article.\n\n## The full system\nThe formal theory of **second-order arithmetic** (in the language of **second-order arithmetic**) consists of the basic axioms, the comprehension axiom for every formula φ (arithmetic or otherwise), and the second-order induction axiom.\nThis theory is sometimes called full second-order arithmetic to distinguish it from its subsystems, defined below.\nBecause full second-order semantics imply that every possible set exists, the comprehension axioms may be taken to be part of the deductive system when full second-order semantics is employed.\n\n# Models\nThis section describes second-order arithmetic with first-order semantics.\nThus a **model** \\mathcal{M} of the language of second-order arithmetic consists of a set M (which forms the range of individual variables) together with a constant 0 (an element of M), a function S from M to M, two binary operations + and · on M, a binary relation < on M, and a collection D of subsets of M, which is the range of the set variables.\nOmitting D produces a model of the language of first-order arithmetic.\nWhen D is the full powerset of M, the model \\mathcal{M} is called a **full model**.\nThe use of full second-order semantics is equivalent to limiting the models of second-order arithmetic to the full models.\nIn fact, the axioms of second-order arithmetic have only one full model.\nThis follows from the fact that the [Peano axioms](https://bliptext.com/articles/peano-axioms) with the second-order induction axiom have only one model under second-order semantics.\n\n## Definable functions\nThe first-order functions that are provably [total](https://bliptext.com/articles/total-function) in second-order arithmetic are precisely the same as those representable in [system F](https://bliptext.com/articles/system-f).\nAlmost equivalently, system F is the theory of functionals corresponding to second-order arithmetic in a manner parallel to how Gödel's [system T](https://bliptext.com/articles/dialectica-interpretation) corresponds to first-order arithmetic in the [Dialectica interpretation](https://bliptext.com/articles/dialectica-interpretation).\n\n## More types of models\nWhen a model of the language of second-order arithmetic has certain properties, it can also be called these other names:\n\n# Subsystems\nThere are many named subsystems of second-order arithmetic.\nA subscript 0 in the name of a subsystem indicates that it includes only\na restricted portion of the full second-order induction scheme.\nSuch a restriction lowers the [proof-theoretic strength](https://bliptext.com/articles/proof-theoretic-strength) of the system significantly.\nFor example, the system ACA0 described below is [equiconsistent](https://bliptext.com/articles/equiconsistency) with [Peano arithmetic](https://bliptext.com/articles/peano-arithmetic).\nThe corresponding theory ACA, consisting of ACA0 plus the full second-order induction scheme, is stronger than Peano arithmetic.\n\n## Arithmetical comprehension\nMany of the well-studied subsystems are related to closure properties of models.\nFor example, it can be shown that every ω-model of full second-order arithmetic is closed under [Turing jump](https://bliptext.com/articles/turing-jump), but not every ω-model closed under [Turing jump](https://bliptext.com/articles/turing-jump) is a model of full second-order arithmetic.\nThe subsystem ACA0 includes just enough axioms to capture the notion of closure under Turing jump.\nACA0 is defined as the theory consisting of the basic axioms, the **arithmetical comprehension axiom** scheme (in other words the comprehension axiom for every arithmetical formula φ) and the ordinary second-order induction axiom.\nIt would be equivalent to also include the entire arithmetical induction axiom scheme, in other words to include the induction axiom for every arithmetical formula φ.\nIt can be shown that a collection S of subsets of ω determines an ω-model of ACA0 if and only if S is closed under Turing jump, [Turing reducibility](https://bliptext.com/articles/turing-reducibility), and Turing join.\nThe subscript 0 in ACA0 indicates that not every instance of the induction axiom scheme is included this subsystem.\nThis makes no difference for ω-models, which automatically satisfy every instance of the induction axiom.\nIt is of importance, however, in the study of non-ω-models.\nThe system consisting of ACA0 plus induction for all formulas is sometimes called ACA with no subscript.\nThe system ACA0 is a [conservative extension](https://bliptext.com/articles/conservative-extension) of **first-order arithmetic** (or first-order Peano axioms), defined as the basic axioms, plus the first-order induction axiom scheme (for all formulas φ involving no class variables at all, bound or otherwise), in the language of **first-order arithmetic** (which does not permit class variables at all).\nIn particular it has the same [proof-theoretic ordinal](https://bliptext.com/articles/ordinal-analysis) [ε0](https://bliptext.com/articles/epsilon-number) as first-order arithmetic, owing to the limited induction schema.\n\n## The arithmetical hierarchy for formulas\nA formula is called bounded arithmetical, or Δ0_{0, when all its quantifiers are of the form ∀n1 (or sometimes Σ1), respectively Π0_{1 (or sometimes Π1) when it is of the form ∃mundefinedφ, respectively ∀mundefinedφ where φ is a bounded arithmetical formula and m is an individual variable (that is free in φ).\nMore generally, a formula is called Σ0_{n, respectively Π0_{n when it is obtained by adding existential, respectively universal, individual quantifiers to a Π0_{n−1 , respectively Σ0_{n−1 formula (and Σ0_{0 and Π0_{0 are both equal to Δ0_{0 ).\nBy construction, all these formulas are arithmetical (no class variables are ever bound) and, in fact, by putting the formula in [Skolem prenex form](https://bliptext.com/articles/skolem-prenex-form) one can see that every arithmetical formula is logically equivalent to a Σ0_{n or Π0_{n formula for all large enough n.\n\n## Recursive comprehension\nThe subsystem RCA0 is a weaker system than ACA0 and is often used as the base system in [reverse mathematics](https://bliptext.com/articles/reverse-mathematics).\nIt consists of: the basic axioms, the Σ0_{1 induction scheme, and the Δ0_{1 comprehension scheme.\nThe former term is clear: the Σ0_{1 induction scheme is the induction axiom for every Σ0_{1 formula φ.\nThe term \"Δ0_{1 comprehension\" is more complex, because there is no such thing as a Δ0_{1 formula.\nThe Δ0_{1 comprehension scheme instead asserts the comprehension axiom for every Σ0_{1 formula that is logically equivalent to a Π0_{1 formula.\nThis scheme includes, for every Σ0_{1 formula φ and every Π0_{1 formula ψ, the axiom:\nThe set of first-order consequences of RCA0 is the same as those of the subsystem IΣ1 of Peano arithmetic in which induction is restricted to Σ0_{1 formulas.\nIn turn, IΣ1 is conservative over [primitive recursive arithmetic](https://bliptext.com/articles/primitive-recursive-arithmetic) (PRA) for \\Pi^0_2 sentences.\nMoreover, the proof-theoretic ordinal of is ωω, the same as that of PRA.\nIt can be seen that a collection S of subsets of ω determines an ω-model of RCA0 if and only if S is closed under Turing reducibility and Turing join.\nIn particular, the collection of all [computable subsets](https://bliptext.com/articles/computable-set) of ω gives an ω-model of RCA0.\nThis is the motivation behind the name of this system—if a set can be proved to exist using RCA0, then the set is recursive (i.e. computable).\n\n## Weaker systems\nSometimes an even weaker system than RCA0 is desired.\nOne such system is defined as follows: one must first augment the language of arithmetic with an [exponential function](https://bliptext.com/articles/exponential-function) symbol (in stronger systems the exponential can be defined in terms of addition and multiplication by the usual trick, but when the system becomes too weak this is no longer possible) and the basic axioms by the obvious axioms defining exponentiation inductively from multiplication; then the system consists of the (enriched) basic axioms, plus Δ0_{1 comprehension, plus Δ0_{0 induction.\n\n## Stronger systems\nOver ACA0, each formula of second-order arithmetic is equivalent to a Σ1_{n or Π1_{n formula for all large enough n.\nThe system **Π1_{1 -comprehension** is the system consisting of the basic axioms, plus the ordinary second-order induction axiom and the comprehension axiom for every ([boldface](https://bliptext.com/articles/boldface-mathematics)) Π1_{1 formula φ.\nThis is equivalent to Σ1_{1 -comprehension (on the other hand, Δ1_{1 -comprehension, defined analogously to Δ0_{1 -comprehension, is weaker).\n\n# Projective determinacy\n[Projective determinacy](https://bliptext.com/articles/[projective](https://bliptext.com/articles/projective-set)-determinacy) is the assertion that every two-player perfect information game with moves being natural numbers, game length ω and [projective](https://bliptext.com/articles/projective-set) payoff set is determined, that is, one of the players has a winning strategy.\n(The first player wins the game if the play belongs to the payoff set; otherwise, the second player wins.) A set is projective if and only if (as a predicate) it is expressible by a formula in the language of second-order arithmetic, allowing real numbers as parameters, so projective determinacy is expressible as a schema in the language of Z2.\nMany natural propositions expressible in the language of second-order arithmetic are independent of Z2 and even [ZFC](https://bliptext.com/articles/zfc) but are provable from projective determinacy.\nExamples include coanalytic [perfect subset property](https://bliptext.com/articles/perfect-set-property), measurability and the [property of Baire](https://bliptext.com/articles/property-of-baire) for \\Sigma^1_2 sets, \\Pi^1_3 [uniformization](https://bliptext.com/articles/uniformization-set-theory), etc. Over a weak base theory (such as RCA0), projective determinacy implies comprehension and provides an essentially complete theory of second-order arithmetic — natural statements in the language of Z2 that are independent of Z2 with projective determinacy are hard to find.\nZFC + {there are n [Woodin cardinals](https://bliptext.com/articles/woodin-cardinal): n is a natural number} is conservative over Z2 with projective determinacy, that is a statement in the language of second-order arithmetic is provable in Z2 with projective determinacy if and only if its translation into the language of set theory is provable in ZFC + {there are n [Woodin cardinals](https://bliptext.com/articles/woodin-cardinal): n∈N}.\n\n# Coding mathematics\nSecond-order arithmetic directly formalizes natural numbers and sets of natural numbers.\nHowever, it is able to formalize other mathematical objects indirectly via coding techniques, a fact that was first noticed by [Weyl](https://bliptext.com/articles/hermann-weyl).\nThe [integers](https://bliptext.com/articles/integer), [rational numbers](https://bliptext.com/articles/rational-number), and [real numbers](https://bliptext.com/articles/real-number) can all be formalized in the subsystem RCA0, along with [complete](https://bliptext.com/articles/complete-metric-space) [separable](https://bliptext.com/articles/separable-space) [metric spaces](https://bliptext.com/articles/metric-space) and continuous functions between them.\nThe research program of [reverse mathematics](https://bliptext.com/articles/reverse-mathematics) uses these formalizations of mathematics in second-order arithmetic to study the set-existence axioms required to prove mathematical theorems.\nFor example, the [intermediate value theorem](https://bliptext.com/articles/intermediate-value-theorem) for functions from the reals to the reals is provable in RCA0, while the Bolzano**–**Weierstrass theorem is equivalent to ACA0 over RCA0.\nThe aforementioned coding works well for continuous and total functions, assuming a higher-order base theory plus [weak Kőnig's lemma](https://bliptext.com/articles/k-nig-s-lemma).\nAs perhaps expected, in the case of [topology](https://bliptext.com/articles/topology), coding is not without problems.","current_revision":null,"created_by":"kACnuQmH5k9Nr5VNVEpVeg7XpvUmMctD","created_at":"2025-01-26T06:58:36.604Z","updated_at":"2025-01-26T06:58:36.604Z","search_vector":"'arithmet':4 'order':3 'second':2 'second-ord':1","search_content":" \n \n\n# \nIn [mathematical logic](https://bliptext.com/articles/mathematical-logic), **second-order arithmetic** is a collection of [axiomatic](https://bliptext.com/articles/axiom) systems that formalize the [natural numbers](https://bliptext.com/articles/natural-number) and their [subsets](https://bliptext.com/articles/subset).\nIt is an alternative to [axiomatic set theory](https://bliptext.com/articles/axiomatic-set-theory) as a [foundation](https://bliptext.com/articles/foundation-of-mathematics) for much, but not all, of mathematics.\nA precursor to second-order arithmetic that involves third-order parameters was introduced by [David Hilbert](https://bliptext.com/articles/david-hilbert) and [Paul Bernays](https://bliptext.com/articles/paul-bernays) in their book [Grundlagen der Mathematik](https://bliptext.com/articles/grundlagen-der-mathematik).\nThe standard axiomatization of second-order arithmetic is denoted by **Z2**.\nSecond-order arithmetic includes, but is significantly stronger than, its [first-order](https://bliptext.com/articles/first-order-logic) counterpart [Peano arithmetic](https://bliptext.com/articles/peano-axioms).\nUnlike Peano arithmetic, second-order arithmetic allows [quantification](https://bliptext.com/articles/quantification-logic) over sets of natural numbers as well as numbers themselves.\nBecause [[real numbers](https://bliptext.com/articles/real-number)](https://bliptext.com/articles/real-number) can be represented as ([infinite](https://bliptext.com/articles/infinite-set)) sets of natural numbers in well-known ways, and because second-order arithmetic allows quantification over such sets, it is possible to formalize the [[real numbers](https://bliptext.com/articles/real-number)](https://bliptext.com/articles/real-number) in second-order arithmetic.\nFor this reason, second-order arithmetic is sometimes called \"[analysis](https://bliptext.com/articles/mathematical-analysis)\".\nSecond-order arithmetic can also be seen as a weak version of [set theory](https://bliptext.com/articles/set-theory) in which every element is either a natural number or a set of natural numbers.\nAlthough it is much weaker than [Zermelo–Fraenkel set theory](https://bliptext.com/articles/zermelo-fraenkel-set-theory), second-order arithmetic can prove essentially all of the results of classical mathematics expressible in its language.\nA **subsystem of second-order arithmetic** is a [theory](https://bliptext.com/articles/theory-logic) in the language of second-order arithmetic each axiom of which is a theorem of full second-order arithmetic (Z2).\nSuch subsystems are essential to [reverse mathematics](https://bliptext.com/articles/reverse-mathematics), a research program investigating how much of classical mathematics can be derived in certain weak subsystems of varying strength.\nMuch of core mathematics can be formalized in these weak subsystems, some of which are defined below.\nReverse mathematics also clarifies the extent and manner in which classical mathematics is [nonconstructive](https://bliptext.com/articles/nonconstructive).\n\n# Definition\n\n## Syntax\nThe language of second-order arithmetic is [two-sorted](https://bliptext.com/articles/many-sorted-logic).\nThe first sort of [terms](https://bliptext.com/articles/term-logic) and in particular [variables](https://bliptext.com/articles/variable-mathematics), usually denoted by lower case letters, consists of [individuals](https://bliptext.com/articles/individual), whose intended interpretation is as natural numbers.\nThe other sort of variables, variously called \"set variables\", \"class variables\", or even \"predicates\" are usually denoted by upper-case letters.\nThey refer to classes/predicates/properties of individuals, and so can be thought of as sets of natural numbers.\nBoth individuals and set variables can be quantified [universally](https://bliptext.com/articles/universal-quantification) or [existentially](https://bliptext.com/articles/existential-quantification).\nA formula with no [bound](https://bliptext.com/articles/bound-variable) set variables (that is, no quantifiers over set variables) is called **arithmetical**.\nAn arithmetical formula may have free set variables and bound individual variables.\nIndividual terms are formed from the constant 0, the unary function S (the [successor function](https://bliptext.com/articles/successor-function)), and the binary operations + and \\cdot (addition and multiplication).\nThe successor function adds 1 to its input.\nThe relations = (equality) and 0, when all its quantifiers are of the form ∀n 1 (or sometimes Σ1), respectively Π0 1 (or sometimes Π1) when it is of the form ∃mundefinedφ, respectively ∀mundefinedφ where φ is a bounded arithmetical formula and m is an individual variable (that is free in φ).\nMore generally, a formula is called Σ0 n, respectively Π0 n when it is obtained by adding existential, respectively universal, individual quantifiers to a Π0 n−1 , respectively Σ0 n−1 formula (and Σ0 0 and Π0 0 are both equal to Δ0 0 ).\nBy construction, all these formulas are arithmetical (no class variables are ever bound) and, in fact, by putting the formula in [Skolem prenex form](https://bliptext.com/articles/skolem-prenex-form) one can see that every arithmetical formula is logically equivalent to a Σ0 n or Π0 n formula for all large enough n.\n\n## Recursive comprehension\nThe subsystem RCA0 is a weaker system than ACA0 and is often used as the base system in [reverse mathematics](https://bliptext.com/articles/reverse-mathematics).\nIt consists of: the basic axioms, the Σ0 1 induction scheme, and the Δ0 1 comprehension scheme.\nThe former term is clear: the Σ0 1 induction scheme is the induction axiom for every Σ0 1 formula φ.\nThe term \"Δ0 1 comprehension\" is more complex, because there is no such thing as a Δ0 1 formula.\nThe Δ0 1 comprehension scheme instead asserts the comprehension axiom for every Σ0 1 formula that is logically equivalent to a Π0 1 formula.\nThis scheme includes, for every Σ0 1 formula φ and every Π0 1 formula ψ, the axiom:\nThe set of first-order consequences of RCA0 is the same as those of the subsystem IΣ1 of Peano arithmetic in which induction is restricted to Σ0 1 formulas.\nIn turn, IΣ1 is conservative over [primitive recursive arithmetic](https://bliptext.com/articles/primitive-recursive-arithmetic) (PRA) for \\Pi^0_2 sentences.\nMoreover, the proof-theoretic ordinal of is ωω, the same as that of PRA.\nIt can be seen that a collection S of subsets of ω determines an ω-model of RCA0 if and only if S is closed under Turing reducibility and Turing join.\nIn particular, the collection of all [computable subsets](https://bliptext.com/articles/computable-set) of ω gives an ω-model of RCA0.\nThis is the motivation behind the name of this system—if a set can be proved to exist using RCA0, then the set is recursive (i.e. computable).\n\n## Weaker systems\nSometimes an even weaker system than RCA0 is desired.\nOne such system is defined as follows: one must first augment the language of arithmetic with an [exponential function](https://bliptext.com/articles/exponential-function) symbol (in stronger systems the exponential can be defined in terms of addition and multiplication by the usual trick, but when the system becomes too weak this is no longer possible) and the basic axioms by the obvious axioms defining exponentiation inductively from multiplication; then the system consists of the (enriched) basic axioms, plus Δ0 1 comprehension, plus Δ0 0 induction.\n\n## Stronger systems\nOver ACA0, each formula of second-order arithmetic is equivalent to a Σ1 n or Π1 n formula for all large enough n.\nThe system **Π1 1 -comprehension** is the system consisting of the basic axioms, plus the ordinary second-order induction axiom and the comprehension axiom for every ([boldface](https://bliptext.com/articles/boldface-mathematics)) Π1 1 formula φ.\nThis is equivalent to Σ1 1 -comprehension (on the other hand, Δ1 1 -comprehension, defined analogously to Δ0 1 -comprehension, is weaker).\n\n# Projective determinacy\n[Projective determinacy](https://bliptext.com/articles/[projective](https://bliptext.com/articles/projective-set)-determinacy) is the assertion that every two-player perfect information game with moves being natural numbers, game length ω and [projective](https://bliptext.com/articles/projective-set) payoff set is determined, that is, one of the players has a winning strategy.\n(The first player wins the game if the play belongs to the payoff set; otherwise, the second player wins.) A set is projective if and only if (as a predicate) it is expressible by a formula in the language of second-order arithmetic, allowing real numbers as parameters, so projective determinacy is expressible as a schema in the language of Z2.\nMany natural propositions expressible in the language of second-order arithmetic are independent of Z2 and even [ZFC](https://bliptext.com/articles/zfc) but are provable from projective determinacy.\nExamples include coanalytic [perfect subset property](https://bliptext.com/articles/perfect-set-property), measurability and the [property of Baire](https://bliptext.com/articles/property-of-baire) for \\Sigma^1_2 sets, \\Pi^1_3 [uniformization](https://bliptext.com/articles/uniformization-set-theory), etc. Over a weak base theory (such as RCA0), projective determinacy implies comprehension and provides an essentially complete theory of second-order arithmetic — natural statements in the language of Z2 that are independent of Z2 with projective determinacy are hard to find.\nZFC + {there are n [Woodin cardinals](https://bliptext.com/articles/woodin-cardinal): n is a natural number} is conservative over Z2 with projective determinacy, that is a statement in the language of second-order arithmetic is provable in Z2 with projective determinacy if and only if its translation into the language of set theory is provable in ZFC + {there are n [Woodin cardinals](https://bliptext.com/articles/woodin-cardinal): n∈N}.\n\n# Coding mathematics\nSecond-order arithmetic directly formalizes natural numbers and sets of natural numbers.\nHowever, it is able to formalize other mathematical objects indirectly via coding techniques, a fact that was first noticed by [Weyl](https://bliptext.com/articles/hermann-weyl).\nThe [integers](https://bliptext.com/articles/integer), [rational numbers](https://bliptext.com/articles/rational-number), and [real numbers](https://bliptext.com/articles/real-number) can all be formalized in the subsystem RCA0, along with [complete](https://bliptext.com/articles/complete-metric-space) [separable](https://bliptext.com/articles/separable-space) [metric spaces](https://bliptext.com/articles/metric-space) and continuous functions between them.\nThe research program of [reverse mathematics](https://bliptext.com/articles/reverse-mathematics) uses these formalizations of mathematics in second-order arithmetic to study the set-existence axioms required to prove mathematical theorems.\nFor example, the [intermediate value theorem](https://bliptext.com/articles/intermediate-value-theorem) for functions from the reals to the reals is provable in RCA0, while the Bolzano**–**Weierstrass theorem is equivalent to ACA0 over RCA0.\nThe aforementioned coding works well for continuous and total functions, assuming a higher-order base theory plus [weak Kőnig's lemma](https://bliptext.com/articles/k-nig-s-lemma).\nAs perhaps expected, in the case of [topology](https://bliptext.com/articles/topology), coding is not without problems.","revisionCount":0},"hasMore":false,"nextCursor":null}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}

History