4.5. Presburger Arithmetic
Firstorder theories of arithmetic
After the formalization of ℕ in set theory,
let us review theories of firstorder arithmetic, which means firstorder theories
describing ℕ as their only type, and interpreting induction as a schema of axioms by secondorder universal elimination
(thus with A only ranging over classes
of that theory). Firstorder theories with 2 types ℕ and ℘(ℕ), called
secondorder arithmetic,
will be studied in Part 5.
Unlike the set theoretical framework, firstorder logic cannot define recursive sequences for
arithmetic from the mere successor function. In particular it cannot proceed the recursive
definitions of addition and multiplication, as will be clear from the description of nonstandard
models (4.9). So, different choices of language give
nonequivalent versions
of firstorder arithmetic, with nonequivalent versions of the schema of induction:

Bare arithmetic, with the mere symbols 0 and S, is very poor.
 Presburger
arithmetic, detailed below, 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. By tedious tricks it
can define recursion (express any recursive sequence (f^{n}(a))_{n∈ℕ} as a predicate with variables n and a using the
given definition of f), and more generally the sequence defined by
any condition of the form u_{n+1} =
f(u_{n},n) expressed in its language.
Presburger arithmetic
Its usual presentations have
primitive symbols 0, +, and either 1 or S which are definable from each other (1 =
S0 and Sx =
x+1) ; actually + would suffice to define all.
Among its equivalent
formalizations, a very short one which superficially looks weakest, 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) 
The axiom (Min), expressed for simplicity in set theory where it makes 1 a generator of (ℕ*,+),
is then reduced to a firstorder axiom schema by secondorder universal elimination. It will be
seen equivalent to the axiom of induction, both set theoretically and as axiom schemas.
(A1) is a particular case of the associativity
axiom (As).
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) ⇒ commutativity, as deduced from 1∈C({1}).
Now take ℕ = ℕ*∪{0} where 0∉ℕ*, to which + is extended as ∀n∈ℕ,
0+n = n+0 = n. This extension is still commutative and associative.
With S_{ℕ} defined as x↦ x+1, obviously
(H0) holds. As x+0 = x ≠ 0,
(F) ⇔ (∀x∈ℕ*, ∀y∈ℕ, x+y ≠ y)
(Inj ∧ Ind ∧ A1) ⇒ (F) because ∀x∈ℕ*,
{y∈ℕ  x+y ≠ y} ∈ Sub_{{0,S}}ℕ .
The proof of the converse (F ⇒ Inj) using other axioms, will come from the study of
the order relation.
Equivalence of axiom schemas
Let (Ind_{1}) be the statement ∀A⊂ℕ*,
(1∈A ∧ (∀x∈A, x+1 ∈A)) ⇒ A=ℕ*.
(Ind_{1}) ⇒ (Ind) and (Ind_{1}) ⇒ (Min) are obvious
(Ind) ⇒ (Ind_{1}) either by using A∪{0},
or {x∈ℕx+1∈A} once noted that (Ind) ⇒ Im S = ℕ*.
Proof of (A1 ∧ Min) ⇒ (Ind) in set theory (ignoring our previous definition of ℕ):
∀x∈〈0〉_{S}, +⃗(x) ∈ End_{S} ℕ
∴ {x+y  y ∈ 〈0〉_{S}} = 〈x〉_{S}
⊂ 〈0〉_{S}
{0,1} ⊂ 〈0〉_{S} ∴
〈0〉_{S} = ℕ ∎
Proof of (As ∧ Min) ⇒ (Ind) 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.
The order relation
In Presburger arithmetic,
let us define binary relations ≤ and < as x<y ⇔ ∃z∈ℕ*, y =
x+z
x≤y ⇔ ∃z∈ℕ, y = x+z
(A1 ∧ Ind) implies
 < is transitive
 ∀x,y∈ℕ, x≤y ⇔ (x<y ∨ x=y)
 ∀x∈ℕ*,∃y∈ℕ, x = y + 1
(ℕ is a surjective
{0,S}algebra)
 ∀x,y∈ℕ, x<y ⇔ x+1≤y
 ∀x,y,z∈ℕ, x<y ⇒ x+z < y+z
 (schema) ∀A⊂ℕ, A≠∅ ⇒ ∃x∈A, ∀y∈A,
