3.8. Arithmetic with addition

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:

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,yA, x+yA) ⇒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}).

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) in set theory (ignoring our previous definition of ℕ)
Let M=Min{0,S}ℕ.
xM, M∈Sub(ℕ,x,S) ∧ fx=(Myx+y)∈Mor((M,0,S),(ℕ,x,S)).
Images of minimal algebras by morphisms are included in any subalgebras: Im fxM.
As M is stable by + and contains 1, it equals ℕ.∎
(As ∧ Min) ⇒ (Ind) in first-order logic
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 in Presburger arithmetic, let us define binary relations ≤ and < on ℕ and show that they form an order and its strict order (it coincides with the order between terms in the common particular case of the set theoretical ℕ, thanks to the properties of generated preorders) :

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

For this, here are successive consequences of (Ind ∧ A1) :
  1. < is transitive
  2. xy ⇔ (x<yx=y)
  3. x<yx+1≤y
  4. A⊂ℕ, A≠∅ ⇒ ∃xA, ∀yA, xy (to be interpreted as a schema of formulas if we study Presburger arithmetic)
  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). The last formula gives (Inj) as a particular case, and means cancellativity, as sides can be switched thanks to commutativity (deduced from the same assumptions as shown above).

Proof: the direct implications were shown above; the converses are deduced from there as < is a strict total order : one of the 3 formulas (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.

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. Algebras
3.3. Special morphisms
3.4. Monoids
3.5. Actions of monoids
3.6. Categories
3.7. Algebraic terms and term algebras
3.8. Integers and recursion
3.9. Arithmetic with addition
4. Model Theory
4.1. Finiteness and countability