The first explicit attempts to axiomatize whole number arithmetic were made near the end of the 19th century. The most famous presentations of such axioms are Dedekind's 1888 book, Was sind und was sollen die Zahlen [1] and Peano's Arithmetices Principia Novo Methodo Exposita [10] of 1889. Peano listed four truths about equality and five special postulates for the positive integers. His special postulates were, [7, page 473,]:
Our axioms for ordered rings replace Peano's postulates 1 - 4. Peano's 5th postulate which has come to be known as the axiom of induction is the subject of this Section.
Peano is using here a somewhat antiquated language about
properties. We translate his word property to mean
set and
we say that a number belongs to a set rather than a set
belonging to a number. This is just a matter of convention.
We would express his axiom using second order logic as introduced
on page 
as
Again, this axiom is only supposed to refer to the positive integers.
Another way to phrase this same axiom is to say that the empty set is the only set of positive integers with no least element. This is the version that will be most useful for us. Translated to the domain of all integers, positive, negative, and zero, this becomes, ``Any non-empty set with a lower bound has a least element.'' Writing this as a logical formula gives us our axiom of induction:
This axiom uses the abbreviation, 
as shorthand
for 
.
This may not seem like a very exciting theorem since it is so obviously true. The reader should keep in mind however that our task is to present a logical analysis, not to actually do number theory. We have an axiom system and if it is adequate, it must be able to prove the obvious facts as well the more esoteric ones. So our real purpose in proving this theorem is not to show that it is true, but rather that it is a logical consequence of the axioms. Besides, the analysis of its proof gives us a chance to introduce plenty of logic.
We begin our analysis of this proof by translating the statement
of the theorem into formal logic. There are many equivalent ways
one could read this theorem. I shall choose the one requiring
the most logical analysis. So one could say that it means,
where again 
is an abbreviation for 
so that, according to axiom 10 on page
, 
is equivalent to
y < x.
The proof is a proof by contradiction. We begin by adding the negation of the theorem to our data base of facts and adopt the goal of trying to prove a contradiction. Usually this means deducing enough facts to add to the data base so that some statement and its negation are both facts. Going for a proof by contradiction has one big advantage and one big disadvantage. The advantage is that we have an extra fact to work with. The disadvantage is that the goal is kind of vague. With the goal just being, ``Find some contradiction,'' we cannot work backwards from that goal very easily until we have a better idea as to just which contradiction we are seeking. So we must really begin with some forward argument.
The new fact to add to the data base is the negation of the theorem,
When faced with a fact like this it is almost always advisable to ``move the negation sign into the formula.'' This means replacing the formula by an equivalent formula in which the negation sign does not come right at the beginning. There are very specific rules about how this is done. Here they are.
We can apply rule 1 to replace (2.16) by the equivalent fact,
Then use rule 4 to push the negation sign in still further, replacing (2.17) by,
We can now apply the 
-left-(P)
rule on page
to (2.18) using the new variable b to get,
It is our intention to use (2.19) to deduce
that 
is non-empty.
There is a problem however. Our logical symbolism does not
yet include the richness necessary to name this set. Nor
does it include the axioms necessary for proving anything about
sets. We can overcome this in an extremely simple and
direct manner. A constant symbol is just a string of symbols
we wish to use in a certain way, so declare the string,
, to be a constant symbol in the universe of
sets and add to our
axiom list the two new axioms,
Of course, it would be somewhat ad hoc to do this just
for this one set. We need to add axioms for every possible
formula. If A(x) is a formula and
x is the only free variable of A(x),
we declare 
to be a constant symbol for the
universe of sets and add to our axiom base two axioms
corresponding to (2.20) and
(2.21). This will suffice for all the
applications we will present, but the reader should be
warned that it is not enough to fully exploit the induction
axiom. For the full system, we must allow A(x) to have
free variables other than x. Then would no
longer be a constant symbol but would have to be a function
symbol. We will not go into details.
So with axiom (2.20) and fact
(2.19) we can use the 
-left-(P)
rule to deduce 
and so, applying
the -right-(P) rule,
Now we need to prove the other hypothesis of the induction axiom,
Using -right-(P), we can replace this goal
with the new goal:
To prove this goal, use the -right-(P)
rule and the 
-right-(P)
rule. In other words, introduce a new variable, c, and
assume 
in order to prove
0 < c. This goal follows easily using axiom
(2.21) with the -left-(P)
and -left-(P) rules.
Now use the -left-(P) rule on the induction
axiom (2.15),
putting the term in for X. Then combine
the result with (2.22) and (2.23). Apply
the -left-(P) (with new variable a)
and 
-left-(P)
rules to the result to get the two new facts,
From (2.25) and axiom (2.21)
it follows that 0 < a < 1. We can now use
-left-(P) on axiom 13 to deduce
that 
. This is a clear contradiction
with what we get by putting 
in for x in (2.26),
completing the proof.
As far as logic is concerned, the new feature of this proof
is that we used the
fact that either n is prime or it is not prime. Another
logical law you may use in a proof is the Law of the excluded middle. It says
that you may at any time add any fact of the form 
to the data base of facts. Such facts of course get
used with the 
-left-(P) rule which says that
you break the proof down into two subproofs, one using A
as a fact, the other using 
.
Our proof of the next theorem uses the factorial function,
n!. This function is defined by induction for all integers
with the equations:
0! = 1
There does not appear to be any real good way to include such functions into our logical symbolism. The only feasible way is to make up a new function symbol, ! and add it to the language of arithmetic and then add axioms to define it. So we must add the axioms,
This concludes our excursion into number theory. I hope the reader has been enlightened by our sometimes painful analysis of the obvious.
iff 
iff 
iff 
iff 
iff 
iff A
