3.10. Arithmetic with addition

First-order theories of arithmetic

Our first formalization of ℕ was based on the framework of set theory, using the powerset to determine the isomorphism class of ℕ. This allowed recursion, from which addition and multiplication could be defined.

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

In any model of Presburger arithmetic, let us define binary relations ≤ and < as

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

Let us show that they form an order and its strict order (which coincides with the order between terms in the common particular case of the set theoretical ℕ, thanks to the properties of generated preorders). First, 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 (meaning a schema of formulas in 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 by 4., every nonempty subset A of ℕ has a smallest element (unique by antisymmetry), written min A.

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.

Trajectories of recursive sequences

A trajectory K = Im u where u= (f n(a))n∈ℕ is a copy of ℕ as soon as it is an injective {0,S}-algebra.
Let us look at the rest of cases (there will turn out to be only one pair in {0,S}⋆K mapped to a singleton).
Let y the minimal number such that ∃x<y, ux= uy. This x is unique because y is minimal.
The restriction of u to Vy is injective; its image being stable, equals K.
As Inj f|Kx=0 ⇔ a∈ Im f|Kfn(a)=a ⇔ (f|K)n = IdK, a trajectory K where these are true is called a cycle of f with period y; the restriction of f to K is then a permutation of K.
Picking another element a in such a K would leave both K and y unaffected.
Now if f is a permutation then every cycle of f is also a cycle of f -1 with the same period.

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. Invertibility and groups
3.7. Categories
3.8. Algebraic terms and term algebras
3.9. Integers and recursion
3.10. Arithmetic with addition
4. Model Theory
4.1. Finiteness and countability