PineWikiThe Peano axioms define the NaturalNumbers: { 0, 1, 2, 3, ... }. They can be written in a number of ways; here is a simple version that uses only the constant 0 and a function symbol S(x), where y = S(x) is interpreted as "y is the successor of x" or "y = x+1". (Note that since the axioms don't define addition, we can't just say that y=S(x) is equivalent to y=x+1.)
- ∀x ¬(S(x)=0). "Zero is not the successor of any number."
- ∀x ∀y (S(x)=S(y) ⇒ x=y). "If two numbers are equal, their predecessors are equal."
plus the induction schema, which represents infinitely many axioms obtained by filling in your choice of P:
- (P0 ∧ ∀x Px ⇒ P(S(x))) ⇒ ∀x Px.
This says that if any property holds for zero, and if in addition the fact that the property holds for some number n means that it holds for n+1, then we can deduce from this that it holds for all numbers.
Without the first axiom, we could have a model where zero is its own successor (and no other numbers exist). It's easy to check that this satisfies the other axioms: Zero has a successor, it is its own predecessor, and as soon as P(0) holds we can conclude ∀x Px without bothering with the rest of the induction schema.
Without the second axiom, we could have just two numbers 0 and 1, with S(0)=1 and S(1)=1. By throwing it in (or the logically equivalent "if x does not equal y, then x's successor does not equal y's successor), we guarantee that we get an infinite sequence of numbers by repeatedly looking for successors.
Without the induction schema, we could get extra numbers that aren't reachable starting from 0. So we need that too.
Very technical note: there are "non-standard" models of the Peano axioms that sneak in some extra numbers that just happen to satisfy all the predicates that are satisfied by all the standard numbers. Unless we also add a new predicate that isn't covered by the induction schema (e.g. Bogus(x) that is only true for the extra numbers), we can't distinguish between these non-standard models and the ordinary one. So we will generally assume we are working with the usual natural numbers and ignore the paranoid possibility that a few extra numbers are hiding with perfect camouflage up around infinity somewhere.
1. Example
Let's show that every number except 0 is the successor of some number. Formally, we want
- ∀x (x=0 ∨ ∃y x=Sy).
Proof: We'll use the induction schema expanded on the above to get
- (0=0 ∨ ∃y 0=Sy) ∧ ∀x ((x=0 ∨ ∃y x=Sy) ⇒ ((Sx=0) ∨ ∃y Sx=Sy)) ⇒ ∀x (x=0 ∨ ∃y x=Sy).
Now we just need to prove the left-hand side. We have 0=0 from reflexivity, so the first premise holds. For the second premise, observe that ∃y Sx=Sy since we can just choose y=x.