1. More on Peano Arithmetic

The various axiomatizations of Peano arithmetic are many different, but equivalent. Whereas some axiomatizations, such as the one described just recently (the original definition) use a signature containing only symbols of 0, successor, addition and multiplication, other axiomatizations use the ordered semi-ring language, including an extra order relation symbol. One such axiomatization begins with the following axioms that describe a discretely ordered semiring:^[1]

1. [math]\displaystyle{ \forall x, y, z \ ( (x + y) + z = x + (y + z) ) }[/math], i.e., addition is associative.
2. [math]\displaystyle{ \forall x, y \ ( x + y = y + x ) }[/math], i.e., addition is commutative.
3. [math]\displaystyle{ \forall x, y, z \ ( (x \cdot y) \cdot z = x \cdot (y \cdot z) ) }[/math], i.e., multiplication is associative.
4. [math]\displaystyle{ \forall x, y \ ( x \cdot y = y \cdot x ) }[/math], i.e., multiplication is commutative.
5. [math]\displaystyle{ \forall x, y, z \ ( x \cdot (y + z) = (x \cdot y) + (x \cdot z) ) }[/math], i.e., multiplication distributes over addition.
6. [math]\displaystyle{ \forall x \ ( x + 0 = x \land x \cdot 0 = 0 ) }[/math], i.e., zero is an identity for addition, and an absorbing element for multiplication.
7. [math]\displaystyle{ \forall x \ ( x \cdot 1 = x ) }[/math], i.e., one is an identity for multiplication.
8. [math]\displaystyle{ \forall x, y, z \ ( x \lt y \land y \lt z \Rightarrow x \lt z ) }[/math], i.e., the '<' operator is transitive.
9. [math]\displaystyle{ \forall x \ ( \neg (x \lt x) ) }[/math], i.e., the '<' operator is irreflexive.
10. [math]\displaystyle{ \forall x, y \ ( x \lt y \lor x = y \lor y \lt x ) }[/math], i.e., the ordering satisfies trichotomy.
11. [math]\displaystyle{ \forall x, y, z(x \lt y \rightarrow x + z \lt y + z) }[/math], i.e. the ordering is preserved under addition of the same element.
12. [math]\displaystyle{ \forall x, y, z(0 \lt z \and x \lt y \rightarrow x \cdot z \lt y \cdot z }[/math], i.e. the ordering is preserved under multiplication by the same positive element.
13. [math]\displaystyle{ \forall x, y(x \lt y \rightarrow \exists z(x + z = y)) }[/math], i.e. given any two distinct elements, the larger is the smaller plus another element.
14. [math]\displaystyle{ 0 \lt 1 \and \forall x \in \N( x \gt 0 \rightarrow x \geq 1 ) }[/math], i.e. zero and one are distinct and there is no element between them.
15. [math]\displaystyle{ \forall x \ ( x \ge 0 ) }[/math], i.e. zero is the minimum element.

These axioms are known as PA⁻; the theory PA is obtained by adding the first-order induction scheme [math]\displaystyle{ \forall X(0 \in X \and \forall x \in \N(x \in X)) \rightarrow \N \subseteq X }[/math]. An important feature of PA⁻ is that any structure [math]\displaystyle{ M }[/math] satisfying this theory has an initial segment (ordered by [math]\displaystyle{ \leq }[/math]) isomorphic to [math]\displaystyle{ \N }[/math]. Elements in that segment are called standard elements, while other elements are called nonstandard elements.

2. Robinson Arithmetic Q

Robinson arithmetic is a finitely axiomatized first-order fragment of Peano arithmetic (PA), first produced in 1950 by R.M. Robinson. It is often referred to as Q. Q is nearly identical to PA without the mathematical induction axiom schema (PA⁻). Q is weaker than PA, but their language is the same and the two theories are both incomplete. The background logic of Q is first-order logic with identity, denoted by infix '='. The individuals, called natural numbers, are members of a set called N with a distinguished member 0, called zero. There are three operations over N:

• A unary operation called successor and denoted by prefix S;

• Two binary operations, addition and multiplication, denoted by infix + and ·, respectively.

The axioms are:

• [math]\displaystyle{ \forall x \in \N(S(x) \neq 0) }[/math]: 0 is not the successor of any number.
• [math]\displaystyle{ S(x) = S(y) \rightarrow x= y }[/math]: If the successor of x is identical to the successor of y, then x and y are identical.
• [math]\displaystyle{ \forall x(x = 0 \or \exists y(S(y)=x)) }[/math]Every natural number is either 0 or the successor of some number.
• [math]\displaystyle{ \forall x(x + 0 = x) }[/math]
• [math]\displaystyle{ \forall x, y(x + S(y) = S(x + y)) }[/math]
• [math]\displaystyle{ \forall x(x \cdot 0 = 0) }[/math]
• [math]\displaystyle{ \forall x, y(x \cdot S(y) = (x \cdot y) + x) }[/math]

Robinson arithmetic has a proof-theoretic ordinal of [math]\displaystyle{ \omega = \varphi(0, 1) = \psi_0(1) }[/math].

3. Iterated Inductive Definitions

The system of [math]\displaystyle{ \nu }[/math]-times iterated inductive definitions is a hierarchy of strong mathematical systems developed by German mathematician Wilfried Buchholz, well known for creating Buchholz's psi function. ID_ν extends PA by ν iterated least fixed points of monotone operators. If ν = ω, the axioms are:

• The axioms from Peano arithmetic

• [math]\displaystyle{ \forall y \forall x (\mathfrak{M}_y(P^\mathfrak{M}_y, x) \rightarrow x \in P^\mathfrak{M}_y) }[/math]
• [math]\displaystyle{ \forall y (\forall x (\mathfrak{M}_y(F, x) \rightarrow F(x)) \rightarrow \forall x (x \in P^\mathfrak{M}_y \rightarrow F(x))) }[/math] for every L_ID-formula F(x)
• [math]\displaystyle{ \forall y \forall x_0 \forall x_1(P^\mathfrak{M}_{\lt y}x_0x_1 \leftrightarrow x_0 \lt y \and x_1 \in P^\mathfrak{M}_{x_0}) }[/math]

For ν ≠ ω, the axioms are:

• The axioms from Peano arithmetic

• [math]\displaystyle{ \forall y \forall x (\mathfrak{M}_y(P^\mathfrak{M}_y, x) \rightarrow x \in P^\mathfrak{M}_y) }[/math]
• [math]\displaystyle{ \forall x (\mathfrak{M}_u(F, x) \rightarrow F(x)) \rightarrow \forall x (P^\mathfrak{M}_ux \rightarrow F(x)) }[/math] for every L_ID-formula F(x) and all u < ν
• [math]\displaystyle{ \forall y \forall x_0 \forall x_1(P^\mathfrak{M}_{\lt y}x_0x_1 \leftrightarrow x_0 \lt y \and x_1 \in P^\mathfrak{M}_{x_0}) }[/math]

[math]\displaystyle{ \widehat{\mathsf{ID}}_\nu }[/math] is a weakened version of [math]\displaystyle{ \mathsf{ID}_\nu }[/math]. In the system of [math]\displaystyle{ \widehat{\mathsf{ID}}_\nu }[/math], a set [math]\displaystyle{ I \subseteq \N }[/math] is instead called inductively defined if for some monotonic operator [math]\displaystyle{ \Gamma: P(N) \rightarrow P(N) }[/math], [math]\displaystyle{ I }[/math] is a fixed point of [math]\displaystyle{ \Gamma }[/math], rather than the least fixed point. This subtle difference makes the system significantly weaker: [math]\displaystyle{ PTO(\widehat{\mathsf{ID}}_1) = \varphi(\varepsilon_0, 0) = \psi_0(\Omega^{\varepsilon_0}) }[/math], while [math]\displaystyle{ PTO(\mathsf{ID}_1) = \psi_0(\varepsilon_{\Omega+1}) }[/math].

[math]\displaystyle{ \mathsf{ID}_\nu\# }[/math] is [math]\displaystyle{ \widehat{\mathsf{ID}}_\nu }[/math] weakened even further. In [math]\displaystyle{ \mathsf{ID}_\nu\# }[/math], not only does it use fixed points rather than least fixed points, but also has induction only for positive formulas. This once again subtle difference makes the system even weaker: [math]\displaystyle{ PTO(\mathsf{ID}_1\#) = \varphi(\omega, 0) = \psi_0(\Omega^\omega) }[/math], while [math]\displaystyle{ PTO(\widehat{\mathsf{ID}}_1) = \varphi(\varepsilon_0, 0) = \psi_0(\Omega^{\varepsilon_0}) }[/math].

[math]\displaystyle{ \mathsf{W-ID}_\nu }[/math] is the weakest of all variants of [math]\displaystyle{ \mathsf{ID}_\nu }[/math], based on W-types. The amount of weakening compared to regular iterated inductive definitions is identical to removing bar induction given a certain subsystem of second-order arithmetic. [math]\displaystyle{ PTO(\mathsf{W-ID}_1) = \psi_0(\Omega\times\omega) }[/math], while [math]\displaystyle{ PTO(\mathsf{ID}_1) = \psi_0(\varepsilon_{\Omega+1}) }[/math].

[math]\displaystyle{ \mathsf{U(ID}_\nu\mathsf{)} }[/math] is an "unfolding" strengthening of [math]\displaystyle{ \mathsf{ID}_\nu }[/math]. It is not exactly a first-order arithmetic system, but captures what one can get by predicative reasoning based on ν-times iterated generalized inductive definitions. The amount of increase in strength is identical to the increase from [math]\displaystyle{ \varepsilon_0 }[/math] to [math]\displaystyle{ \Gamma_0 }[/math]: [math]\displaystyle{ PTO(\mathsf{ID}_1) = \psi_0(\varepsilon_{\Omega+1}) }[/math], while [math]\displaystyle{ PTO(\mathsf{U(ID}_1\mathsf{)}) = \psi_0(\Gamma_{\Omega+1}) }[/math].

[math]\displaystyle{ \mathsf{Aut(\widehat{\mathsf{ID}})} }[/math] is an automorphism of [math]\displaystyle{ \mathsf{\widehat{ID}}_\nu }[/math]. [math]\displaystyle{ \mathsf{PTO(Aut(\widehat{\mathsf{ID}}))} = \psi_0(\Omega^{\Omega \times 2}) = \mathsf{PTO(\widehat{\mathsf{ID}}}_{\lt \Omega}) }[/math], but [math]\displaystyle{ \mathsf{Aut(\widehat{\mathsf{ID}})} }[/math] is still weaker than [math]\displaystyle{ \mathsf{ID}_1 }[/math].

[math]\displaystyle{ \mathsf{Aut(\mathsf{ID})} }[/math] is an automorphism of [math]\displaystyle{ \mathsf{ID}_\nu }[/math]. [math]\displaystyle{ \mathsf{PTO(Aut(\mathsf{ID}))} = \psi_0(\Omega_\Omega) = \mathsf{PTO(\mathsf{ID}}_{\lt \Omega}) }[/math], but [math]\displaystyle{ \mathsf{Aut(\mathsf{ID})} }[/math] is still weaker than [math]\displaystyle{ \mathsf{KPi} }[/math].

[math]\displaystyle{ \mathsf{Aut(\mathsf{ID\#})} }[/math] is an automorphism of [math]\displaystyle{ \mathsf{ID}_\nu\# }[/math]. [math]\displaystyle{ \mathsf{PTO(Aut(\mathsf{ID\#}))} = \psi_0(\Omega^{\lt \Omega}) = \mathsf{PTO(\mathsf{ID_{\lt \Omega}\#})} }[/math], where [math]\displaystyle{ \psi_0(\Omega^{\lt \Omega}) = \varphi(\mathsf{\lt }\Omega, 0) }[/math] is the Veblen hierarchy with countably iterated least fixed points.

4. Other First-Order Systems

4.1. PA^–

PA^– is the first-order theory of the nonnegative part of a discretely ordered ring. A ring is a set [math]\displaystyle{ R }[/math] equipped with two binary operations: [math]\displaystyle{ + }[/math] (addition) and [math]\displaystyle{ \cdot }[/math] (multiplication) satisfying the following three sets of axioms, called the ring axioms:

• [math]\displaystyle{ + }[/math] is associative, [math]\displaystyle{ + }[/math] is commutative, [math]\displaystyle{ 0 }[/math] is the additive identity, and [math]\displaystyle{ -a }[/math] is the additive inverse of [math]\displaystyle{ a }[/math].
• [math]\displaystyle{ \cdot }[/math] is associative, and [math]\displaystyle{ 1 }[/math] is the multiplicative identity.
• [math]\displaystyle{ a \cdot (b + c) = (a \cdot b) + (a \cdot c) }[/math] for all [math]\displaystyle{ a }[/math], [math]\displaystyle{ b }[/math] and [math]\displaystyle{ c }[/math] in [math]\displaystyle{ R }[/math].
• [math]\displaystyle{ (b + c) \cdot a = (b \cdot a) + (c \cdot a) }[/math] for all [math]\displaystyle{ a }[/math], [math]\displaystyle{ b }[/math] and [math]\displaystyle{ c }[/math] in [math]\displaystyle{ R }[/math].

PA^– has a proof-theoretic ordinal of [math]\displaystyle{ \omega = \varphi(0, 1) = \psi_0(1) }[/math].

4.2. RFA

RFA is rudimentary function arithmetic. A rudimentary function is a function that can be obtained from the following operations:

• [math]\displaystyle{ F(x_1, x_2, ...) = x_j }[/math] is rudimentary
• [math]\displaystyle{ F(x_1, x_2, ...) = \{x_i, x_j\} }[/math] is rudimentary
• [math]\displaystyle{ F(x_1, x_2, ...) = x_i - x_j }[/math] is rudimentary
• Any composition of rudimentary functions is rudimentary
• [math]\displaystyle{ \bigcup\limits_{z \in y} G(z, x_1, x_2, ...) }[/math] is rudimentary

For any set M let rud(M) be the smallest set containing M∪{M} closed under the rudimentary operations. RFA is a version of arithmetic based on rudimentary functions. RFA has a proof-theoretic ordinal of ω².

4.3. IΔ₀ / IΣ₁

IΔ₀ and IΣ₁ are basic arithmetic with induction for Δ₀- and Σ₁-predicates, respectively. Note that when people refer to IΔ₀, IΔ₀ is basic arithmetic with induction for Δ₀-predicates, but without an axiom asserting exponentiation is total, while IΔ₀ with such an axiom is referred to as IΔ₀⁺. IΔ₀ⁿ for 1 < n < ω is IΔ₀⁺ augmented by an axiom ensuring that each element of the n-th level [math]\displaystyle{ \mathcal{E}^n }[/math] of the Grzegorczyk hierarchy is total. IΔ₀ has a proof-theoretic ordinal of ω². IΔ₀⁺. has a proof-theoretic ordinal of ω³. IΔ₀ⁿ has a proof-theoretic ordinal of ωⁿ. IΣ₁ has a proof-theoretic ordinal of ω^ω.

4.4. EFA

EFA is elementary function arithmetic. Its language contains:

• two constants 0, 1,
• three binary operations +, ×, exp, with exp(x,y) usually written as x^y,
• a binary relation symbol < (This is not really necessary as it can be written in terms of the other operations and is sometimes omitted, but is convenient for defining bounded quantifiers).

Bounded quantifiers are those of the form ∀(x < y) and ∃(x < y) which are abbreviations for ∀ x (x < y) → ... and ∃x (x < y)∧... in the usual way. The axioms of EFA are

• The axioms of Robinson arithmetic for 0, 1, +, ×, <
• The axioms for exponentiation: x⁰ = 1, x^y+1 = x^y × x.
• Induction for formulas all of whose quantifiers are bounded (but which may contain free variables).

4.5. PRA

PRA is primitive recursive arithmetic, a quantifier-free formalization of the natural numbers. The language of PRA consists of:

• A countably infinite number of variables x, y, z,....
• The propositional connectives;
• The equality symbol =, the constant symbol 0, and the successor symbol S (meaning add one);
• A symbol for each primitive recursive function.

The logical axioms of PRA are the:

• Tautologies of the propositional calculus;
• Usual axiomatization of equality as an equivalence relation.

The logical rules of PRA are modus ponens and variable substitution.

The non-logical axioms are:

• [math]\displaystyle{ \forall x(S(x) \neq 0) }[/math]
• [math]\displaystyle{ \forall x \,\forall y(S(x) = S(y) \rightarrow x = y) }[/math]

and recursive defining equations for every primitive recursive function as desired.