- Types
*N*and*P*, intended as ℕ and ℘(ℕ); arithmetical symbols 0,*S*, + , ⋅ ; relation ∈ between*N*and*P*; axioms of arithmetic like*Z*_{1}but induction axiom using*P*; extensionality and comprehension for*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}schemes 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 : ∃

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 scheme 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}, - ∆
_{1}^{1}-CA_{0} - Π
_{1}^{1}-SEP_{0} - Σ
_{1}^{1}-AC_{0}(still implied by ATR_{0}) - Σ
_{1}^{1}-DC_{0}(not implied by ATR_{0}).

- Weak-Σ
**ATR**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 scheme, 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.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