Inmathematical logic,second-order arithmetic is a collection ofaxiomatic systems that formalize thenatural numbers and theirsubsets. It is an alternative toaxiomatic set theory as afoundation for much, but not all, of mathematics.

A precursor to second-order arithmetic that involves third-order parameters was introduced byDavid Hilbert andPaul Bernays in their bookGrundlagen der Mathematik.^[1] The standard axiomatization of second-order arithmetic is denoted byZ₂.

Second-order arithmetic includes, but is significantly stronger than, itsfirst-order counterpartPeano arithmetic. Unlike Peano arithmetic, second-order arithmetic allowsquantification over sets of natural numbers as well as numbers themselves. Becausereal numbers can be represented as (infinite) sets of natural numbers in well-known ways, and because second-order arithmetic allows quantification over such sets, it is possible to formalize thereal numbers in second-order arithmetic. For this reason, second-order arithmetic is sometimes called "analysis".^[2]

Second-order arithmetic can also be seen as a weak version ofset theory in which every element is either a natural number or a set of natural numbers. Although it is much weaker thanZermelo–Fraenkel set theory, second-order arithmetic can prove essentially all of the results of classical mathematics expressible in its language.

Asubsystem of second-order arithmetic is atheory in the language of second-order arithmetic each axiom of which is a theorem of full second-order arithmetic (Z₂). Such subsystems are essential toreverse mathematics, a research program investigating how much of classical mathematics can be derived in certain weak subsystems of varying strength. Much of core mathematics can be formalized in these weak subsystems, some of which are defined below. Reverse mathematics also clarifies the extent and manner in which classical mathematics isnonconstructive.

The language of second-order arithmetic istwo-sorted. The first sort ofterms and in particularvariables, usually denoted by lower case letters, consists ofindividuals, whose intended interpretation is as natural numbers. The other sort of variables, variously called "set variables", "class variables", or even "predicates" are usually denoted by upper-case letters. They refer to classes/predicates/properties of individuals, and so can be thought of as sets of natural numbers. Both individuals and set variables can be quantifieduniversally orexistentially. A formula with nobound set variables (that is, no quantifiers over set variables) is calledarithmetical. An arithmetical formula may have free set variables and bound individual variables.

Individual terms are formed from the constant 0, the unary functionS (thesuccessor function), and the binary operations + and${\displaystyle \cdot }$ (addition and multiplication). The successor function adds 1 to its input. The relations = (equality) and < (comparison of natural numbers) relate two individuals, whereas the relation ∈ (membership) relates an individual and a set (or class). Thus in notation the language of second-order arithmetic is given by the signature.

For example,${\displaystyle \mathrm{\forall }n(n\in X\to Sn\in X)}$, is awell-formed formula of second-order arithmetic that is arithmetical, has one free set variableX and one bound individual variablen (but no bound set variables, as is required of an arithmetical formula)—whereas is a well-formed formula that is not arithmetical, having one bound set variableX and one bound individual variablen.

