Second-order arithmetic
Second-order arithmetic, denoted \(Z_2\) is an extension of first-order (i.e. Peano) arithmetic by adding additional second-order variables as well as an induction scheme for \(\mathcal{P}(\mathbb{N})\), and a comprehension scheme. Proof-theoretically, \(Z_2\) is a very expressive system, as it can prove the consistency of Peano arithmetic and its extensions via the addition of iterated inductive definitions - an ordinal analysis of \(Z_2\) is considered the holy grail of ordinal analysis, and many believe it can be done using BMS.
Reverse mathematics[edit | edit source]
One of the primary interests regarding \(Z_2\) is the study of its subsystems, rather than the whole. This is part of a program called reverse mathematics. Since rational numbers, real numbers, complex numbers, continuous functions on the reals, countable groups, and more can be defined in the language of second-order arithmetic, it turns out many classical theorems in number theory, real analysis, topology, abstract algebra and group theory are provable in \(Z_2\), and most even in weak subsystems! The "big five" are the following:[1]
- \(\mathrm{RCA}_0\): recursive comprehension axiom, i.e. \(Z_2\) with comprehension restricted to \(\Delta^0_1\)-formulae and induction restricted to \(\Sigma^0_1\)-formulae.
\(\mathrm{RCA}_0\) has proof-theoretic ordinal \(\omega^\omega\), and it can prove the following famous results: the Baire category theorem, the intermediate value theorem, the soundness theorem, the existence of an algebraic closure of a countable field, the existence of a unique real closure of a countable ordered field.
- \(\mathrm{WKL}_0\): weak König's lemma, i.e. \(\mathrm{RCA}_0\) with the additional axiom "every infinite binary tree has an infinite branch"
\(\mathrm{WKL}_0\) has the same proof-theoretic ordinal as \(\mathrm{RCA}_0\), but is able to prove some non-induction related theorems which \(\mathrm{RCA}_0\) can't, such as: the Heine/Borel covering lemma, every continuous real-valued function on [0, 1], or even any compact metric space, is bounded, the local existence theorem for solutions of (finite systems of) ordinary differential equations, Gödel’s completeness theorem, every countable commutative ring has a prime ideal and Brouwer’s fixed point theorem.
- \(\mathrm{ACA}_0\): arithmetical comprehension axiom, i.e. \(Z_2\) with comprehension restricted to \(\Delta^1_0\)-formulae
\(\mathrm{ACA}_0\) and Peano arithmetic have the same first-order consequences and thus the same proof-theoretic ordinal: namely, \(\varepsilon_0\). Not much has been said regarding \(\mathrm{ACA}_0\)'s ordinary, non-number-theoretical consequences.
- \(\mathrm{ATR}_0\): arithmetical transfinite recursion, i.e. \(\mathrm{ACA}_0\) with the additional axiom "every arithmetical operator can be iterated along any countable well-ordering"
\(\mathrm{ATR}_0\) has the proof-theoretic ordinal \(\Gamma_0\), which is part of the reason why the ordinal in question is claimed to be the limit of what can be predicatively defined. \(\mathrm{ATR}_0\) can prove the following: any two countable well orderings are comparable, any two countable reduced Abelian p-groups which have the same Ulm invariants are isomorphic, and that every uncountable closed, or analytic, set has a perfect subset.
- \(\Pi^1_1 \mathrm{-CA}_0\): \(\Pi^1_1\)-comprehension axiom, i.e. \(Z_2\) with comprehension restricted to \(\Pi^1_1\)-formulae
\(\Pi^1_1 \mathrm{-CA}_0\) has a significantly higher proof-theoretic ordinal than the previous entries - namely, \(\psi_0(\Omega_\omega)\). It can prove the following: every countable Abelian group is the direct sum of a divisible group and a reduced group, the Cantor/Bendixson theorem, a set is Borel iff it and its complement are analytic, any two disjoint analytic sets can be separated by a Borel set, coanalytic uniformization, and more.
There are also even stronger systems such as \(\Pi^1_1 \mathrm{-TR}_0\), which is \(\Pi^1_1 \mathrm{-CA}_0\) with the axiom "every \(\Pi^1_1\)-definable operator can be iterated along any countable well-ordering", \(\Pi^1_2 \mathrm{-CA}_0\), and more. The former has proof-theoretic ordinal EBO, while the latter's proof-theoretic ordinal hasn't been precisely calibrated but has been bound.[2][3]