From HandWiki - Reading time: 8 min
In set theory and mathematical logic, first-order arithmetic is a collection of axiomatic systems formalising natural and subsets of the natural numbers. It is a choice for axiomatic theory as a basis for many mathematics, but not all. The primary first-order axiom is Peano arithmetic, created by Giuseppe Peano:[1]
Peano arithmetic has a proof-theoretic ordinal of .
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:[2]
These axioms are known as PA−; the theory PA is obtained by adding the first-order induction scheme . An important feature of PA− is that any structure satisfying this theory has an initial segment (ordered by ) isomorphic to . Elements in that segment are called standard elements, while other elements are called nonstandard elements.
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:
The axioms are:
Robinson arithmetic has a proof-theoretic ordinal of .
The system of -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:
For ν ≠ ω, the axioms are:
is a weakened version of . In the system of , a set is instead called inductively defined if for some monotonic operator , is a fixed point of , rather than the least fixed point. This subtle difference makes the system significantly weaker: , while .
is weakened even further. In , 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: , while .
is the weakest of all variants of , 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. , while .
is an "unfolding" strengthening of . 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 to : , while .
is an automorphism of . , but is still weaker than .
is an automorphism of . , but is still weaker than .
is an automorphism of . , where is the Veblen hierarchy with countably iterated least fixed points.
PA– is the first-order theory of the nonnegative part of a discretely ordered ring. A ring is a set equipped with two binary operations: (addition) and (multiplication) satisfying the following three sets of axioms, called the ring axioms:
PA– has a proof-theoretic ordinal of .
RFA is rudimentary function arithmetic. A rudimentary function is a function that can be obtained from the following operations:
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 ω2.
IΔ0 and IΣ1 are basic arithmetic with induction for Δ0- and Σ1-predicates, respectively. Note that when people refer to IΔ0, IΔ0 is basic arithmetic with induction for Δ0-predicates, but without an axiom asserting exponentiation is total, while IΔ0 with such an axiom is referred to as IΔ0+. IΔ0n for 1 < n < ω is IΔ0+ augmented by an axiom ensuring that each element of the n-th level of the Grzegorczyk hierarchy is total. IΔ0 has a proof-theoretic ordinal of ω2. IΔ0+. has a proof-theoretic ordinal of ω3. IΔ0n has a proof-theoretic ordinal of ωn. IΣ1 has a proof-theoretic ordinal of ωω.
EFA is elementary function arithmetic. Its language contains:
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
PRA is primitive recursive arithmetic, a quantifier-free formalization of the natural numbers. The language of PRA consists of:
The logical axioms of PRA are the:
The logical rules of PRA are modus ponens and variable substitution.
The non-logical axioms are:
and recursive defining equations for every primitive recursive function as desired.