### First-order theories of arithmetic

Our first formalization of ℕ was based on the framework of set theory, where it used the powerset to characterize ℕ in an "essentially unique" way (specify its isomorphism class). It allowed recursion, from which we could define addition and multiplication.

Let us now consider formalizations in the framework of first-order logic, thus called first-order arithmetic. As first-order logic cannot fully express the powerset, the (∀A⊂ℕ) in the induction axiom must be replaced by a weaker version : it can only be expressed with A ranging over all classes of the theory, that is, the only subsets of ℕ defined by first-order formulas in the given language, with bound variables and parameters in ℕ. For this, it must take the form of a schema of axioms, one for each formula that can define a class.

But without the set theoretical framework we used to express and justify the definiteness of recursive definitions, the successor function no more suffices to define addition and multiplication. This leaves us with several non-equivalent versions of first-order arithmetic depending on the choice of the primitive language, thus non-equivalent versions of the axiom schema of induction whose range of expressible classes depends on this language:
• Bare arithmetic, with the mere symbols 0 and S, is very poor.
• Presburger arithmetic, with addition, starts to be interesting, but still cannot define multiplication.
• Full arithmetic, with addition and multiplication, is finally able to express all recursive definitions.

### Presburger arithmetic

Presburger arithmetic has been proven by experts to be a decidable theory, i.e. all its ground formulas are either provable or refutable from its axioms. Let us present its shortest equivalent formalization, describing the set ℕ* of nonzero natural numbers, with 2 primitive symbols: the constant 1 and the operation +. Axioms will be
 ∀x,y∈ℕ*, x + (y+1) = (x+y)+1 (A1) : + is associative on 1 ∀A⊂ℕ*,(1∈A ∧ ∀x,y∈A, x+y∈A) ⇒A=ℕ* (Min) ∀x,y∈ℕ*, x + y ≠ y (F)

In set theory, (Min) would make ℕ* a minimal {1,+}-algebra. But let us regard our present use of set theoretical notations as mere abusive abbreviations of works in first-order logic, as long as we only consider subsets of ℕ* defined by first-order formulas in this arithmetical language. In particular, (Min) will be meant as abbreviating a schema of axioms with A ranging over all classes in this theory.
(A1) is a particular case of
 ∀x,y,z∈ℕ*, x + (y+z) = (x+y)+z (As) : + is associative

Conversely, (A1 ∧ Min) ⇒ (As) :
Let A={a∈ℕ* |∀x,y ∈ℕ*, x+(y+a) = (x+y)+a}. ∀a,bA,
x,y ∈ℕ*, x + (y+(a+b)) = x + ((y+a)+b) = (x + (y+a))+b = ((x + y)+a)+b = (x+y)+(a+b)
a+b A.
(A1) ⇔ 1∈A.
(A1 ∧ Min) ⇒ A=ℕ* ∎
(As ∧ Min) ⇒ (+ is commutative), as deduced from 1∈C({1}) by the above proposition.

Now take ℕ = ℕ*∪{0} where 0∉ℕ*, to which + is extended as ∀n∈ℕ, 0+n = n+0 = n. This extension preserves its properties of commutativity and associativity.
Define S as ℕ∋xx+1.
These definitions directly imply (H0).

(Ind) ⇒ (Min) :
A⊂ℕ*, the set A0= A∪{0} satisfies 0∈A0 and
(1∈A ∧ (∀x,yA, x+yA)) ⇒ (S0∈A0 ∧ (∀xA, Sx=x+1 ∈AA0)) ⇒ A0=ℕ∎
(As ∧ Min) ⇒ (Ind)
Let A∈Sub{0,S}ℕ, and B = {y∈ℕ* |∀xA, x+yA}.
y,zB, (∀xA, x+yx+y+zA) ∴ y+zB.
(∀xA, x+1 ∈A) ⇔ 1∈B ⇒ ((Min)⇒ B=ℕ*).
0∈A ⇒ (∀yB, 0+yA) ⇒ BA
(F) ⇔ (∀x∈ℕ*, ∀y∈ℕ, x+y y) because x+0 = x ≠ 0.
(Inj ∧ Ind ∧ A1) ⇒ (F) : ∀x∈ℕ*,
x+0 ≠ 0
y∈ℕ, x+y yx+y+1 ≠ y+1∎
For the converse, we need to use the order relation.

### The order relation

From the operation of addition, let us define binary relations < and ≤ on ℕ and show that they form an order and its strict order (even in first order arithmetic); its equivalence with the definition of the order between terms in set theory in the common particular case of ℕ with full set theoretical induction, will be left here as an intuitive fact.

x<y ⇔ ∃z∈ℕ*, y = x+z
xy ⇔ ∃z∈ℕ, y = x+z

These are consequences of (Ind ∧ A1) :
1. < is transitive
2. xy ⇔ (x<yx=y)
3. x<yx+1≤y
4. A⊂ℕ, A≠∅ ⇒ ∃xA, ∀yA, xy (this may also be interpreted either set theoretically or as a schema in first order logic)
5. x,y∈ℕ, xyyx
6. x<yx+z < y+z
Proofs :
1. using (As), x < y < z ⇒ (∃n,p∈ℕ*, z = y+p = x+n+p) ⇒ x <z.
2. obvious from definitions;
3. thanks to (Ind), ℕ is a bijective {0,S}-algebra;
4. xy ⇒ (x+1≤yx=y)
0∈{x∈ℕ |∀yA, xy}=B
xB, x+1∈BxA
AB=∅ ⇒ (B=ℕ ∴ A=∅)
5. from 4. with A={x,y}
6. y = x+n y+z = x+z+n
(for 5. it is also possible to more directly prove for A={x∈ℕ |∀y∈ℕ, x<yx=y y<x} that 0∈A and ∀xA, x+1∈A)

Now, (F) means that < is irreflexive, thus a strict total order thanks to 1. and 5.

Moreover it implies ∀x,y,z∈ℕ, (x<yx+z < y+z) and (x = yx+z = y+z), which gives (Inj) as a particular case.

Proof: the direct implications were shown above; the converses are deduced from there as < is a strict total order : one of (x<y, x = y, y<x) must be true while only one of (x+z<y+z, x+z=y+z, y+z<x+z) can.∎
Finally, ≤ is a total order with strict order < and every nonempty subset of ℕ has a smallest element, which is unique by antisymmetry.

### Arithmetic with order

It is possible to express a first-order arithmetic with language {0,S, ≤}, stronger than {0,S} but weaker than Presburger arithmetic, in the sense that addition cannot be defined from ≤.
Namely, it can be based on the characteristion of the order by the property:
For all n ∈ℕ, the set {x∈ℕ | nx} is the unique A⊂ℕ such that
x∈ℕ, xA ⇔ (x = n ∨∃yA, Sy=x).
Its existence in ℘(ℕ) can be deduced by induction on n; its uniqueness for a fixed n is deduced by induction on x.

Back to homepage : Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
3.1. Morphisms of relational systems and concrete categories
3.2. Special morphisms
3.3. Algebras
3.4. Algebraic terms and term algebras
3.5. Integers and recursion