x≤y
 ∀x,y∈ℕ, x≤y ∨ y≤x
Proofs :
 using (As), x < y < z
⇒ (∃n,p∈ℕ*, z = y+p = x+n+p)
⇒ x < z.
 obvious from definitions;
 by (Ind)
 from 3.
 y = x+n ⇒ y+z = x+z+n
∎

repeats the proof that the transitive closure of a wellfounded relation is wellfounded
(3.12), without assuming Inj which would make it a particular case.
To forget +, let
S = {(x,y)∈ℕ^{2}x+1 = y}.
From 2. and 4., ∀(x,y)∈S, ∀z∈ℕ,
x≤z ⇒ (y≤z ∨ x=z)
0∈{x∈ℕ ∀z∈A, x≤z}=B
∀(x,y)∈S,
x∈B ⇒ (y∈B ∨ x∈A)
By (Ind), A∩B = ∅ ⇒ (B = ℕ ∴ A = ∅).
 from 6. with A={x,y}. Or using 3.,
A = {x∈ℕ
 ∀y∈ℕ, x<y ∨ x=y ∨ y<x}
⇒ (0∈A ∧ ∀x∈A, x+1 ∈ A)
(A1 ∧ Ind ∧ F) implies < 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) gives irreflexivity ; other conditions for a strict total order come from 1. and 7.
There must be one true formula among (x<y),
(x
= y), (y<x), which by 5. 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.
∎
In the set theoretical ℕ, this order coincides with the order
between terms with either language {S} or {0,S}.
Also, for each n ∈ℕ, the set <⃗(n) ⊂ ℕ can be seen as recursively defined by
¬(n<0) ∧ ∀x∈ℕ, n < Sx ⇔ (x = n ∨ n < x)
which can also be written
∀x∈ℕ, x ∈ ≤⃗(n) ⇔ (x = n
∨ ∃y∈ ≤⃗(n), Sy=x).
(Its existence in ℘(ℕ) can be deduced by induction on n,
more simply than other recursions)
Parity
Presburger arithmetic can qualify a number n∈ℕ as even by
∃x∈ℕ, n = x+x; and odd
by ∃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. Then it can be shown by (Ind) that any n must be either even or odd, and
by also using (Inj) that it cannot be both and that this x is unique.
Taken as primitive with a relevant set of axioms, the order relation can form a variant of firstorder arithmetic
more expressive than bare arithmetic, but less than Presburger arithmetic, as it suffices to define S but
cannot suffice to define +
(nor parity) and cannot be defined from S in firstorder logic.
Images of recursive sequences
In set theory with axiom of infinity, the image of a recursive sequence u = (f^{
n}(a))_{n∈ℕ} by a transformation f∈X^{X}
is a trajectory Y = 〈a〉_{f} = Im u of an action of (ℕ,0,+) on E.
As + is commutative, Y gets a
monoid structure with identity a and generator f(a), that is a quotient of ℕ.
The injectivity of u (that would make it an isomorphism from ℕ to Y) is equivalent to
the injectivity (H0) ∧ (Inj) of the {0,S}algebra structure of Y.
If u is not injective, let y = min{z∈ℕ  ∃x<z,
u_{x} = u_{z}}. Then the restriction of u to <⃖(y)
is bijective to Y (its image is Y because it is {0,S}stable). Then there is a unique
x<y such that u_{x} = u_{y}, and this data of
x and y determine the isomorphism class of Y.
A cycle of a transformation f∈X^{X}, is a nonfree trajectory Y
= 〈a〉_{f} for some a∈X, such that,
equivalently (using the above defined x and y),
 x = 0
 Inj f_{Y}
 f_{Y} ∈ 𝔖_{Y}
 f^{ y}(a) = a
 a∈ Im f_{Y}
 (f_{Y})^{y} = Id_{Y}
 ∀b∈Y, Y = 〈b〉_{f}
Then this y, independent of the chosen generator a of Y, is called the period
of Y.
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
3. Algebra 1
4. Arithmetic and firstorder foundations
5. Secondorder foundations
6. Foundations of Geometry