Several different interpretations of the quantifiers are possible. If second-order arithmetic is studied using the full semantics ofsecond-order logic then the set quantifiers range over all subsets of the range of the individual variables. If second-order arithmetic is formalized using the semantics offirst-order logic (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 fullpowerset of the domain of individual variables.^[3]

The following axioms are known as thebasic axioms, or sometimes theRobinson axioms. The resultingfirst-order theory, known asRobinson arithmetic, is essentiallyPeano arithmetic without induction. Thedomain of discourse for thequantified variables is thenatural numbers, collectively denoted byN, and including the distinguished member${\displaystyle 0}$, called "zero."

The primitive functions are the unarysuccessor function, denoted byprefix${\displaystyle S}$, and twobinary operations,addition andmultiplication, denoted by theinfix operator "+" and "${\displaystyle \cdot }$", respectively. There is also a primitivebinary relation calledorder, denoted by the infix operator "<".

Axioms governing thesuccessor function andzero:

1. ${\displaystyle \mathrm{\forall }m[Sm=0\to \mathrm{\perp }].}$ ("the successor of a natural number is never zero")
2. ${\displaystyle \mathrm{\forall }m\mathrm{\forall }n[Sm=Sn\to m=n].}$ ("the successor function isinjective")
3. ${\displaystyle \mathrm{\forall }n[0=n\vee \mathrm{\exists }m[Sm=n]].}$ ("every natural number is zero or a successor")

Addition definedrecursively:

4. ${\displaystyle \mathrm{\forall }m[m+0=m].}$
5. ${\displaystyle \mathrm{\forall }m\mathrm{\forall }n[m+Sn=S(m+n)].}$

Multiplication defined recursively:

6. ${\displaystyle \mathrm{\forall }m[m\cdot 0=0].}$
7. ${\displaystyle \mathrm{\forall }m\mathrm{\forall }n[m\cdot Sn=(m\cdot n)+m].}$

Axioms governing theorder relation "<":

8. ("no natural number is smaller than zero")
9. 
10. ("every natural number is zero or bigger than zero")
11. 

These axioms are allfirst-order statements. That is, all variables range over thenatural numbers and notsets thereof, a fact even stronger than their being arithmetical. Moreover, there is but oneexistential quantifier, in Axiom 3. Axioms 1 and 2, together with anaxiom schema of induction make up the usualPeano–Dedekind definition ofN. Adding to these axioms any sort ofaxiom schema of induction makes redundant the axioms 3, 10, and 11.

Ifφ(n) is a formula of second-order arithmetic with a free individual variablen and possibly other free individual or set variables (writtenm₁,...,m_k andX₁,...,X_l), theinduction axiom forφ is the axiom:

${\displaystyle \mathrm{\forall }{m}_1\dots m_k\mathrm{\forall }{X}_1\dots X_l((\phi (0)\wedge \mathrm{\forall }n(\phi (n)\to \phi (Sn)))\to \mathrm{\forall }n\phi (n))}$

The (full)second-order induction scheme consists of all instances of this axiom, over all second-order formulas.

One particularly important instance of the induction scheme is whenφ is the formula "${\displaystyle n\in X}$" expressing the fact thatn is a member ofX (X being a free set variable): in this case, the induction axiom forφ is

${\displaystyle \mathrm{\forall }X((0\in X\wedge \mathrm{\forall }n(n\in X\to Sn\in X))\to \mathrm{\forall }n(n\in X))}$

This sentence is called thesecond-order induction axiom.

Ifφ(n) is a formula with a free variablen and possibly other free variables, but not the variableZ, thecomprehension axiom forφ is the formula

${\displaystyle \mathrm{\exists }Z\mathrm{\forall }n(n\in Z\leftrightarrow \phi (n))}$

This axiom makes it possible to form the set${\displaystyle Z=\{n|\phi (n)\}}$ of natural numbers satisfyingφ(n). There is a technical restriction that the formulaφ may not contain the variableZ, for otherwise the formula${\displaystyle n\notin Z}$ would lead to the comprehension axiom

${\displaystyle \mathrm{\exists }Z\mathrm{\forall }n(n\in Z\leftrightarrow n\notin Z)}$,

which is inconsistent. This convention is assumed in the remainder of this article.

The formal theory ofsecond-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. This theory is sometimes calledfull second-order arithmetic to distinguish it from its subsystems, defined below. Because 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.^[3]

This section describes second-order arithmetic with first-order semantics. Thus amodel${\displaystyle \mathcal{M}}$ of the language of second-order arithmetic consists of a setM (which forms the range of individual variables) together with a constant 0 (an element ofM), a functionS fromM toM, two binary operations + and · onM, a binary relation < onM, and a collectionD of subsets ofM, which is the range of the set variables. OmittingD produces a model of the language of first-order arithmetic.

WhenD is the full powerset ofM, the model${\displaystyle \mathcal{M}}$ is called afull model. The use of full second-order semantics is equivalent to limiting the models of second-order arithmetic to the full models. In fact, the axioms of second-order arithmetic have only one full model. This follows from the fact that thePeano axioms with the second-order induction axiom have only one model under second-order semantics.

The first-order functions that are provablytotal in second-order arithmetic are precisely the same as those representable insystem F.^[4] Almost equivalently, system F is the theory of functionals corresponding to second-order arithmetic in a manner parallel to how Gödel'ssystem T corresponds to first-order arithmetic in theDialectica interpretation.

When a model of the language of second-order arithmetic has certain properties, it can also be called these other names:

• WhenM is the usual set of natural numbers with its usual operations,${\displaystyle \mathcal{M}}$ is called anω-model. In this case, the model may be identified withD, its collection of sets of naturals, because this set is enough to completely determine an ω-model. The unique full${\displaystyle \omega }$-model, which is the usual set of natural numbers with its usual structure and all its subsets, is called theintended orstandard model of second-order arithmetic.^[5]
• A model${\displaystyle \mathcal{M}}$ of the language of second-order arithmetic is called aβ-model if${\displaystyle \mathcal{M}{\prec }_1^1\mathcal{P}(\omega )}$, i.e. theΣ¹₁-statements with parameters from${\displaystyle \mathcal{M}}$ that are satisfied by${\displaystyle \mathcal{M}}$ are the same as those satisfied by the full model.^[6] Some notions that are absolute with respect to β-models include "${\displaystyle A\subseteq \omega \times \omega }$ encodes awell-order"^[7] and "${\displaystyle A\subseteq \omega \times \omega }$ is atree".^[6]
• The above result has been extended to the concept of aβ_n-model for${\displaystyle n\in \mathbb{N}}$, which has the same definition as the above except${\displaystyle {\prec }_1^1}$ is replaced by${\displaystyle {\prec }_n^1}$, i.e.${\displaystyle {\mathrm{\Sigma }}_1^1}$ is replaced by${\displaystyle {\mathrm{\Sigma }}_n^1}$.^[6] Using this definition β₀-models are the same as ω-models.^[8]

There are many named subsystems of second-order arithmetic.

A subscript 0 in the name of a subsystem indicates that it includes onlya restricted portion of the full second-order induction scheme.^[9] Such a restriction lowers theproof-theoretic strength of the system significantly. For example, the system ACA₀ described below isequiconsistent withPeano arithmetic. The corresponding theory ACA, consisting of ACA₀ plus the full second-order induction scheme, is stronger than Peano arithmetic.

Many of the well-studied subsystems are related to closure properties of models. For example, it can be shown that every ω-model of full second-order arithmetic is closed underTuring jump, but not every ω-model closed under Turing jump is a model of full second-order arithmetic. The subsystem ACA₀ includes just enough axioms to capture the notion of closure under Turing jump.

ACA₀ is defined as the theory consisting of the basic axioms, thearithmetical comprehension axiom scheme (in other words the comprehension axiom for everyarithmetical formulaφ) and the ordinary second-order induction axiom. It would be equivalent to also include the entire arithmetical induction axiom scheme, in other words to include the induction axiom for every arithmetical formulaφ.

It can be shown that a collectionS of subsets of ω determines an ω-model of ACA₀ if and only ifS is closed under Turing jump,Turing reducibility, and Turing join.^[10]

The subscript 0 in ACA₀ indicates that not every instance of the induction axiom scheme is included this subsystem. This makes no difference for ω-models, which automatically satisfy every instance of the induction axiom. It is of importance, however, in the study of non-ω-models. The system consisting of ACA₀ plus induction for all formulas is sometimes called ACA with no subscript.

The system ACA₀ is aconservative extension offirst-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). In particular it has the sameproof-theoretic ordinalε₀ as first-order arithmetic, owing to the limited induction schema.

