3.12. Presburger Arithmetic
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 review firstorder theories describing ℕ as their only type, called theories
of 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 is arithmetic with addition. It still
cannot define multiplication.
 Full arithmetic, named Z_{1},
admits symbols 0,S, + and ⋅ , and
all axioms of their definitions. It
can express any other recursion.
Presburger arithmetic
A minimal formalization describes the set ℕ* of nonzero natural
numbers, with symbols 1 (constant) and + (binary operation), and axioms :
∀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).
Let (Ind_{1}) be the statement ∀A⊂ℕ*,
(1∈A ∧ (∀x∈A, x+1 ∈A)) ⇒ A=ℕ*.
(Ind_{1}) ⇒ (Ind) ; (Ind) ⇒ (Ind_{1}) using A∪{0}.
One may instead use {x∈ℕx+1∈A} once noted that (Ind) ⇒ Im S = ℕ*.
(Ind_{1}) ⇒ (Min)
(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) as directly convertible to 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.
Parity
A number n∈ℕ is even if ∃x∈ℕ, n=x+x; it is odd
if ∃x∈ℕ, n=x+x+1.
Obviously, if n is even then n+1 is odd; if n is odd then n+1 is even thanks to commutativity. Thus by induction, any number is either even or odd.
But to show that it cannot be both and that this x is unique, also requires the use of
(Inj). These are left as a possible exercise. But instead of (Inj) we proposed axiom (F).
This raises the question of their equivalence.
(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. Initial and final objects
3.9. Algebraic terms
3.10. Term algebras
3.11. Integers and recursion
3.12. Presburger Arithmetic
4. Model Theory
4.1. Finiteness
and countability