One of the basic topics in the theory of numbers is the relationship between the way a number is built up with addition and the way it is built up with multiplication. This study was begun in Euclid and in this section we want to analyze the very first theorem on number theory proved in Euclid.
We begin with a definition.
This simple proof raises a host of logical issues. Let us begin
with the definition. It is phrased in English. It uses some technical
language, but it is still English. However, we should have no trouble
in recognizing that the English is really just a variant of the formal
language we introduced in Chapter 1. The definition introduced
a new relation symbol, |, and defined a | b with the formula,
There are several ways of incorporating such
definitions into formal
logic. The one I propose to adopt is that definitions introduce
abbreviations for longer formulas. So that when we use a | b in
a logical formula, we do not have an actual formula, but rather an
abbreviation for an actual formula. Thus, for instance, the statement
of the theorem is not an actual formula, but is rather an abbreviation
for the somewhat more cumbersome
Note that we were forced into using a somewhat tricky process for
expanding the definition. The definition used the variable c
which was in conflict with the use of the same letter in the abbreviated
formula. But there is no magic in the use of any particular variable
as the target of a quantifier, 
or 
. The formula,
means exactly the same thing as 
. We can state a rule governing the expansion of
a formula using definitions:
In expanding a definition used in an abbreviated formula, first change the names of all the bound variables used in the definition in order to avoid conflict with any symbolic names used in the abbreviated formula.
We now come to the theorem itself. But before going into details
we need to enquire into the overall structure of proof in general.
Most proofs are constructed using what Solow [15] calls
the forward-backward method.
At every stage of the proof, we have
a data base of facts and we have goals. The facts consist of axioms,
theorems already proven from those axioms, things deduced from the
axioms in the course of the given proof, and temporary assumptions
made during the proof. The goals are a list of things to prove. In
progressing through the proof, we can either work forward from
the facts, that is to say, deduce more facts, or we can work
backwards from the goals. Working back from the goals consists
of finding new goals from which the old goals can be deduced. (I
need to prove B, but I know 
so let me replace
the goal B with the goal A.)
Theorem 1 starts
with the axioms of number theory as its only source of facts.
These axioms consist of the basic algebraic axioms together
with one more axiom, the axiom of induction. We will introduce
induction in Section 2.2 so for now let us content ourselves
with stating the algebraic axioms. To repeat, the language of
arithmetic as introduced on page 
uses the
constant symbols; 0, 1, 2, ...; the two binary function symbols;
; the unary function symbol, -, and the two binary
relation symbols, =, <. The algebraic axioms are those axioms for
ordered fields from page which do not use the
symbol 
. This includes all the equality axioms on page
as well as:
In addition, we must define the constant symbols with axioms. This
group of axioms consists of the infinite number of axioms such as
31 + 23 = 54 and 
. The entire addition and
multiplication tables for integer arithmetic must be included.
The goal (the statement of the theorem) uses an abbreviation technique common
through all of mathematics. It
uses free variables, a and b, with the obvious expectation that
they are to be universally quantified, but it does not explicitly use
quantifiers.
This is common practice. When a mathematician uses a formula with
free variables as if it were a sentence, the reader is supposed to
understand that there are implicit universal quantifiers being used.
Thus, in formal logic we would have to make the theorem more explicit
and translate it as
The next step in our analysis is to begin the proof. Since the
goal is a universally quantified statement, the proof must begin
with the question, ``How can one prove a sentence?''
The answer to this question was first
formulated by Aristotle himself. Essentially all it does is to revert
to the ordinary usage that we have just removed. The way to prove
is to choose a new variable which does not
occur freely in any of the facts in the current data
base (let us call it new_constant) and
then adopt
as the new goal. Thus we see that the usual
mathematical convention is really just a matter of skipping one
step in the proof.
In our case, we can even use the variables a, b, and c
because they do not occur freely anywhere. We get the sentence
and it is now our goal to prove this. Since we have no facts using the names a, b, or c, we can interpret these three variables in any way we want without destroying the facts. Thus proving the goal will show it to be true for all a, b, and c.
In order to prove the goal (2.3),
observe that it is an implication, . The usual procedure for
proving such a statement is to assume A and prove B. That is to
say, add A to the data base of facts and adopt B as the new goal.
This gives a | (b+c) as the new goal. Remember however that in this
form it is not an actual formula, since it contains
an abbreviation which has to be expanded:
At this point we can ask ourselves, ``How does one prove an existential
statement, 
?''
The answer however is somewhat disappointing. The usual method is to
choose some term t and prove A(t). But in this case it is not at
all clear what term to use. In fact, there is no term to use. We must
turn to the forward direction of the proof and use the data base of facts.
We have the two existential facts,
How can we use them? An existential fact is very much like a
universal goal. To use the fact, , choose a
new variable (one not occurring freely in the the goal or in
any fact in the data base) and replace
the assumption by 
.
Let us use the new constant u to apply this procedure to
(2.5). We thus replace (2.5)
with the new fact, 
. Since u is not used in any
of the axioms or the goal, we are free to interpret it in any way
we want, so after a and b have been interpreted to satisfy
(2.5), just interpret u to be the number that
(2.5) asserts to exist. That will
make 
true and so if we can prove the goal using
this fact, it too will be true. Now carry out the same
process for (2.6). When we do this of course,
the symbol u is no longer new so we must make up yet another new
symbol, v. Thus the above two assumptions become
It is now time to use an axiom, the equality axiom
A universal fact is similar to an existential goal. The way to
use the fact, is to create the new fact
A(t) where t is any term you wish to use. In our case,
we wish to substitute for x in (2.9).
We see at once that there is a problem, (2.9) already
uses the variable u. If we just blindly substitute for
x, we get,
which is not at all what we had in mind. The situation is similar to
our above situation with definitions. In order to use an instance of
a fact, you must change names of the bound variables in
the fact in order to avoid a clash with the free variables used in
the instance. Doing this with (2.9), we change u to
in (2.9) and make the substitution of
for x to get,
Applying this rule three more
times to (2.9), we get the new fact,
From this and our earlier assumptions, we can conclude
We also have the fact,
as an instance of the distributive law and
as an instance of the third equality axiom.
Combining the last three statements, we get
So finally it should be clear that we have a term to use in (2.4). Replace that goal by substituting the term u+v for x to get the goal (2.14) which is proven. This completes the proof.
The reader should now go back to our original proof of Theorem
1 and see how all the parts of our
somewhat long-winded expansion of this proof were used there.
One real difference is that in actual mathematics no one bothers
to be as explicit about the use of equality laws as we have been.
For instance, we said that 
and 
and therefore
. In real life you would never see anything
so pedantic as that. What you would see is 
with no further explanation.
Also, the original proof did not go into the steps of refining the goal; it just worked forward from the hypotheses to the conclusion without bothering to explain the guiding principles which lead to making just that series of deductions and no others. This is often done in simple proofs like this, but in more difficult real mathematics the backward process is often explicitly included in the proof.
In summary we can list the rules of logic used in the above
proof. They fall into two categories, how to refine the goal
and how to use facts. One can think of the goals as being
written to the right of the facts so that the corresponding rules
might be called right rules and left rules
respectively. So for instance our above rule for proving
a goal would be the -right rule
and our rule for using a fact would be the
-left rule.
This notation would however be in conflict with the more
precise formal rules we shall be presenting in
Chapter . So let us instead
call them instead the -right-(P) rule
and the -left-(P) rules where the P
stands for Preliminary. Here are the rules we used:
-right-(P))
, use a new variable, c, and
prove A(c). Here the word ``new'' means not occurring
freely in either the data base or in .
-right-(P))
, You may adopt as a new goal A(t) where
t is any term you may wish to use and bound variables in A
have been renamed to avoid any clash with the variables of
t. As we saw in the example, this rule
sometimes has to be delayed until the forward process has
created the term you need.
-right-(P))
, you may add A to the data base of facts
and then use this enlarged data base to prove the goal B.
-left-(P))
, you may add A(c) to the data base where
c is a new variable.
-left-(P))
, you may add to the data base any sentence of the form A(t)
where t is a term and bound variables in A
have been renamed to avoid any clash with the variables of
t. A(t) is called an instance of
.
-left-(P))
, you may deduce the new
fact, B.
-left-(P))
, you may deduce the two separate
facts, A and B, and vice versa.
To be complete we should add the left and right rules for the
other connectives, the -right-(P) rule, both
rules and the 
rules. The -right-(P)
and -left-(P) rules are dual to each other. Both
split the proof into two subproofs.
-right-(P)
, prove each of
A and B separately.
-left-(P)
, first prove your
goal using A, then prove it again using B.
We will not state the negation rules in the same format
as the other rules. To deal with a negated formula, either
as a goal or a fact, you simplify it using the rules given
on page . There is no really good way
to express the -right-(P) rule
in the current context. It will be much easier to deal with
it after we have set up the whole proof structure
differently so as to fully incorporate the duality between
left and right. Until then the best we can
do is say that to prove a goal of the form, , you
should probably change the goal to either 
or 
, whichever one works.
Let us call the
equality axioms from page
together with the
algebraic axioms on page
the axioms
of ordered rings and let us say that a model for these
axioms is an ordered ring.
These
axioms do not in any way characterize integer arithmetic
since for instance both the real numbers and the rational
numbers are ordered rings.