A formula is calledbounded arithmetical, or Δ⁰₀, when all its quantifiers are of the form ∀n<t or ∃n<t (wheren is the individual variable being quantified andt is an individual term), where

stands for

and

stands for

.

A formula is called Σ⁰₁ (or sometimes Σ₁), respectively Π⁰₁ (or sometimes Π₁) when it is of the form ∃mφ, respectively ∀mφ whereφ is a bounded arithmetical formula andm is an individual variable (that is free inφ). More generally, a formula is called Σ⁰_n, respectively Π⁰_n when it is obtained by adding existential, respectively universal, individual quantifiers to a Π⁰_n−1, respectively Σ⁰_n−1 formula (and Σ⁰₀ and Π⁰₀ are both equal to Δ⁰₀). By construction, all these formulas are arithmetical (no class variables are ever bound) and, in fact, by putting the formula inSkolem prenex form one can see that every arithmetical formula is logically equivalent to a Σ⁰_n or Π⁰_n formula for all large enoughn.

The subsystem RCA₀ is a weaker system than ACA₀ and is often used as the base system inreverse mathematics. It consists of: the basic axioms, the Σ⁰₁ induction scheme, and the Δ⁰₁ comprehension scheme. The former term is clear: the Σ⁰₁ induction scheme is the induction axiom for every Σ⁰₁ formulaφ. The term "Δ⁰₁ comprehension" is more complex, because there is no such thing as a Δ⁰₁ formula. The Δ⁰₁ comprehension scheme instead asserts the comprehension axiom for every Σ⁰₁ formula that is logically equivalent to a Π⁰₁ formula. This scheme includes, for every Σ⁰₁ formulaφ and every Π⁰₁ formulaψ, the axiom:

${\displaystyle \mathrm{\forall }m\mathrm{\forall }X((\mathrm{\forall }n(\phi (n)\leftrightarrow \psi (n)))\to \mathrm{\exists }Z\mathrm{\forall }n(n\in Z\leftrightarrow \phi (n)))}$

The set of first-order consequences of RCA₀ is the same as those of the subsystem IΣ₁ of Peano arithmetic in which induction is restricted to Σ⁰₁ formulas. In turn, IΣ₁ is conservative overprimitive recursive arithmetic (PRA) for${\displaystyle {\mathrm{\Pi }}_2^0}$ sentences. Moreover, the proof-theoretic ordinal of${\displaystyle {\mathrm{R}\mathrm{C}\mathrm{A}}_0}$ is ω^ω, the same as that of PRA.

It can be seen that a collectionS of subsets of ω determines an ω-model of RCA₀ if and only ifSis closed under Turing reducibility and Turing join. In particular, the collection of allcomputable subsets of ω gives an ω-model of RCA₀. This is the motivation behind the name of this system—if a set can be proved to exist using RCA₀, then the set is recursive (i.e. computable).

Sometimes an even weaker system than RCA₀ is desired. One such system is defined as follows: one must first augment the language of arithmetic with anexponential 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 Δ⁰₁ comprehension, plus Δ⁰₀ induction.

Over ACA₀, each formula of second-order arithmetic is equivalent to a Σ¹_n or Π¹_n formula for all large enoughn. The systemΠ¹₁-comprehension is the system consisting of the basic axioms, plus the ordinary second-order induction axiom and the comprehension axiom for every (boldface^[11]) Π¹₁ formulaφ. This is equivalent to Σ¹₁-comprehension (on the other hand, Δ¹₁-comprehension, defined analogously to Δ⁰₁-comprehension, is weaker).

Projective determinacy is the assertion that every two-playerperfect information game with moves being natural numbers, game length ω andprojective payoff set is determined, that is, one of the players has a winning strategy. (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 Z₂.

Many natural propositions expressible in the language of second-order arithmetic are independent of Z₂ and evenZFC but are provable from projective determinacy. Examples include coanalyticperfect subset property, measurability and theproperty of Baire for${\displaystyle {\mathrm{\Sigma }}_2^1}$ sets,${\displaystyle {\mathrm{\Pi }}_3^1}$uniformization, etc. Over a weak base theory (such as RCA₀), projective determinacy implies comprehension and provides an essentially complete theory of second-order arithmetic — natural statements in the language of Z₂ that are independent of Z₂ with projective determinacy are hard to find.^[12]

ZFC + {there arenWoodin cardinals:n is a natural number} is conservative over Z₂ with projective determinacy^{[citation needed]}, that is a statement in the language of second-order arithmetic is provable in Z₂ with projective determinacy if and only if its translation into the language of set theory is provable in ZFC + {there aren Woodin cardinals:n∈N}.

Second-order arithmetic directly formalizes natural numbers and sets of natural numbers. However, it is able to formalize other mathematical objects indirectly via coding techniques, a fact that was first noticed byWeyl.^[13] Theintegers,rational numbers, andreal numbers can all be formalized in the subsystem RCA₀, along withcompleteseparablemetric spaces and continuous functions between them.^[14]

The research program ofreverse mathematics uses these formalizations of mathematics in second-order arithmetic to study the set-existence axioms required to prove mathematical theorems.^[15] For example, theintermediate value theorem for functions from the reals to the reals is provable in RCA₀,^[16] while theBolzano–Weierstrass theorem is equivalent to ACA₀ over RCA₀.^[17]

The aforementioned coding works well for continuous and total functions, assuming a higher-order base theory plusweak Kőnig's lemma.^[18] As perhaps expected, in the case oftopology, coding is not without problems.^[19]

• Paris–Harrington theorem
• Presburger arithmetic
• True arithmetic

• Burgess, J. P. (2005).Fixing Frege. Princeton University Press.
• Buss, S. R. (1998).Handbook of Proof Theory. Elsevier.ISBN 0-444-89840-9.
• Takeuti, G. (1975).Proof Theory.ISBN 0-444-10492-5.

• Formal theories of arithmetic

• Articles with short description
• Short description matches Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from July 2023