**Second-order arithmetic** (also known as **Z _{2}** or as \(\Pi_\infty^1-CA\)) is a first-order theory of arithmetic allowing quantification over the natural numbers as well as

*sets*of natural numbers.

## Language

The **language of second-order arithmetic**, **L _{2}**, allows us to discuss two types of objects, namely numbers themselves, or sets of numbers. It is an extension of predicate calculus with the following:

- Infinitely many numeric variables \(x_0\), \(x_1\), ... and infinitely many set variables \(X_0\), \(X_1\), ...
- Constant symbol \(0\), called zero
- Three binary relation symbols \(=,<,\in\), called equality, comparison and set membership. The first two are relations between numbers, and the last one is a relation between a number and a set
- Unary function symbol \(S(x)\), called successor, mapping numbers to numbers
- Two binary function symbols, \(+(a,b),\cdot(a,b)\), called addition and multiplication respectively, which map pairs of numbers to a single number. They are often denoted by \(a+b,a\cdot b\).

The language of second-order arithmetic is expressive enough to allow us to talk about not only natural numbers and subsets of these, but also about integers, rational numbers and real numbers, and even countable sets (i.e. sequences) of real numbers.

## Axioms

The theory of second-order arithmetic consists of the axioms of Peano arithmetic, plus:

- \(\forall X (0 \in X \wedge \forall x (x \in X \Rightarrow Sx \in X) \Rightarrow \forall x : x \in X)\), the second-order induction axiom. It states that if a set contains 0 and contains the successor of each of its own members, then that set contains all natural numbers.
- For every formula \(\phi\) where \(X\) is not a free variable: \(\exists X \forall x (x \in X \Leftrightarrow \phi(x))\), the axiom schema of comprehension. It tells us that every predicate over the natural numbers defines a subset of the natural numbers (namely the set of these number which satisfy \(\phi\)).

## Subsystems

Z_{2} is an extremely strong formal theory, and in many cases we do not require all of its strength to prove a desired result. We naturally ask what happens when we *weaken* Z_{2}. Harvey Friedman started a project, now known as reverse mathematics, that addresses questions about what axioms are necessary to prove a given theorem, and what axioms are not strong enough to prove it.

Reverse mathematics focuses on subsystems of second-order arithmetic, which have been extensively studied to measure strength of their theorems. The "Big Five" are RCA_{0}, WKL_{0}, ACA_{0}, ATR_{0}, and \(\Pi_1^1-CA_0\). Each member of the Big Five is a proper extension of the preceding ones. All theorems seen in professional mathematics about the integers, real numbers, and complex numbers, with the exception of a small minority, can be assigned a "strength" based on the weakest member of the Big Five required to prove them. Many of them can be proven in just RCA_{0}.

These subsystems still use the *language* of second-order arithmetic, but not necessarily its axioms. Although some of these theories may be intuitively weaker than Peano arithmetic, unlike PA, they are all able to make statements about the real numbers.

### RCA_{0}

RCA_{0}, for "recursive comprehension axiom," is the weakest of the Big Five. It consists of:

- Robinson arithmetic
- First-order schema of induction limited to \(\Sigma_1^0\) formulas (see arithmetical hierarchy)
- Axiom schema of comprehension, limited to \(\Delta_1^0\) formulas

This is the so-called *base system*, and all other subsystems have RCA_{0}'s axioms. RCA_{0} is a weak system, but it can prove many basic properties of natural numbers and real numbers, including the uniqueness of a limit of a sequence and the intermediate value theorem). RCA_{0} can prove most "everyday" properties of natural numbers and real numbers.

RCA_{0} only has enough strength to prove the existence of objects which are recursive. For example, the set existence axioms of this theory lack the strength to prove the existence of uncomputable functions.

RCA_{0} has a proof-theoretic ordinal of \(\omega^\omega\).

### WKL_{0}

WKL_{0} stands for "weak König's lemma." We form WKL_{0} by extending RCA_{0} with a weak form of König's lemma:

- Let \(2^{<\omega}\) be the tree of all finite binary sequences, and let \(T\) be one of its infinite subtrees. Then \(T\) has an infinite branch.

RCA_{0} cannot prove this lemma — recalling that RCA_{0} cannot prove the existence of uncomputable sets, we can create an infinite computable tree \(T\) which has no computable infinite branches. Consequently, WKL_{0} is a proper extension of RCA_{0}.

