You're using an outdated browser. Please upgrade to a modern browser for the best experience.
First-Order Arithmetic
Edit

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: Peano arithmetic has a proof-theoretic ordinal of ε0=φ(1,0)=ψ0(Ω).

axiomatic theory set theory ordinal

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. x,y,z ((x+y)+z=x+(y+z)), i.e., addition is associative.
  2. x,y (x+y=y+x), i.e., addition is commutative.
  3. x,y,z ((xy)z=x(yz)), i.e., multiplication is associative.
  4. x,y (xy=yx), i.e., multiplication is commutative.
  5. x,y,z (x(y+z)=(xy)+(xz)), i.e., multiplication distributes over addition.
  6. x (x+0=xx0=0), i.e., zero is an identity for addition, and an absorbing element for multiplication.
  7. x (x1=x), i.e., one is an identity for multiplication.
  8. x,y,z (x<yy<zx<z), i.e., the '<' operator is transitive.
  9. x (¬(x<x)), i.e., the '<' operator is irreflexive.
  10. x,y (x<yx=yy<x), i.e., the ordering satisfies trichotomy.
  11. x,y,z(x<yx+z<y+z), i.e. the ordering is preserved under addition of the same element.
  12. Undefined control sequence \and, i.e. the ordering is preserved under multiplication by the same positive element.
  13. x,y(x<yz(x+z=y)), i.e. given any two distinct elements, the larger is the smaller plus another element.
  14. Undefined control sequence \and, i.e. zero and one are distinct and there is no element between them.
  15. x (x0), 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 Undefined control sequence \and. An important feature of PA is that any structure M satisfying this theory has an initial segment (ordered by ) isomorphic to Undefined control sequence \N. 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:

  • Undefined control sequence \N: 0 is not the successor of any number.
  • S(x)=S(y)x=y: If the successor of x is identical to the successor of y, then x and y are identical.
  • Undefined control sequence \orEvery natural number is either 0 or the successor of some number.
  • x(x+0=x)
  • x,y(x+S(y)=S(x+y))
  • x(x0=0)
  • x,y(xS(y)=(xy)+x)

Robinson arithmetic has a proof-theoretic ordinal of ω=φ(0,1)=ψ0(1).

3. Iterated Inductive Definitions

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:

  • The axioms from Peano arithmetic
  • yx(My(PyM,x)xPyM)
  • y(x(My(F,x)F(x))x(xPyMF(x))) for every LID-formula F(x)
  • Undefined control sequence \and

For ν ≠ ω, the axioms are:

  • The axioms from Peano arithmetic
  • yx(My(PyM,x)xPyM)
  • x(Mu(F,x)F(x))x(PuMxF(x)) for every LID-formula F(x) and all u < ν
  • Undefined control sequence \and

ID^ν is a weakened version of IDν. In the system of ID^ν, a set Undefined control sequence \N is instead called inductively defined if for some monotonic operator Γ:P(N)P(N), I is a fixed point of Γ, rather than the least fixed point. This subtle difference makes the system significantly weaker: PTO(ID^1)=φ(ε0,0)=ψ0(Ωε0), while PTO(ID1)=ψ0(εΩ+1).

IDν# is ID^ν weakened even further. In IDν#, 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: PTO(ID1#)=φ(ω,0)=ψ0(Ωω), while PTO(ID^1)=φ(ε0,0)=ψ0(Ωε0).

WIDν is the weakest of all variants of IDν, 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. PTO(WID1)=ψ0(Ω×ω), while PTO(ID1)=ψ0(εΩ+1).

U(IDν) is an "unfolding" strengthening of IDν. 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 ε0 to Γ0: PTO(ID1)=ψ0(εΩ+1), while PTO(U(ID1))=ψ0(ΓΩ+1).

Aut(ID^) is an automorphism of ID^ν. PTO(Aut(ID^))=ψ0(ΩΩ×2)=PTO(ID^<Ω), but Aut(ID^) is still weaker than ID1.

Aut(ID) is an automorphism of IDν. PTO(Aut(ID))=ψ0(ΩΩ)=PTO(ID<Ω), but Aut(ID) is still weaker than KPi.

Aut(ID#) is an automorphism of IDν#. PTO(Aut(ID#))=ψ0(Ω<Ω)=PTO(ID<Ω#), where ψ0(Ω<Ω)=φ(<Ω,0) 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 R equipped with two binary operations: + (addition) and (multiplication) satisfying the following three sets of axioms, called the ring axioms:

  • + is associative, + is commutative, 0 is the additive identity, and a is the additive inverse of a.
  • is associative, and 1 is the multiplicative identity.
  • a(b+c)=(ab)+(ac) for all a, b and c in R.
  • (b+c)a=(ba)+(ca) for all a, b and c in R.

PA has a proof-theoretic ordinal of ω=φ(0,1)=ψ0(1).

4.2. RFA

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

  • F(x1,x2,...)=xj is rudimentary
  • F(x1,x2,...)={xi,xj} is rudimentary
  • F(x1,x2,...)=xixj is rudimentary
  • Any composition of rudimentary functions is rudimentary
  • zyG(z,x1,x2,...) 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 ω2.

4.3. IΔ0 / IΣ1

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 En 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 ωω.

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 xy,
  • 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: x0 = 1, xy+1 = xy × 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:

  • x(S(x)0)
  • xy(S(x)=S(y)x=y)

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

References

  1. Kaye, Richard (1991). Models of Peano Arithmetic. pp. 16-18. 
More
Information
Subjects: Mathematics
Contributor MDPI registered users' name will be linked to their SciProfiles pages. To register with us, please refer to https://encyclopedia.pub/register :
View Times: 2.2K
Entry Collection: HandWiki
Revisions: 4 times (View History)
Update Date: 10 Oct 2022
Video Production Service