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:

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,yA, x+yA) ⇒ 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) : (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 xx+1, obviously (H0) holds. As x+0 = x ≠ 0,

(F) ⇔ (∀x∈ℕ*, ∀y∈ℕ, x+y y)

(Inj ∧ Ind ∧ A1) ⇒ (F) because ∀x∈ℕ*, {y∈ℕ | x+yy} ∈ 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 ∧ (∀xA, 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 ℕ): Proof of (As ∧ Min) ⇒ (Ind) directly convertible to first-order logic: 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
xy ⇔ ∃z∈ℕ, y = x+z

(A1 ∧ Ind) implies
  1. < is transitive
  2. x,y∈ℕ, xy ⇔ (x<yx=y)
  3. x∈ℕ*,∃y∈ℕ, x = y + 1 (ℕ is a surjective {0,S}-algebra)
  4. x,y∈ℕ, x<yx+1≤y
  5. x,y,z∈ℕ, x<yx+z < y+z
  6. (schema) ∀A⊂ℕ, A≠∅ ⇒ ∃xA, ∀yA, xy
  7. x,y∈ℕ, xyyx
Proofs :
  1. using (As), x < y < z ⇒ (∃n,p∈ℕ*, z = y+p = x+n+p) ⇒ x < z.
  2. obvious from definitions;
  3. by (Ind)
  4. from 3.
  5. y = x+ny+z = x+z+n
  6. 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∈ℕ, xz ⇒ (yzx=z)
    0∈{x∈ℕ |∀zA, xz}=B
    ∀(x,y)∈S, xB ⇒ (yBxA)
    By (Ind), AB = ∅ ⇒ (B = ℕ ∴ A = ∅).
  7. from 6. with A={x,y}. Or using 3.,
    A = {x∈ℕ | ∀y∈ℕ, x<yx=y y<x} ⇒ (0∈A ∧ ∀xA, x+1 ∈ A)
(A1 ∧ Ind ∧ F) implies 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 = nn < 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)


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 fXX is a trajectory Y = 〈af = 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 fXX, is a non-free trajectory Y = 〈af for some aX, such that, equivalently (using the above defined x and y),

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
4.1. Algebraic terms
4.2. Quotient systems
4.3. Term algebras
4.4. Integers and recursion
4.5. Presburger Arithmetic
4.6. Finiteness
4.7. Countability and Completeness
4.8. More recursion tools
4.9. Non-standard models of Arithmetic
4.10. Developing theories : definitions
4.11. Constructions
4.A. The Berry paradox
5. Second-order foundations
6. Foundations of Geometry