Unlike Presburger arithmetic which cannot define recursion, an

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 ℕ).

- Types
*N*and*P*, intended as ℕ and ℘(ℕ); language and axioms like*Z*_{1}but induction axiom using*P*; - Types
*N*and Rel_{N}^{(2)}; structures 0 and*S* - Types
*N*and*N*^{N}; structures 0 and*S*

2. gives 3. by constructing

3. allows to define recursion, giving + and ⋅ as particular cases, thus 1.

*Z*_{2} 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:

- While the set ℝ of real numbers may be described using its own
powerset ℘(ℝ), it may also be built from
*P*using binary representations; - Sequences in
*P*and thus in ℝ can be represented by Rel_{N}^{(2)}≅*P*^{N}. Recursive ones can be defined from there.

- AC
_{X}for any uncountable set*X*, by lack of uncountable products - The existence of non-measurable sets by lack of range where such sets might exist
- The continuum hypothesis, also by lack of a set of all functions between uncountable sets, where a bijection might exist.

A formula is called

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

Formulas are classified in the following inclusion-ordered hierarchy of ranges, all allowing parameters in

- a formula is Σ
_{n}^{0}(resp. Π_{n}^{1}) when it is arithmetical, made of*n*alternating quantifiers starting with ∃ (resp. with ∀), over a bounded formula; -
a formula is Σ
_{n}^{1}(resp. Π_{n}^{1}) when it is made of*n*alternating set quantifiers starting with ∃ (resp. with ∀), over an arithmetical formula. (Moving numerical variables right would depend on the below axiom of countable choice, which may not hold, so that care is needed...); - the ∆
_{n}^{i}schemas are "intersections" of Σ_{n}^{i}and Π_{n}^{i}, ranging over sets equivalently defined both ways:

For all ϕ,ψ in Σ_{n}^{i}, (∀param.,(∀*n*,ϕ(*n*)⇔¬ψ(*n*))⇒...) (ref.)

Each Σ

- To any Σ
_{1}^{0}formula (∃*n*, ϕ(*n*)), corresponds the algorithm of search for a number*n*satisfying ϕ(*n*); - The halting of any algorithm is expressible by a Σ
_{1}^{0}formula, essentially (∃*n*, it halts at time*n*).

Ind (induction) : (ϕ(0) ∧ ∀

SEP (separation) : (∀

AC (countable choice) : (∀

Weak AC : (∀

DC (dependent choice) : (∀

Strong DC : ∃

TI : transfinite induction

They are related by

Π_{n}^{i}-CA ⇔ Σ_{n}^{i}-CA ⇒ Σ_{n}^{i}-SEP ⇒ ∆_{n}^{i}-CA

Π_{n}^{i}-CA ⇒ Π_{n}^{i}-SEP ⇒ ∆_{n}^{i}-CA

Σ_{n}^{i}-Ind ⇔ Π_{n}^{i}-Ind

**RCA**(Recursive Comprehension) = Σ_{0}_{1}^{0}-Ind + ∆_{1}^{0}-CA. Implies Π_{1}^{0}-SEP- WWKL
_{0}(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. **WKL**(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 Σ_{0}_{1}^{0}-SEP, Π_{1}^{0}-AC, Π_{1}^{0}-DC and strong Π_{1}^{0}-DC. Its first-order part is still that of first-order arithmetic with Σ_{1}^{0}induction. Details.**ACA**(Arithmetic Comprehension Axioms): the CA schema for all arithmetical formulas, which (by the induction axiom) leads to the same first-order part as_{0}*Z*_{1}. It is equivalent to the existence in*P*of the image of any injective numerical function: this first implies Σ_{1}^{0}-CA (= Turing jump), whose allowance of parameters means that*P*is stable by this jump, thus ∀*n*∈ℕ, the stability by*n*successive Turing jumps: Σ_{n}^{0}-CA.- 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):
- Weak-Σ
_{1}^{1}-AC_{0}(implies the existence of a system of interpretations of first-order formulas in any given countable system ; I am not sure of the converse). - ∆
_{1}^{1}-CA_{0} - Π
_{1}^{1}-SEP_{0} - Σ
_{1}^{1}-AC_{0}(still implied by ATR_{0}) - Σ
_{1}^{1}-DC_{0}equivalent to Π_{1}^{1}-TI_{0}(not implied by ATR_{0}).

- Weak-Σ
**ATR**: Arithmetical transfinite recursion (expressing the definiteness of sets by transfinite recursion along countable well-orders), equivalent to Σ_{0}_{1}^{1}-SEP.**Π**, equivalent to Strong Σ_{1}^{1}-CA_{0}_{1}^{1}-DC_{0}. For the standard*N*=ℕ, there is no minimal*P*satisfying this schema, but there is a minimal one among those Π_{1}^{1}-elementarily embedded in ℘(ℕ). In guise of construction, it is the minimal one stable by hyperjump, which is crazily more powerful than the Turing jump.- ∆
_{2}^{1}-CA_{0}⇔ Σ_{2}^{1}-AC_{0}⇔ Π_{2}^{1}-SEP_{0} - Σ
_{2}^{1}-DC_{0}is equivalent to Δ_{2}^{1}-CA + Σ_{2}^{1}-Ind - Π
_{2}^{1}-CA_{0}⇔ Strong Σ_{2}^{1}-DC_{0}⇔ Σ_{2}^{1}-SEP_{0} *Z*_{2}. But even the whole ZF set theory does not imply Π_{2}^{1}-AC.*Z*_{2}+ AC. But even ZF with countable choice does not imply Π_{2}^{1}-DC.*Z*_{2}+ DC

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 Π

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.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 :
5.2. Second-order logic

5.3. Well-foundedness

5.4. Ordinals and cardinals

5.5. Undecidability of the axiom of choice

5.6.

5.7. The Incompleteness Theorem