4.7. Second-order arithmetic

Arithmetic with Henkin semantics is denoted Z2, while Z1 is full first-order arithmetic. The following 3 presentations are equivalent in the sense of first-order developments from each other:
  1. Types N and P, intended as ℕ and ℘(ℕ); arithmetical symbols 0, S, + , ⋅ ; relation ∈ between N and P; axioms of arithmetic like Z1 but induction axiom using P; extensionality and comprehension for P.
  2. Types N and RelN(2); structures 0 and S
  3. Types N and NN; structures 0 and S
1. by + and ⋅ can define a bijection from N×N to N, letting P represent RelN(2), thus 2.
2. gives 3. by constructing NN as the subset of functional graphs from RelN(2).
3. allows to define recursion, giving + and ⋅ as particular cases, thus 1.

Z2 suffices as a foundation for most of ordinary mathematics (and all physics). Compared to set theory, it suffers not so much its weaker proving power (still quite good), than the harder work it takes to develop the needed mathematical concepts on its basis. First are easy cases:

Other objects can be harder to represent. In lack of type for ℘(ℝ) or ℝ, we can still encode specific ranges of sets or functions from these, by expressions with parameters in P. For example, continuous functions f:ℝ→ℝ can be encoded as relations, namely {(x,y)∈A2|f(x)>y} with a countable A dense in ℝ, e.g. {a/bb/a|a,b>0}, or {ab2|a,bN}. But the following statements are inexpressible in Z2: In the study of reverse mathematics, specialists discovered a natural hierarchy of variants of second-order arithmetic, differing by the range of their axioms and thus their theorems. Most of these systems are have a number of equivalent theorems from ordinary mathematics, and are pairwise comparable by implication, totally ordering their sets of theorems by inclusion. They are expressed by axiom schemes classified by what they say (the containing formula) and the range of admitted sub-formulas.

Hierarchy of formulas

To properly classify formulas for admission in axiom schemes, the order ≤ in N with its definition must be added to the theory.
A formula is called arithmetical if all its quantifiers are numerical. Similarly as in set theory, a formula is bounded or Σ00 if it is numerical and all its quantifiers are bounded above, i.e. (∀xn) or (∃xn), which roughly means its truth is computable in known time.
Once written a formula in prenex form, its chain of quantifiers is reducible to an alternation between ∃ and ∀, as two successive quantifiers of the same kind are reducible to only one thanks to N×NN and P×PP. In arithmetical formulas, bounded quantifiers can be moved right thanks to the finite choice theorem encoded by a representation of tuples.
Formulas are classified in the following inclusion-ordered hierarchy of ranges, all allowing parameters in N and P: for any n∈ℕ, As Σni ∪ Πni ⊂ Σn+1i ∩ Πn+1i, any ∆n+1i scheme implies both Σni and Πni versions of the scheme.
Each Σ10 formula represents an algorithm, as it means that this algorithm will halt for the given value(s) of parameter(s) as input: The Σ10 sets are recursively enumerable (sets of all outputs of an endlessly running algorithm). An important example is the set {t|∃p, p is a proof of t} of all theorems of any theory defined with a recursively enumerated set of axioms (the axiom schemes presented here are even Σ00 defined).

The diverse axioms using variable subformulas

CA (comprehension axiom) : ∃X,∀n, nX ⇔ ϕ(n).
Ind (induction) : (ϕ(0) ∧ ∀n, ϕ(n)⇒ϕ(Sn)) ⇒ ∀n, ϕ(n)
SEP (separation) : (∀n,ϕ(n)⇒¬ψ(n)) ⇒ (∃X,∀n, ϕ(n) ⇒ nX ⇒ ¬ψ(n))
AC (countable choice) : (∀n, ∃X, ϕ(n, X)) ⇒ ∃ZPN, ∀n, ϕ(n, Z(n))
Weak AC : (∀n, ∃!X, ϕ(n, X)) ⇒ ∃Z∈PN, ∀n, ϕ(n, Z(n))
DC (dependent choice) : (∀n, ∀X, ∃Y, η(n,X,Y)) ⇒ ∃ZPN, ∀n η(n,Z(n),Z(n+1))
Strong DC : ∃ZPNn (∃Y, η(n,Z(n),Y)) ⇒ η(n,Z(n),Z(n+1))

