[ Pobierz całość w formacie PDF ]
If we can prove a formula B in predicate calculus using the additional axioms 6
and 7, we will write B. In this case, we say that B is a theorem of E, and
E
that E proves B. It s interesting to note that these two axioms actually do a
pretty good job of describing the way that equality acts. In particular, Axiom
7 captures the sort of substitution steps that are commonly used in elementary
algebra. In this sense, a lot of elementary algebra has more to do with the
equality predicate than with functions or numbers. Here are several instances
of Axiom 7.
3.1. THE THEORY OF EQUALITY 65
x = y ’! (P (x, x, z) ’! P (x, y, z))
y = z ’! (R(y) ’! R(z))
y = z ’! (x = y ’! x = z)
x = y ’! (x = x ’! y = x)
x =2 ’! (x · y =6 ’! 2 · y =6
x = y ’! (x +2=x +2’! x +2=y +2)
Note that Axiom 7 can t be used on quantified variables, so the following
statement is not an instance of Axiom 7: x = y ’! ("xP (x, x, z) ’!"xP (x, y, z)).
Remember that all the axioms of L and K are axioms of E. Consequently, all of
the theorems we proved using L and K are theorems of E. Now it is time to try
our hand at a proof that uses the new axioms.
Theorem E 1. "x"y(x = y ’! y = x) (Mathematicians would paraphrase
E
this by saying equality is symmetric.)
Proof:
1. x = y ’! (x = x ’! y = x) Axiom 7
2. x = x ’! (x = y ’! y = x) L7, line 1
3. "x(x = x) Axiom 6
4. "x(x = x) ’! x = x Axiom 4
5. x = x MP, lines 3 and 4
6. x = y ’! y = x MP, lines 2 and 5
7. "y(x = y ’! y = x) GEN, line 6
8. "x"y(x = y ’! y = x) GEN, line 7
Exercises.
Prove the following in E.
Theorem E 2. x = y ’! (y = z ’! x = z) (This is often called the transitive
E
law of equality.)
Theorem E 3. (x = y '" x = z) ’! y = z (This is an axiom of Euclid:
E
things equal to the same thing are equal to each other.)
Theorem E 4. x = y ’!"z(f(z, x) =f(z, y))
E
Note that Theorem E4 holds regardless of the choice of f(x, z). For example,
we could replace f(x, z) by x + z, x - z, x · z, xz, zx, or any other two place
function.
66 CHAPTER 3. TRANSITION TO INFORMAL PROOFS
3.2 Formal Number Theory
In this section, we will discuss an axiom system for formal number theory.
By formal number theory, we mean a theory that describes arithmetic on the
natural numbers. The mathematical objects we are trying to describe with our
new axioms are the counting numbers {0, 1, 2, ...} and various familiar functions
on them, like addition and multiplication.
Rather than trying to cook up a reasonable set of axioms from scratch, we
can rely on the expertise of some other mathematicians. The following axioms
were used by Kleene [?] and Mendelson [?]. We ll call our axiom system PA,
short for Peano s Axioms for Arithmetic. The function x is read as successor
and is intended to represent x +1.
The axiom system PA consists of the axioms of E and the eight following axioms.
Axiom 8: "x"y(x = y ’! x = y )
Axiom 9: "x(0 = x )
Axiom 10: "x"y(x = y ’! x = y)
Axiom 11: "x(x +0=x)
Axiom 12: "x"y(x +(y ) =(x + y) )
Axiom 13: "x(x · 0 =0)
Axiom 14: "x"y(x · (y ) =(x · y) +x)
Axiom 15: If A(x) is a formula of PA, then
A(0) ’! ("n(A(n) ’! A(n )) ’!"nA(n)).
We can easily paraphrase what these axioms say. Axioms 8, 9 and 10 say
that equality acts the way we expect equality to act related to numbers and
successors. Axiom 9 says that 0 is the least counting number. Axiom 10 says
that 0 is the additive identity. Axioms 11 and 12 outline the behavior of addition,
and Axioms 13 and 14 do the same for multiplication. Axiom 15 says that we
can use induction to prove facts about the counting numbers. All in all, this
seems like a very reasonable list of properties of the natural numbers.
The language of PA is very expressive. That is, lots of properties of the
natural numbers can be written as formulas of PA. Here are some examples.
Example. Each of the following mathematical concepts is presented with its
formalization in PA. Note that these are just formulas representing properties
of natural numbers, not provable statements.
1. x is even: "k(x =2 · k)
(2 is an abbreviation for 0 .)
3.2. FORMAL NUMBER THEORY 67
2. x is odd: "k(x =2 · k +1)
(1 is an abbreviation for 0 .)
3. y|x (y divides x evenly): "k(x = y · k) )
4. x d" y (x is less than or equal to y): "k(x + k = y)
5. x
(k = 0 is an abbreviation for ¬(k = 0.)
6. x is a prime number: 1
(y|x is an abbreviation for "k(x = y · k), as shown in part 3.)
Besides being able to express a multitude of number theoretical concepts,
PA can actually prove gobs of facts about the natural numbers. Here are some
additional statements and their formalizations, each of which can be proved in
PA.
Example. Each of the following mathematical statements is presented with its
[ Pobierz całość w formacie PDF ]