Topics in Nonstandard Arithmetic 6: The Axioms

Prev TOC Next

This is a “reference” post. With all the posts already filed under Peano Arithmetic, I realize I never explicitly stated the axioms. Of course you can find them on Wikipedia and at a large (but finite) number of other places, but I thought I should put them down somewhere on this site.

Let’s start with the signature. My preference is (0,1,<,+,·). Some people include a function symbol for successor, usually S(x). With 1 as a constant, this is superfluous. On the other hand, some define x≤y as ∃z(x+z=y), and x<y as x≤y∧x≠y. But bounded quantifiers play a fundamental role in the model theory of PA, so I feel it’s better to have < as a built-in relation. (See the Arithmetic Hierarchy posts.)

In the second-order theory of arithmetic (or in set theory), you can define + and · by induction, using successor. That’s how Peano did it! Nowadays ‘PA’ always refers to a first order theory; in that context, neither + nor · can be omitted. Presburger Arithmetic has + but not ·, and unlike PA, it’s decidable.

I’ll give two equivalent sets of axioms, the first more economical than the second. In stating the axioms, I’ll make free use of ‘vernacular’, i.e., formulas that are half-way to being completely formal. (For example, the use of ≠, ≤, >, and the like.)

First set of axioms:

1. ∀x  x+1≠0
2. ∀x∀y ( x+1=y+1 → x=y )
3. ∀x  x+0=x
4. ∀x∀y  x+(y+1)=(x+y)+1
5. ∀x  x·0=0
6. ∀x∀y  x·(y+1)=x·y+x
7. ∀x∀y  ( x<y ↔ ∃w x+(w+1)=y )
8. The Induction Scheme: for any formula ψ(x,y₁,…,y_n) we have

∀y₁…∀y_n [ ψ(0,y₁,…,y_n) ∧ ∀x ( ψ(x,y₁,…,y_n) → ψ(x+1,y₁,…,y_n) )
→ ∀x ψ(x,y₁,…,y_n) ]

It’s either pleasant or tedious to prove consequences like the commutativity of addition and multiplication, using induction. The second set of axioms includes many of these. (These come from Kaye, Chapters 2 and 4.)

1. ∀x∀y∀z  (x+y)+z=x+(y+z)
2. ∀x∀y  x+y=y+x
3. ∀x∀y∀z  (x·y)·z=x·(y·z)
4. ∀x∀y  x·y=y·x
5. ∀x∀y∀z  x·(y+z)=x·y+x·z
6. ∀x  x+0=x
7. ∀x  x·0=0
8. ∀x  x·1=x
9. ∀x∀y∀z ( x<y ∧ y<z → x<z )
10. ∀x ¬x<x
11. ∀x∀y ( x<y ∨ x=y ∨ y<x )
12. ∀x∀y∀z ( x<y → x+z<y+z )
13. ∀x∀y∀z ( z≠0 ∧ x<y → x·z<y·z )
14. ∀x∀y ( x<y → ∃w x+w=y )
15. 0<1 ∧ ∀x ( x>0 → x≥1 )
16. ∀x x≥0
17. The Induction Scheme.

We could replace the Induction Scheme with the Least Number Principle (LNP) in either set of axioms: for any formula ψ(x,y₁,…,y_n) we have

∀y₁…∀y_n [ ∃x ψ(x,y₁,…,y_n) → ∃x ( ψ(x,y₁,…,y_n) ∧ ∀w<x ¬ψ(w,y₁,…,y_n) ) ]

(I don’t know why traditionally you call one a Scheme and the other a Principle.)

PA is not finitely axiomatizable. In other words, no finite subset of the theorems of PA imply all the axioms. Even stronger: a set of theorems that is bounded in the Arithmetic Hierarchy (i.e.,for some n, they all belong to Σ_n(PA)) cannot imply all the axioms. (See Kaye Chapter 10 for a proof.)

Take the second set of axioms and omit the Induction Scheme. The remaining sixteen axioms are called PA^–. They are the axioms for a discretely ordered semiring. Just as you can construct ℤ out of ℕ, you can also construct a discretely ordered ring out of any discretely ordered semiring; conversely, the nonnegative elements of this ordered ring will give you back your original semiring. Kaye’s Chapter 2 has the details.

Finally, I think it’s worth noting that almost all the axioms are universal (∀₁; see post 2). The exceptions are (7) in the first set, and (14) in the second, which are ∀₂ (aka ∀∃), and of course the induction axioms, which go all the way up the hierarchy.

Prev TOC Next