They are related by

Πni-CA ⇔ Σni-CA ⇒ Σni-SEP ⇒ ∆ni-CA
Πni-CA ⇒ Πni-SEP ⇒ ∆ni-CA
Σni-Ind ⇔ Πni-Ind

Ordered list of the main axiomatic theories

Here are listed some of the main systems, following the total order between their strengths, with the 5 most important ones in bold (the 0 index indicates the lack of full induction scheme, and should be ignored). The first-order part is the set of theorems expressible in the language of Z1.
  1. RCA0 (Recursive Comprehension) = Σ10-Ind + ∆10-CA. Implies Π10-SEP
  2. WWKL0 (Weak Weak König's lemma), means that no sequence of intervals in ℝ can cover a longer interval than the sum of their lengths. This is the basic requirement for measure theory to work.
  3. WKL0 (Weak König's lemma) is equivalent to the completeness theorem (whose difficulty is to choose consistent values of Boolean variables, while the recursive choice depends on the unbounded condition of consistency), and to each of Σ10-SEP, Π10-AC, Π10-DC and strong Π10-DC. Its first-order part is still that of first-order arithmetic with Σ10 induction. Details.
  4. ACA0 (Arithmetic Comprehension Axioms): the CA scheme for all arithmetical formulas, which (by the induction axiom) leads to the same first-order part as Z1. It is equivalent to the existence in P of the image of any injective numerical function: this first implies Σ10-CA (= Turing jump), whose allowance of parameters means that P is stable by this jump, thus ∀n∈ℕ, the stability by n successive Turing jumps: Σn0-CA.
  5. Theories of hyperarithmetic analysis require S to be hyperarithmetically closed while admitting the set of hyperarithmetic sets as their minimal model. Still there are endlessly many inequivalent versions (all stronger that the mere requirement of hyperarithmetic closure):
    1. Weak-Σ11-AC0,
    2. 11-CA0
    3. Π11-SEP0
    4. Σ11-AC0 (still implied by ATR0)
    5. Σ11-DC0 (not implied by ATR0).
  6. ATR0 equivalent to Σ11-SEP
  7. Π11-CA0, equivalent to Strong Σ11-DC0. For the standard N=ℕ, there is no minimal P satisfying this scheme, but there is a minimal one among those Π11-elementarily embedded in ℘(ℕ). In guise of construction, it is the minimal one stable by hyperjump, which is crazily more powerful than the Turing jump.
  8. 21-CA0 ⇔ Σ21-AC0 ⇔ Π21-SEP0
  9. Σ21-DC0 is equivalent to Δ21-CA + Σ21-Ind
  10. Π21-CA0 ⇔ Strong Σ21-DC0 ⇔ Σ21-SEP0
  11. Z2. But even the whole ZF set theory does not imply Π21-AC.
  12. Z2 + AC. But even ZF with countable choice does not imply Π21-DC.
  13. Z2 + DC

References

Stephen G. Simpson, Subsystems of Second Order Arithmetic
Antonio Montalban, On the Pi-1-1 Separation Principle - Theories of Hyperarithmetic Analysis - A survey.
Victoria Gitman, A model of second-order arithmetic with the choice scheme in which Π21-dependent choice fails
Connie Fan, Reverse mathematics
Wikipedia : Second-order arithmetic - Reverse mathematics - arithmetical hierarchy
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
4. Model Theory
4.1. Finiteness and countability
4.2. The Completeness Theorem
4.3. Non-standard models of Arithmetic
4.4. How theories develop
4.5. Second-order logic
4.6. The undecidability of the axiom of choice
4.7. Second-order arithmetic
4.8. The Incompleteness Theorem