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 as the set theoretical framework was involved to justify recursive definitions, the successor function no more suffices to define addition and multiplication in first-order logic. 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 we shall use set theoretical notations in such ways that they can be read as abbreviations of works in first-order logic: as long as we only consider subsets of ℕ* defined by first-order formulas in this arithmetical language, (Ind) and (Min) can be read as abbreviations of schemas of statements, 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{S}(M,ℕ).
Im fx = fx [〈0〉{S}] = 〈x{S}M.
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.∎
So, all possible axiom pairs are equivalent: (A1 ∧ Min) ⇔ (As ∧ Min) ⇔ (As ∧ Ind) ⇔ (A1 ∧ Ind), and imply commutativity.
Now (F) ⇔ (∀x∈ℕ*, ∀y∈ℕ, x+y y) because x+0 = x ≠ 0.
(Inj ∧ Ind ∧ A1) ⇒ (F) because ∀x∈ℕ*, {y∈ℕ | x+yy} ∈ Sub{0,S}ℕ .
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

(A1 ∧ Ind) implies that
  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}. Or using 3, A={x∈ℕ |∀y∈ℕ, x<yx=y y<x} ⇒ (0∈A ∧ ∀xA, x+1∈A)
  6. y = x+ny+z = x+z+n
Now the full system (A1 ∧ Ind ∧ F) implies that Proof. (F) means that < is irreflexive, which with transitivity (1.) implies that it is a strict order, which is total by 5.
There must be one true formula among (x<y), (x = y), (y<x), which by 6. respectively imply (x+z<y+z), (x+z = y+z), (y+z<x+z). But only one of the latter can be true, thus each implication must be an equivalence. Cancellativity on one side extends to the other side by commutativity. ∎
Finally, by 4., every nonempty subset A of ℕ has a smallest element (unique by antisymmetry), written min A.
This order coincides with the order between terms in the common particular case of the set theoretical ℕ, as will be clear from the properties of generated preorders.

Arithmetic with order

It is possible to express a first-order arithmetic with language {0,S, ≤}, more expressive than {0,S} but less than Presburger arithmetic, in the sense that addition cannot be defined from ≤.
There, ≤ is related to S by the following property (which determines it in set theory, but no more in bare arithmetic due to the poverty of its interpretation of induction by an axiom schema):
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 in set theory (not first-order arithmetic) by induction on n; its uniqueness for a fixed n is deduced by induction on x.

Trajectories of recursive sequences

For any recursive sequence u∈Mor(ℕ,(E,a,f)), the trajectory K = Im u = {f n(a) | n∈ℕ} of an action of ℕ on E is generated by a, which is a free element for the image of ℕ as a transformation monoid of K thanks to the commutativity of +. Therefore K can be seen as a commutative monoid, whose description coincides with the above arithmetic without axiom (F), where the roles of the neutral element 0 and the generator 1 are respectively played by a and f(a). However for convenience, let us focus on the set theoretical viewpoint on the remaining case, when u is not injective so that K is not a copy of ℕ. Then K must be a non-injective {0,S}-algebra: there must be a pair in {0,S}⋆K mapped to a singleton, but we shall see that such a pair is unique.
Let y the minimal number such that ∃x<y, ux = uy. This x is unique because y is minimal.
{un | n<y} ∈ Sub{0,S}K, thus =K.
As Inj f|Kx=0 ⇔ a∈ Im f|Kfy(a)=a ⇔ (f|K)y = 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. Then replacing a by another element of 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