It can be shown that many natural statements are equivalent (over base theory RCA_{0}) to WKL_{0}, e.g. Heine-Borel theorem for closed intervals, or Riemann-integrability of continuous functions. One of the most important equivalent statements is \(\Sigma^0_1\) separation: given two \(\Sigma^0_1\) sentences with a free variable \(n\), never both true, there is a set which contains all \(n\) which make first formula true, and none which make second one true.

WKL_{0} has a proof-theoretic ordinal of \(\omega^\omega\) and has the same *consistency strength* than RCA_{0}, i.e. they are equiconsistent.

### ACA_{0}

Arithmetical comprehension axiom. We get this by adjoining to RCA_{0} axiom schema of comprehension for all arithmetical formulas (ones contained in \(\Sigma_n^0\) for some \(n\in\Bbb N\)). It can be shown that formulas provable in ACA_{0} which can be expressed in *first*-order arithmetic are precisely the formulas provable by Peano arithmetic (one says that ACA_{0} is *conservative* over Peano arithmetic for arithmetical sentences). Like before, it can be shown that ACA_{0} is a proper extension of WKL_{0}, although the proof in this case is not as simple.

ACA_{0} is strong enough to prove all the statements required to work well with real (or complex) analysis, including Bolzano-Weierstrass theorem or full König's lemma (for trees on finite sequences of natural numbers) (in fact, ACA_{0} is provably equivalent to these two statements).

ACA_{0} has a proof-theoretic ordinal of ε₀.

### ATR_{0}

This one stands for "arithmetical transfinite recursion". This system is ACA_{0} together with axiom schema stating, intuitively, that if we have countable well-ordering (coded in a certain way) and so called arithmetical functional, we can iterate application of this functional transfinitely by following the mentioned well-ordering. This means that certain set constructions can be accomplished by iterating a simple construction transfinite number of times.

Addition of this axiom schema makes it possible to build a theory of ordinal numbers in second-order arithmetic. An example of strength of this schema is that it's sufficient to prove the consistency of ACA_{0}, which means that it is significantly stronger than ACA_{0} (see Gödel's incompleteness theorems).

Important single theorem which is equivalent (over RCA_{0}) to ATR_{0} is that every two countable well-orderings are comparable, so that ordinal numbers form a linear order.

Another important schema equivalent to ATR_{0} is \(\Sigma^1_1\) separation: given two \(\Sigma^1_1\) sentences (see analytical hierarchy) with free variable \(n\), never both true, there is a set which contains all \(n\) which make first formula true, and none which make second one true.

The proof-theoretic ordinal of ATR_{0} is the Feferman–Schütte ordinal.

### \(\Pi_1^1-CA_0\)

The last, and the strongest system in the big five is RCA_{0} extended by \(\Pi_1^1\) comprehension axiom schema, hence the abbreviation. This is so called impredicative system, because it's axioms, in a way, assert existence of objects which depend on the object defined (this is because defining set \(X\) using \(\Pi_1^1\) formula involves statement which is supposed to hold for *all* sets, including \(X\) itself).

It's clear that \(\Pi_1^1-CA_0\) contains all the axioms of ACA_{0}, and it can be shown that it also proves all instances of ATR_{0} axioms, which shows that \(\Pi_1^1-CA_0\) can build basic theory of ordinal numbers. However, as one can show, statement that given order is well-order is a \(\Pi_1^1\) statement, which means that this last system can show existence of sets definitions of which explicitly use notions of well-ordering, which, in big part, is where the strength of the system comes from.

The proof-theoretic ordinal of \(\Pi_1^1-CA_0\) is Ψ_{0}(Ω_{ω}).

### Other subsystems

Apart from the Big Five, many subsystems of Z_{2} have been analysed. Below is the list of more noteworthy ones.

