5.6. Second-order arithmetic

First-order arithmetic

Full first-order arithmetic, with symbols 0, S, + , ⋅ and the relevant axioms, is denoted Z1.
Unlike Presburger arithmetic which cannot define recursion, an H ⊂ Eℕ that suffices to define recursion can be constructed in Z1 (abbreviating a range of operations defined by a formula with parameters). But naive attempts to construct such an H cannot fit because they need to assume the definiteness of recursion which we wish them to provide. A solution was discovered by Gödel (from which he could build the needed tools to prove his famous incompleteness theorem), but is too difficult to be presented here. Still our exposition may escape the accusation of skipping a proof of a used result, by replacing, in all what follows, the theory Z1 with a richer theory with structures and axioms for numbering finite sequences, that would give such an H more directly built in.
From recursion, many operations can be defined: exponentiation, binary representations, factorials, approximations of square roots and third roots... possibilities escape any attempt of nicely ordered description. Among recursively defined concepts are the crucial cases of formulas and proofs.
Thus, for any consistent theory (given by an arithmetical definition), the proof of the completeness theorem provides a model that is arithmetically defined using a recursive use of an oracle of answers to provability questions. In general, this complexity escapes itself the power of any particular recursion: the totality of what is recursive is not itself recursive, as illustrated by the famous halting problem (which is another aspect of the incompleteness theorem). We could only exceptionally describe non-standard models of Presburger arithmetic thanks to the weakness of that arithmetic, unable to express recursion. But the ability of full arithmetic to contain recursion does not leave the possibility for recursion to describe any of its non-standard models. Namely, Tennenbaum's theorem forbids arithmetic from having any countable non-standard model where either addition or multiplication is computable (in the sense of its countability, i.e. as interpreted in ℕ).

Second-order arithmetic

Arithmetic with Henkin semantics is denoted Z2. The following 3 presentations (each with the relevant stuff of Henkin semantics : interpreter symbol, extensionality axiom or similar, and schema of comprehension using the whole language of Z2) are equivalent in the sense of first-order developments from each other:
  1. Types N and P, intended as ℕ and ℘(ℕ); language and axioms like Z1 but induction axiom using 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/b−b/a|a,b>0}, or {a−b√2|a,b∈N}. 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 schemas 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 schemas, 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. (∀x≤n) or (∃x≤n), 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×N≅N and P×P≅P. 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 schema implies both Σni and Πni versions of the schema.
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 schemas presented here are even Σ00 defined).

The diverse axioms using variable subformulas

CA (comprehension axiom) : ∃X,∀n, n∈X ⇔ ϕ(n).
Ind (induction) : (ϕ(0) ∧ ∀n, ϕ(n)⇒ϕ(Sn)) ⇒ ∀n, ϕ(n)
SEP (separation) : (∀n,ϕ(n)⇒¬ψ(n)) ⇒ (∃X,∀n, ϕ(n) ⇒ n∈X ⇒ ¬ψ(n))
AC (countable choice) : (∀n, ∃X, ϕ(n, X)) ⇒ ∃Z∈PN, ∀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)) ⇒ ∃Z∈PN, ∀n η(n,Z(n),Z(n+1))
Strong DC : ∃Z∈PN ∀n (∃Y, η(n,Z(n),Y)) ⇒ η(n,Z(n),Z(n+1))
TI : transfinite induction
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 schema, 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 schema 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 (implies the existence of a system of interpretations of first-order formulas in any given countable system ; I am not sure of the converse).
    2. ∆11-CA0
    3. Π11-SEP0
    4. Σ11-AC0 (still implied by ATR0)
    5. Σ11-DC0 equivalent to Π11-TI0 (not implied by ATR0).
  6. ATR0 : Arithmetical transfinite recursion (expressing the definiteness of sets by transfinite recursion along countable well-orders), equivalent to Σ11-SEP.
  7. Π11-CA0, equivalent to Strong Σ11-DC0. For the standard N=ℕ, there is no minimal P satisfying this schema, 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. Arithmetic and first-order foundations
5. Second-order foundations
5.1. Second-order structures and invariants
5.2. Second-order logic
5.3. Well-foundedness
5.4. Ordinals and cardinals
5.5. Undecidability of the axiom of choice
5.6. Second-order arithmetic
5.7. The Incompleteness Theorem
More philosophical notes :
Gödelian arguments against mechanism : what was wrong and how to do instead
Philosophical proof of consistency of the Zermelo-Fraenkel axiomatic system