Second-order arithmetic

View full site to see MathJax equation

Second-order arithmetic (also known as Z₂ 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₂, allows us to discuss two types of objects, namely numbers themselves, or sets of numbers. It is an extension of propositional 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₂ 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₂. 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₀, WKL₀, ACA₀, ATR₀, and Π₁¹-CA₀. 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₀.

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₀

RCA₀, 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₀'s axioms. RCA₀ 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₀ can prove most "everyday" properties of natural numbers and real numbers.

RCA₀ 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₀ has a proof-theoretic ordinal of \(\omega^\omega\).

WKL₀

WKL₀ stands for "weak König's lemma." We form WKL₀ by extending RCA₀ 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₀ cannot prove this lemma — recalling that RCA₀ cannot prove the existence of uncomputable sets, we can create an infinite computable tree \(T\) which has no computable infinite branches. Consequently, WKL₀ is a proper extension of RCA₀.

It can be shown that many natural statements are equivalent (over base theory RCA₀) to WKL₀, 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₀ has a proof-theoretic ordinal of \(\omega^\omega\) and has the same consistency strength than RCA₀, i.e. they are equiconsistent.

ACA₀

Arithmetical comprehension axiom. We get this by adjoining to RCA₀ 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₀ which can be expressed in first-order arithmetic are precisely the formulas provable by Peano arithmetic (one says that ACA₀ is conservative over Peano arithmetic for arithmetical sentences). Like before, it can be shown that ACA₀ is a proper extension of WKL₀, although the proof in this case is not as simple.

ACA₀ 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₀ is provably equivalent to these two statements).

ACA₀ has a proof-theoretic ordinal of ε₀.

ATR₀

This one stands for "arithmetical transfinite recursion". This system is ACA₀ 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₀, which means that it is significantly stronger than ACA₀ (see Gödel's incompleteness theorems).

Important single theorem which is equivalent (over RCA₀) to ATR₀ is that every two countable well-orderings are comparable, so that ordinal numbers form a linear order.

Another important schema equivalent to ATR₀ 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₀ is the Feferman–Schütte ordinal.

\(\Pi_1^1\textrm{-CA}_0\)

The last, and the strongest system in the big five is RCA₀ 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\textrm{-CA}_0\) contains all the axioms of ACA₀, and it can be shown that it also proves all instances of ATR₀ axioms, which shows that \(\Pi_1^1\textrm{-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\textrm{-CA}_0\) is Ψ₀(Ω_ω) with respect to Buchholz's function.

Other subsystems

Apart from the Big Five, many subsystems of Z₂ have been characterized. Below is the list of more noteworthy ones.

1. RCA, WKL, etc. - these are extensions of corresponding systems RCA₀, WKL₀, etc. resulting by addition of first-order induction schema for all formulas in language of second-order arithmetic. The indicator of whether this full axiom schema appears in subsystem or not is the 0 in the subscript.
2. \(\Sigma_m^n\textrm{-IND}\), \(\Pi_m^n\textrm{-IND}\), \(\Delta_m^n\textrm{-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, and the classes of formulae are with respect to the analytical hierarchy). Additionally, \(\Pi_\infty^1\textrm{-IND}\) is conjunction of all of these schemas.
3. \(\Sigma_m^n\textrm{-TI}\), \(\Pi_m^n\textrm{-TI}\), \(\Delta_m^n\textrm{-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.
4. \(\Sigma_m^n\textrm{-CA}\), \(\Pi_m^n\textrm{-CA}\), \(\Delta_m^n\textrm{-CA}\) - these are schemas of comprehension for respective classes of formulas. Their conjunction, \(\Pi_\infty^1\textrm{-CA}\) - over a weak base system this is equivalent to all of Z₂.
5. \(\textrm{BI}\) - the axiom-schema of bar induction. To state it, we first need a notion of well-founded partial order. We say an ordering \(\prec\) on 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 an arithmetical formula.
6. \(\Sigma_m^n\textrm{-AC}\), \(\Pi_m^n\textrm{-AC}\), \(\Delta_m^n\textrm{-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.
7. \(\Sigma_m^n\textrm{-DC}\), \(\Pi_m^n\textrm{-DC}\), \(\Delta_m^n\textrm{-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})\). 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\).
8. \(\Sigma_m^n\textrm{-TR}\), \(\Pi_m^n\textrm{-TR}\), \(\Delta_m^n\textrm{-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.

Note that there are different ways of denoting subsystems of second-order arithmetic, including "\((\Pi_1^1\textrm{-CA})\)" for \(\Pi_1^1\textrm{-CA}_0\) augmented by induction for \(\mathcal L_2\)-formulae.

Sources

Ordinals, ordinal analysis, and set theory

Basics: cardinal numbers · ordinal numbers · limit ordinals · fundamental sequence · normal form · transfinite induction · ordinal notation · Absolute infinity
Theories: Robinson arithmetic · Presburger arithmetic · Peano arithmetic · KP · second-order arithmetic · ZFC
Model Theoretic Concepts: structure · elementary embedding
Countable ordinals: \(\omega\) · \(\varepsilon_0\) · \(\zeta_0\) · \(\eta_0\) · \(\Gamma_0\) (Feferman–Schütte ordinal) · \(\varphi(1,0,0,0)\) (Ackermann ordinal) · \(\psi_0(\Omega^{\Omega^\omega})\) (small Veblen ordinal) · \(\psi_0(\Omega^{\Omega^\Omega})\) (large Veblen ordinal) · \(\psi_0(\varepsilon_{\Omega + 1}) = \psi_0(\Omega_2)\) (Bachmann-Howard ordinal) · \(\psi_0(\Omega_\omega)\) with respect to Buchholz's ψ · \(\psi_0(\varepsilon_{\Omega_\omega + 1})\) (Takeuti-Feferman-Buchholz ordinal) · \(\psi_0(\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}})\) (countable limit of Extended Buchholz's function)‎ · \(\omega_1^\mathfrak{Ch}\) (Omega one of chess) · \(\omega_1^{\text{CK}}\) (Church-Kleene ordinal) · \(\omega_\alpha^\text{CK}\) (admissible ordinal) · recursively inaccessible ordinal · recursively Mahlo ordinal · reflecting ordinal · stable ordinal · \(\lambda,\gamma,\zeta,\Sigma\) (Infinite time Turing machine ordinals) · gap ordinal · List of countable ordinals
Ordinal hierarchies: Fast-growing hierarchy · Hardy hierarchy · Slow-growing hierarchy · Middle-growing hierarchy · N-growing hierarchy
Ordinal functions: enumeration · normal function · derivative · Veblen function · ordinal collapsing function · Weak Buchholz's function · Bachmann's function · Madore's function · Feferman's theta function · Buchholz's function · Extended Weak Buchholz's function · Extended Buchholz's function · Jäger-Buchholz function · Jäger's function · Rathjen's psi function · Rathjen's Psi function · Stegert's Psi function · Arai's psi function
Uncountable cardinals: \(\omega_1\) · omega fixed point · inaccessible cardinal \(I\) · Mahlo cardinal \(M\) · weakly compact cardinal \(K\) · indescribable cardinal · rank-into-rank cardinal · Berkeley cardinal · (Club Berkeley cardinal · limit club Berkeley cardinal)
Classes: \(\textrm{Card}\) · \(\textrm{On}\) · \(V\) · \(L\) · \(\textrm{Lim}\) · \(\textrm{AP}\) · Class (set theory)