- RCA, WKL, etc. - these are extensions of corresponding systems RCA
_{0}, WKL_{0}, etc. resulting by addition of first-order induction schema for*all*formulas in language of second-order arithmetic. Indicator of whether this full axiom schema appears in subsystem or not is 0 in the subscript. - \(\Sigma_m^n-IND\), \(\Pi_m^n-IND\), \(\Delta_m^n-IND\) - these are schemas of first-order induction limited to \(\Sigma_m^n\), \(\Pi_m^n\), \(\Delta_m^n\) formulas respectively (here and below \(n\) is 0 or 1). Additionally, \(\Pi_\infty^1-IND\) is conjunction of all of these schemas.
- \(\Sigma_m^n-TI\), \(\Pi_m^n-TI\), \(\Delta_m^n-TI\) - these are schemas of transfinite induction limited to formulas in respective classes. This means that for every formula \(\psi(n)\) of respective complexity and any well-ordering of natural numbers (coded as some set \(X\)) we can prove \(\forall n:\psi(n)\) by following this well-order. Like above, \(\Pi_\infty^1-TI\) is conjunction of the above.
- \(\Sigma_m^n-CA\), \(\Pi_m^n-CA\), \(\Delta_m^n-CA\) - these are schemas of comprehension for respective classes of formulas. Their conjunction, \(\Pi_\infty^1-CA\), over a weak base system is equivalent to all of Z
_{2}. - BI - the axiom-schema of bar induction. To state it, we first need a notion of well-founded partial order. We say the ordering \(\prec\) of natural numbers is well-founded if for every set \(X\) the following is true: if for all \(((\forall i\prec j:i\in X)\Rightarrow j\in X)\Rightarrow\forall n:n\in X\). BI states that such an implication is still true if we replace \(n\in X\) by any formula \(\psi(n)\), provided \(a\prec b\) is expressible by arithmetical formula.
- \(\Sigma_m^n-AC\), \(\Pi_m^n-AC\), \(\Delta_m^n-AC\) - these are schemas "adaptating" ZFC's
*axiom of choice*to second-order arithmetic. They say that if for every \(n\) there is a set \(X\) such that \(\psi(n,X)\) (of complexity asserted by the schema), then we can create sequence of sets \(X_n\) such that \(\psi(n,X_n)\). A variant of this schema is so called weak axiom of choice, which requires that for every \(n\) there is precisely one \(X\) making the formula true. - \(\Sigma_m^n-DC\), \(\Pi_m^n-DC\), \(\Delta_m^n-DC\) - these schemas adapt to second-order arithmetic a weak form of the axiom of choice named "axiom of dependent choice". They say that if for every \(n,X\) there is \(Y\) such that \(\psi(n,X,Y)\), then we can find sequence \(X_n\) of sets such that \(\psi(n,X_n,X_{n+1})\). Slight extension to
*strong*dependent choice tells us that the same can be done if we don't assume that such a \(Y\) exists always, but \(\psi(n,X_n,X_{n+1})\) has to hold whenever it exists for \(X_n\). - \(\Sigma_m^n-TR\), \(\Pi_m^n-TR\), \(\Delta_m^n-TR\) - these are extensions to arithmetical transfinite recursion to formulas other than arithmetical ones. As before, intuitively, it says that we can iterate certain constructions transfinitely many times.

## See also

**Basics:** cardinal numbers · normal function · ordinal notation · ordinal numbers · fundamental sequence · ordinal collapsing function · transfinite induction**Theories:** Robinson arithmetic · Presburger arithmetic · Peano arithmetic · KP · **second-order arithmetic** · ZFC**Countable ordinals:** \(\omega\) · \(\varepsilon_0\) · \(\zeta_0\) · \(\Gamma_0\) · \(\vartheta(\Omega^3)\) · \(\vartheta(\Omega^\omega)\) · \(\vartheta(\Omega^\Omega)\) · \(\vartheta(\varepsilon_{\Omega + 1}) = \psi(\Omega_2)\) · \(\psi(\Omega_\omega)\) · \(\psi(\varepsilon_{\Omega_\omega + 1})\) · \(\psi(\psi_I(0))\) · \(\omega_1^\mathfrak{Ch}\) · \(\omega_1^\text{CK}\) · \(\omega_\alpha^\text{CK}\) · \(\lambda,\zeta,\Sigma,\gamma\) · List of countable ordinals**Ordinal hierarchies:** Fast-growing hierarchy · Slow-growing hierarchy · Hardy hierarchy · Middle-growing hierarchy · N-growing hierarchy**Ordinal collapsing functions** Madore · Buchholz · Jäger**Uncountable cardinals:** \(\omega_1\) · omega fixed point · inaccessible cardinal \(I\) · Mahlo cardinal \(M\) · weakly compact cardinal \(K\) · indescribable cardinal · rank-into-rank cardinal**Classes:** \(V\) · \(L\) · \(\textrm{On}\) · Class (set theory)**Other concepts:** Veblen function · absolute infinity