4.5. Presburger Arithmetic
First-order theories of arithmetic
After the formalization of ℕ in set theory,
let us review theories of first-order arithmetic, which means first-order theories
describing ℕ as their only type, and interpreting induction as a schema of axioms by second-order universal elimination
(thus with A only ranging over classes
of that theory). First-order theories with 2 types ℕ and ℘(ℕ), called
second-order arithmetic,
will be studied in Part 5.
Unlike the set theoretical framework, first-order 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 non-standard
models (4.9). So, different choices of language give
non-equivalent versions
of first-order arithmetic, with non-equivalent 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 Z1,
admits symbols 0,S, + and ⋅ , and
all axioms of their definitions. By tedious tricks it
can define recursion (express any recursive sequence (fn(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 un+1 =
f(un,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 first-order axiom schema by second-order 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 (Ind1) be the statement ∀A⊂ℕ*,
(1∈A ∧ (∀x∈A, x+1 ∈A)) ⇒ A=ℕ*.
(Ind1) ⇒ (Ind) and (Ind1) ⇒ (Min) are obvious
(Ind) ⇒ (Ind1) 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) ∈ EndS ℕ
∴ {x+y | y ∈ 〈0〉S} = 〈x〉S
⊂ 〈0〉S
{0,1} ⊂ 〈0〉S ∴
〈0〉S = ℕ ∎
Proof of (As ∧ Min) ⇒ (Ind) directly convertible to first-order 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 well-founded relation is well-founded
(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 first-order 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 first-order 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∈XX
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,
ux = uz}. 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 ux = uy, and this data of
x and y determine the isomorphism class of Y.
A cycle of a transformation f∈XX, is a non-free 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 = IdY
- ∀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 first-order foundations
5. Second-order foundations
6. Foundations of Geometry