3.10. Arithmetic with addition
Firstorder 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 firstorder logic, thus
called firstorder arithmetic. As firstorder 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 firstorder 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 firstorder logic.
This leaves us with several nonequivalent versions of firstorder arithmetic
depending on the choice of the primitive language, thus nonequivalent 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, can finally
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 we shall use set
theoretical notations in such ways that they can be read as abbreviations of works in
firstorder logic: as long as we only consider subsets of ℕ* defined by firstorder 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,b∈A,
∀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 ℕ∋x↦ x+1.
These definitions directly imply (H0).
(Ind) ⇒ (Min) :
∀A⊂ℕ*, the set A_{0}= A∪{0}
satisfies 0∈A_{0} and
(1∈A ∧ (∀x,y∈A, x+y ∈A))
⇒ (S0∈A_{0} ∧ (∀x∈A, Sx=x+1
∈A⊂A_{0})) ⇒ A_{0}=ℕ.∎
(As ∧ Min) ⇒ (Ind) in set theory (ignoring our previous definition of ℕ)
Let M = Min_{{0,S}}ℕ.
∀x∈M, M ∈ Sub(ℕ,x,S) ∧ f_{x} =
(M∋y↦x+y) ∈ Mor_{{S}}(M,ℕ).
Im f_{x} = f_{x} [〈0〉_{{S}}] =
〈x〉_{{S}} ⊂ M.
As M is stable by + and contains 1, it equals ℕ.∎
(As ∧ Min) ⇒ (Ind) in firstorder logic
Let A∈Sub_{{0,S}}ℕ, and B
= {y∈ℕ* ∀x∈A, x+y∈A}.
∀y,z∈B, (∀x∈A, x+y∈A ∴
x+y+z∈A) ∴ y+z ∈B.
(∀x∈A, x+1 ∈A) ⇔ 1∈B ⇒ ((Min)⇒
B=ℕ*).
0∈A ⇒ (∀y∈B, 0+y∈A) ⇒ B⊂A.∎
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+y ≠ y} ∈ 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
x≤y ⇔ ∃z∈ℕ, y = x+z
(A1 ∧ Ind) implies that
 < is transitive
 x≤y ⇔ (x<y ∨ x=y)
 x<y ⇔ x+1≤y
 ∀A⊂ℕ, A≠∅ ⇒ ∃x∈A, ∀y∈A,
x≤y (meaning a schema of formulas in Presburger arithmetic)
 ∀x,y∈ℕ, x≤y ∨ y≤x
 x<y ⇒ x+z < y+z
Proofs :
 using (As), x < y < z
⇒ (∃n,p∈ℕ*, z = y+p = x+n+p)
⇒ x < z.
 obvious from definitions;
 thanks to (Ind), ℕ is a bijective
{0,S}algebra;
 x≤y ⇒ (x+1≤y ∨ x=y)
0∈{x∈ℕ ∀y∈A, x≤y}=B
∀x∈B, x+1∈B ∨ x∈A
A⋂B=∅ ⇒ (B=ℕ ∴ A=∅)
 from 4. with A={x,y}. Or using 3, A={x∈ℕ
∀y∈ℕ, x<y ∨ x=y ∨ y<x}
⇒ (0∈A ∧ ∀x∈A, x+1∈A)
 y = x+n ⇒ y+z = x+z+n
∎
Now the full system (A1 ∧ Ind ∧ F) implies that  < is a strict total order, associated
with the total order ≤
 ∀x,y,z∈ℕ, x<y ⇔ x+z
< y+z
 + is cancellative (which gives (Inj) as a particular case).
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 firstorder 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∈ℕ  n ≤ x} is the unique A⊂ℕ
such that
∀x∈ℕ, x∈A ⇔ (x = n
∨ ∃y∈A, Sy=x).
Its existence in ℘(ℕ) can be deduced in set theory (not firstorder 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
noninjective {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, u_{x} =
u_{y}. This x is unique because y is minimal.
{u_{n}  n<y} ∈ Sub_{{0,S}}K,
thus =K.
As Inj f_{K} ⇔ x=0 ⇔ a∈ Im
f_{K} ⇔ f^{y}(a)=a
⇔ (f_{K})^{y} = Id_{K},
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