[ Pobierz całość w formacie PDF ]
Exercises.
1. Prove:
Theorem K 13. "xA(x) ’!"xA(x)
2. Consider the theorem:
Theorem K 14. "yA(y) ’!"xA(x)
(a) Prove K14 using the deduction theorem, Axiom 4 and K13.
(b) Prove K14 using the Add "x Rule.
3. Prove:
Theorem K 15. "x(A(x) (" B(x)) ’! ("xA(x) (""xB(x))
4. Prove the following theorems. Like the proof of Theorem K11, these re-
sults use the fact that "xA(x) is an abbreviation for ¬"x¬A(x). Math-
ematicians use results like these whenever they push negations past a
quantifier.
(a)
Theorem K 16. ¬"xA(x) "x¬A(x)
(b)
Theorem K 17. "x¬A(x) ¬"xA(x)
(c)
Theorem K 18. "x¬A(x) ¬"xA(x)
(d)
Theorem K 19. ¬"xA(x) "x¬A(x)
2.17 Removing "x
So far, we have strategies for adding and removing "x, and a rule for adding
"x. To complete our survey of techniques for manipulating quantifiers, we need
a rule for removing "x.
Informally, if we have "xA(x), we should be able to find some element to
plug in for x. If we give that element a temporary name, we could proceed
with our proof. The best thing to use as a name is a constant symbol. If we
use a constant symbol that already appears in the proof (or appears in some
weird axioms that we plan to use later), we will be implicitly making additional
assumptions about the element. Consequently, we want to use a new constant
symbol. Here s the rule, presented more formally.
Rule C: If "xA(x) is a previous line in a proof, we may write A(c) as a line,
provided that the following two conditions hold.
2.17. REMOVING "X 59
1. c is a new constant symbol. (That is c doesn t show up in any earlier
lines of the proof, of in any proper axioms we ever plan to use.)
2. If some variable (say y) appears free in the formula "xA(x), then
GEN is never applied to y in the proof.
Here is an example of using Rule C in a proof.
Theorem K 20. "x(A(x) '" B(x)) "xA(x)
1. "x(A(x) '" B(x)) Given
2. A(c) '" B(c) Rule C, line 1
3. (A(c) '" B(c)) ’! A(c) Rule T
4. A(c) MP, lines 2 and 3
5. "xA(x) Add "x Rule, line 4
Why do we need the second condition in Rule C? We need to worry about
GEN and Rule C for the same reason that we worry about GEN and the De-
duction Theorem. If we do a proof with Rule C and break the second condition,
our conclusion may not be sound. For example, consider the following incorrect
proof of "x"y(x = y) from "y(y = y).
1. "y(y = y) Given
2. "y(y = y) ’! y = y Axiom 4
3. y = y MP, lines 1 and 2
4. "x(x = y) Add "x Rule, line 3
5. c = y Rule C, line 4
6. "y(c = y) Illegal use of GEN
7. "x"y(x = y) Add "x Rule, line 6
In line 4, y = y is the result of substituting y for every free occurrence of x
in x = y, and y is free for x in x = y, so this line is a legal application of the
Add "x Rule. Indeed, this is just like the second line in the proof of K12 with
x = y substituted for A(x, y). We pull the substitution trick with the Add "x
Rule again in line 7. It is legal there, too. The only illegal step is in line 6,
where we apply GEN to a variable that appears free in line 4, the formula to
which we applied Rule C. That violates the second condition of Rule C, and it
is a very bad idea. There is a model where "y(y = y) is true, but "x"y(x = y)
is false, so "y(y = y) does not logically imply "x"y(x = y). The illegal use of
GEN with Rule C has destroyed the soundness of our proof system.
We ve seen the bad effects of violating the conditions of Rule C. However,
if we can prove A using Rule C correctly, then we can prove A without using
60 CHAPTER 2. PREDICATE CALCULUS
Rule C. Consequently, correct uses of the shortcut Rule C do not mess up the
completeness and soundness theorems for our proof system. One way to prove
this is to construct an algorithm that converts proofs that use the shortcut
to proofs that do not. This sort of argument closely resembles a proof of the
deduction theorem, and is used in [?].
Exercises.
Use Rule C to prove the following:
Theorem K 21. "xA(x) ’!"x(A(x) (" B(x))
Theorem K 22. "x"yA(x, y) ’!"y"xA(x, y)
Theorem K 23. "x(A(x) ’! B(x)) ’! ("xA(x) ’!"xB(x))
Theorem K 24. "xB(x) ’!"x(A(x) ’! B(x))
Theorem K 25. ¬"xA(x) ’!"x(A(x) ’! B(x)) (Hint: Use K19)
Theorem K 26. ("xA(x) ’!"xB(x)) ’!"x(A(x) ’! B(x)) (Hint: Use
K24 and K25, rather than Rule C.)
2.18 Proof strategies in predicate calculus
Predicate calculus looks a lot like propositional calculus, except for the addition
of quantifiers. We have some excellent tools for dealing with quantifiers. To
add "x we use GEN, and to add "x we use the aptly named Add "x Rule. To
remove "x we use Axiom 4, and to remove "x we use Rule C. A very rough
overall strategy for doing proofs in predicate calculus is:
" Rip off the quantifiers. [ Pobierz całość w formacie PDF ]
zanotowane.pl doc.pisz.pl pdf.pisz.pl chiara76.opx.pl
Exercises.
1. Prove:
Theorem K 13. "xA(x) ’!"xA(x)
2. Consider the theorem:
Theorem K 14. "yA(y) ’!"xA(x)
(a) Prove K14 using the deduction theorem, Axiom 4 and K13.
(b) Prove K14 using the Add "x Rule.
3. Prove:
Theorem K 15. "x(A(x) (" B(x)) ’! ("xA(x) (""xB(x))
4. Prove the following theorems. Like the proof of Theorem K11, these re-
sults use the fact that "xA(x) is an abbreviation for ¬"x¬A(x). Math-
ematicians use results like these whenever they push negations past a
quantifier.
(a)
Theorem K 16. ¬"xA(x) "x¬A(x)
(b)
Theorem K 17. "x¬A(x) ¬"xA(x)
(c)
Theorem K 18. "x¬A(x) ¬"xA(x)
(d)
Theorem K 19. ¬"xA(x) "x¬A(x)
2.17 Removing "x
So far, we have strategies for adding and removing "x, and a rule for adding
"x. To complete our survey of techniques for manipulating quantifiers, we need
a rule for removing "x.
Informally, if we have "xA(x), we should be able to find some element to
plug in for x. If we give that element a temporary name, we could proceed
with our proof. The best thing to use as a name is a constant symbol. If we
use a constant symbol that already appears in the proof (or appears in some
weird axioms that we plan to use later), we will be implicitly making additional
assumptions about the element. Consequently, we want to use a new constant
symbol. Here s the rule, presented more formally.
Rule C: If "xA(x) is a previous line in a proof, we may write A(c) as a line,
provided that the following two conditions hold.
2.17. REMOVING "X 59
1. c is a new constant symbol. (That is c doesn t show up in any earlier
lines of the proof, of in any proper axioms we ever plan to use.)
2. If some variable (say y) appears free in the formula "xA(x), then
GEN is never applied to y in the proof.
Here is an example of using Rule C in a proof.
Theorem K 20. "x(A(x) '" B(x)) "xA(x)
1. "x(A(x) '" B(x)) Given
2. A(c) '" B(c) Rule C, line 1
3. (A(c) '" B(c)) ’! A(c) Rule T
4. A(c) MP, lines 2 and 3
5. "xA(x) Add "x Rule, line 4
Why do we need the second condition in Rule C? We need to worry about
GEN and Rule C for the same reason that we worry about GEN and the De-
duction Theorem. If we do a proof with Rule C and break the second condition,
our conclusion may not be sound. For example, consider the following incorrect
proof of "x"y(x = y) from "y(y = y).
1. "y(y = y) Given
2. "y(y = y) ’! y = y Axiom 4
3. y = y MP, lines 1 and 2
4. "x(x = y) Add "x Rule, line 3
5. c = y Rule C, line 4
6. "y(c = y) Illegal use of GEN
7. "x"y(x = y) Add "x Rule, line 6
In line 4, y = y is the result of substituting y for every free occurrence of x
in x = y, and y is free for x in x = y, so this line is a legal application of the
Add "x Rule. Indeed, this is just like the second line in the proof of K12 with
x = y substituted for A(x, y). We pull the substitution trick with the Add "x
Rule again in line 7. It is legal there, too. The only illegal step is in line 6,
where we apply GEN to a variable that appears free in line 4, the formula to
which we applied Rule C. That violates the second condition of Rule C, and it
is a very bad idea. There is a model where "y(y = y) is true, but "x"y(x = y)
is false, so "y(y = y) does not logically imply "x"y(x = y). The illegal use of
GEN with Rule C has destroyed the soundness of our proof system.
We ve seen the bad effects of violating the conditions of Rule C. However,
if we can prove A using Rule C correctly, then we can prove A without using
60 CHAPTER 2. PREDICATE CALCULUS
Rule C. Consequently, correct uses of the shortcut Rule C do not mess up the
completeness and soundness theorems for our proof system. One way to prove
this is to construct an algorithm that converts proofs that use the shortcut
to proofs that do not. This sort of argument closely resembles a proof of the
deduction theorem, and is used in [?].
Exercises.
Use Rule C to prove the following:
Theorem K 21. "xA(x) ’!"x(A(x) (" B(x))
Theorem K 22. "x"yA(x, y) ’!"y"xA(x, y)
Theorem K 23. "x(A(x) ’! B(x)) ’! ("xA(x) ’!"xB(x))
Theorem K 24. "xB(x) ’!"x(A(x) ’! B(x))
Theorem K 25. ¬"xA(x) ’!"x(A(x) ’! B(x)) (Hint: Use K19)
Theorem K 26. ("xA(x) ’!"xB(x)) ’!"x(A(x) ’! B(x)) (Hint: Use
K24 and K25, rather than Rule C.)
2.18 Proof strategies in predicate calculus
Predicate calculus looks a lot like propositional calculus, except for the addition
of quantifiers. We have some excellent tools for dealing with quantifiers. To
add "x we use GEN, and to add "x we use the aptly named Add "x Rule. To
remove "x we use Axiom 4, and to remove "x we use Rule C. A very rough
overall strategy for doing proofs in predicate calculus is:
" Rip off the quantifiers. [ Pobierz całość w formacie PDF ]