## 4.5. Presburger Arithmetic

### First-order 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 first-order theories describing ℕ as their only type, called theories of first-order arithmetic. As first-order 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 first-order 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 first-order logic. This leaves us with several non-equivalent versions of first-order arithmetic depending on the choice of the primitive language, thus non-equivalent 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 Z1, admits symbols 0,S, + and ⋅ , and all axioms of their definitions. It can express any other recursion.

### Presburger arithmetic

A minimal formalization (with the fewest and seemingly weakest axioms that still suffice) 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 first-order logic: as long as we only consider subsets of ℕ* defined by first-order 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,bA,
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 ℕ∋xx+1.
These definitions directly imply (H0).

Let (Ind1) be the statement ∀A⊂ℕ*, (1∈A ∧ (∀xA, x+1 ∈A)) ⇒ A=ℕ*.
(Ind1) ⇒ (Ind) ; (Ind) ⇒ (Ind1) using A∪{0}.
One may instead use {x∈ℕ|x+1∈A} once noted that (Ind) ⇒ Im S = ℕ*.
(Ind1) ⇒ (Min)
(As ∧ Min) ⇒ (Ind) in set theory (ignoring our previous definition of ℕ):
Let M = Min{0,S}ℕ.
xM, M ∈ Sub(ℕ,x,S) ∧ fx = (Myx+y) ∈ Mor{S}(M,ℕ).
Im fx = fx [〈0〉{S}] = 〈x{S}M.
As M is stable by + and contains 1, it equals ℕ.∎
(As ∧ Min) ⇒ (Ind) as directly convertible to first-order logic:
Let A∈Sub{0,S}ℕ, and B = {y∈ℕ* |∀xA, x+yA}.
y,zB, (∀xA, x+yx+y+zA) ∴ y+zB.
(∀xA, x+1 ∈A) ⇔ 1∈B ⇒ ((Min)⇒ B=ℕ*).
0∈A ⇒ (∀yB, 0+yA) ⇒ BA.∎
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+yy} ∈ 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
xy ⇔ ∃z∈ℕ, y = x+z

(A1 ∧ Ind) implies that
1. < is transitive
2. xy ⇔ (x<yx=y)
3. x<yx+1≤y
4. A⊂ℕ, A≠∅ ⇒ ∃xA, ∀yA, xy (meaning a schema of formulas in Presburger arithmetic)
5. x,y∈ℕ, xyyx
6. x<yx+z < y+z
Proofs :
1. using (As), x < y < z ⇒ (∃n,p∈ℕ*, z = y+p = x+n+p) ⇒ x < z.
2. obvious from definitions;
3. thanks to (Ind), ℕ is a bijective {0,S}-algebra;
4. xy ⇒ (x+1≤yx=y)
0∈{x∈ℕ |∀yA, xy}=B
xB, x+1∈BxA
AB=∅ ⇒ (B=ℕ ∴ A=∅)
5. from 4. with A={x,y}. Or using 3, A={x∈ℕ |∀y∈ℕ, x<yx=y y<x} ⇒ (0∈A ∧ ∀xA, x+1∈A)
6. y = x+ny+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<yx+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 first-order 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∈ℕ | nx} is the unique A⊂ℕ such that
x∈ℕ, xA ⇔ (x = n ∨ ∃yA, Sy=x).
Its existence in ℘(ℕ) can be deduced in set theory (not first-order arithmetic) by induction on n; its uniqueness for a fixed n is deduced by induction on x.

### Full arithmetic

It is obtained by adding to the above Presburger arithmetic the operation symbol of multiplication with its defining axioms as presented in 4.3, and expanding the scope of the axiom schema of induction by allowing multiplication in definitions of its variable predicate.

### 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 non-injective {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, ux = uy. This x is unique because y is minimal.
{un | n<y} ∈ Sub{0,S}K, thus =K.
As Inj f|Kx=0 ⇔ a∈ Im f|Kfy(a)=a ⇔ (f|K)y = IdK, 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
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 and countability (draft)
4.7. The Completeness Theorem
4.8. More recursion tools
4.9. Non-standard models of Arithmetic
4.10. Developing theories : definitions
4.11. Constructions