<< ŌūŚšŻšůýŗˇ ŮÚū. 97(ŤÁ 107 ŮÚū.)ő√ňņ¬ňŇÕ»Ň —ŽŚšůĢýŗˇ >>
[Hint: Notice that (R(c, d) ‚ą§ c = c ) ‚Ü’ R(c , d) is one of the H5 axioms of H. So is
(R(c , d) ‚ą§ d = d ) ‚Ü’ R(c , d ). Show that the desired sentence is a tautological consequence
of these two sentences and hence a tautological consequence of H.]

19.9 Let T be a theory of L. Use Proposition 3 (but without using the Completeness Theorem or
 the Elimination Theorem) to show that if a sentence S of L is a Ô¬Ārst-order consequence of
T ‚ą™ H, then it is a Ô¬Ārst-order consequence of T alone.

Section 19.4
The Elimination Theorem
It follows from Proposition 3 that if a sentence S of L is a Ô¬Ārst-order conse-
quence of T ‚ą™ H, then it is a Ô¬Ārst-order consequence of T alone. (This is what
you established in Exercise 19.9.) This result shows that we‚Ä™ve constructed H
in such a way that it doesn‚Ä™t add any substantive new claims, things that give
us new Ô¬Ārst-order consequences (in L) of T . The Elimination Theorem shows
us that our deductive system is strong enough to give us a similar result on
the formal system side of things.

Proposition 4. (The Elimination Theorem) Let p be any formal Ô¬Ārst-order
Elimination Theorem
proof with a conclusion S that is a sentence of L and whose premises are
sentences P1 , . . . , Pn of L plus sentences from H. There exists a formal proof
p of S with premises P1 , . . . , Pn alone.

Chapter 19
The Elimination Theorem / 535

The proof of this result will take up this section. We break the proof down
into a number of lemmas.
Proposition 5. (Deduction Theorem). If T ‚ą™ {P} Q then T P‚Ü’Q Deduction Theorem

The proof of this is very similar to the proof of Lemma 17.2 and is left as an
exercise. It is also illustrated by the following.

You try it
................................................................
1. Open Deduction Thm 1. This contains a formal Ô¬Ārst-order proof of the
following argument:

‚ąÄx (Dodec(x) ‚Ü’ ‚ąÉy Adjoins(x, y))
‚ąÄx Dodec(x)
‚ąÄx ‚ąÉy ‚ąÉz (Adjoins(x, y) ‚ą§ Adjoins(y, z))

According to the deduction theorem, we should be able to give a proof of

‚ąÄx (Dodec(x) ‚Ü’ ‚ąÉy Adjoins(x, y))
‚ąÄx Dodec(x) ‚Ü’ ‚ąÄx ‚ąÉy ‚ąÉz (Adjoins(x, y) ‚ą§ Adjoins(y, z))

We will show you how to do this.
2. Open Proof Deduction Thm 1, which contains only the Ô¬Ārst premise from
the Ô¬Āle Deduction Thm 1. We‚Ä™ll construct the desired proof in this Ô¬Āle.
3. For the Ô¬Ārst step of the new proof, start a subproof with ‚ąÄx Dodec(x) as
premise.
4. Now using Copy and Paste, copy the entire proof (but not the premises)
from Deduction Thm 1 into the subproof you just created in Proof Deduction
Thm 1. After you paste the proof, verify it. You‚Ä™ll see that you need to
add some support citations to get all the steps to check out, but you can
easily do this.
5. End the subproof and use ‚Ü’ Intro to obtain the desired conclusion. Save
your completed proof as Proof Deduction Thm 1.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations
The following is proven using the Deduction Theorem and modus ponens
repeatedly to get rid of each of the Pi . The details are left as an exercise.
Proposition 6. If T ‚ą™ {P1 , . . . , Pn } Q and, for each i = 1, . . . , n, T Pi
then T Q.

Section 19.4
536 / Completeness and Incompleteness

The main step in our proof of the Elimination Theorem is Lemma 9;
Lemmas 7 and 8 help in the proof of Lemma 9. Used judiciously, Lemma 9
will allow us to eliminate the Henkin witnessing axioms from proofs.

Lemma 7. Let T be a set of Ô¬Ārst-order sentences of some Ô¬Ārst-order language
two simple facts
L, and let P, Q, and R be sentences of L.

1. If T P ‚Ü’ Q and T ¬¬P ‚Ü’ Q then T Q.

2. If T (P ‚Ü’ Q) ‚Ü’ R then T ¬¬P ‚Ü’ R and T Q ‚Ü’ R.

Proof: (1) We have already seen that P ‚ą® ¬¬P is provable without
any premises at all. Hence, T P ‚ą® ¬¬P. Thus, our result will follow
from Proposition 6 if we can show that the following argument has
a proof in F :

P ‚ą® ¬¬P
P‚Ü’Q
¬¬P ‚Ü’ Q
Q

But this is obvious by ‚ą® Elim.
The proof of (2) is similar, using Exercises 19.12 and 19.13.

The following lemma shows how certain constants in proofs can be replaced
by quantiÔ¬Āers, using the rule of ‚ąÉ Elim.

Lemma 8. Let T be a set of Ô¬Ārst-order sentences of some Ô¬Ārst-order language
replacing constants
with quantiÔ¬Āers L and let Q be a sentence. Let P(x) be a wÔ¬Ä of L with one free variable and
which does not contain c. If T P(c) ‚Ü’ Q and c does not appear in T or Q,
then T ‚ąÉx P(x) ‚Ü’ Q.

Proof: Assume that T P(c) ‚Ü’ Q, where c is a constant that does
not appear in T or Q. It is easy to see that for any other constant
d not in T , P(x), or Q, T P(d) ‚Ü’ Q. Just take the original proof
p and replace c by d throughout; if d happened to appear in the
original proof, replace it by some other new constant, c if you like.
Let us now give an informal proof, from T , of the desired conclusion
‚ąÉx P(x) ‚Ü’ Q, being careful to do it in a way that is easily formalizable
in F.

Using the method of ‚Ü’ Intro, we take ‚ąÉx P(x) as a premise
and try to prove Q. Toward this end, we use the rule of

Chapter 19
The Elimination Theorem / 537

‚ąÉ Elim. Let d be a new constant and assume P(d). But by
our Ô¬Ārst observation, we know we can prove P(d) ‚Ü’ Q. By
modus ponens (‚Ü’ Elim), we obtain Q as desired.

This informal proof can clearly be formalized within F , establishing
our result. (Exercise 19.16 illustrates this method.)

By combining Lemmas 7 and 8, we can prove the following, which is just
what we need to eliminate the Henkin witnessing axioms.

Lemma 9. Let T be a set of Ô¬Ārst-order sentences of some Ô¬Ārst-order language eliminating witnessing
axioms
L and let Q be a sentence of L. Let P(x) be a wÔ¬Ä of L with one free variable
which does not contain c. If T ‚ą™ {‚ąÉx P(x) ‚Ü’ P(c)} Q and c does not appear
in T or Q, then T Q.

Proof: Assume T ‚ą™ {‚ąÉx P(x) ‚Ü’ P(c)} Q, where c is a constant that
does not appear in T or Q. By the Deduction Theorem,

T (‚ąÉx P(x) ‚Ü’ P(c)) ‚Ü’ Q

By (2) of Lemma 7,
T ¬¬‚ąÉx P(x) ‚Ü’ Q
and
T P(c) ‚Ü’ Q
From the latter, using (1) of Lemma 8, we obtain T ‚ąÉx P(x) ‚Ü’ Q.
Then by (1) of Lemma 7, T Q.

Lemma 9 will allow us to eliminate the Henkin witnessing axioms from
formal proofs. But what about the other sentences in H? In conjunction with
Lemma 6, the next result will allow us to eliminate these as well.

Lemma 10. Let T be a set of Ô¬Ārst-order sentences, let P(x) be a wÔ¬Ä with eliminating other
members of H
one free variable, and let c and d be constant symbols. The following are all
provable in F :
P(c) ‚Ü’ ‚ąÉx P(x)
¬¬‚ąÄx P(x) ‚Ü” ‚ąÉx ¬¬P(x)
(P(c) ‚ą§ c = d) ‚Ü’ P(d)
c=c

Section 19.4
538 / Completeness and Incompleteness

Proof: The only one of these that is not quite obvious from the
rules of inference of F is the DeMorgan biconditional. We essentially
proved half of this biconditional on page 355, and gave you the other
half as Exercise 19.44.

We have now assembled the tools we need to prove the Elimination The-
orem.

Proof of the Elimination Theorem. Let k be any natural number
proof of Elimination
Theorem and let p be any formal Ô¬Ārst-order proof of a conclusion in L, all of
whose premises are all either sentences of L or sentences from H, and
such that there are at most k from H. We show how to eliminate
those premises that are members of H. The proof is by induction
on k. The basis case is where k = 0. But then there is nothing to
eliminate, so we are done. Let us assume the result for k and prove
it for k + 1. The proof breaks into two cases.
Case 1: At least one of the premises to be eliminated, say P, is
of one of the forms mentioned in Lemma 10. But then P can be
eliminated by Lemma 6 giving us a proof with at most k premises
to be eliminated, which we can do by the induction hypothesis.
Case 2: All of the premises to be eliminated are Henkin witnessing
axioms. The basic idea is to eliminate witnessing axioms introducing
young witnessing constants before eliminating their elders. Pick the
premise of the form ‚ąÉx P(x) ‚Ü’ P(c) whose witnessing constant c is
as young as any of the witnessing constants mentioned in the set of
premises to be eliminated. That is, the date of birth n of c is greater
than or equal to that of any of witnessing constants mentioned in
the premises. This is possible since there are only Ô¬Ānitely many such
premises. By the independence lemma, c is not mentioned in any of
the other premises to be eliminated. Hence, c is not mentioned in any
of the premises or in the conclusion. By Lemma 9, ‚ąÉx P(x) ‚Ü’ P(c)
can be eliminated. This gets us to a proof with at most k premises
to be eliminated, which we can do by our induction hypothesis.

Exercises

19.10 If you skipped the You try it section, go back and do it now. Submit the Ô¬Āle Proof Deduction
√‚ Thm 1.

Chapter 19
The Elimination Theorem / 539

Give formal proofs of the following arguments. Because these results are used in the proof of Complete-
ness, do not use any of the Con rules in your proofs.

19.11 19.12 19.13
P‚Ü’Q (P ‚Ü’ Q) ‚Ü’ R (P ‚Ü’ Q) ‚Ü’ R
√‚ √‚ √‚
¬¬P ‚Ü’ Q
¬¬P ‚Ü’ R Q‚Ü’R
Q

19.14 Prove the Deduction Theorem (Proposition 5). [Hint: The proof of this is very similar to the
 proof of Lemma 17.2.]

19.15 Prove Proposition 6. [Hint: Use induction on n and the Deduction Theorem.]

19.16 Use Fitch to open Exercise 19.16. Here you will Ô¬Ānd a Ô¬Ārst-order proof of the following argument:
√‚
‚ąÄx (Cube(x) ‚Ü’ Small(x))
‚ąÄx ‚ąÄy (x = y)
Cube(b) ‚Ü’ ‚ąÄx Small(x)

Using the method of Lemma 8, transform this proof into a proof of

‚ąÄx (Cube(x) ‚Ü’ Small(x))
‚ąÄx ‚ąÄy (x = y)
‚ąÉy Cube(y) ‚Ü’ ‚ąÄx Small(x)

Submit your proof as Proof 19.16.

19.17 Open Exercise 19.17. This Ô¬Āle contains the following argument:
√‚
‚ąÄx (Cube(x) ‚Ü’ Small(x))
‚ąÉx Cube(x)
‚ąÉx Cube(x) ‚Ü’ Cube(c)
Small(c) ‚Ü’ ‚ąÉx Small(x)
¬¬(Cube(c) ‚Ü’ Small(c)) ‚Ü’ ‚ąÉx ¬¬(Cube(x) ‚Ü’ Small(x))
¬¬‚ąÄx (Cube(x) ‚Ü’ Small(x)) ‚Ü” ‚ąÉx ¬¬(Cube(x) ‚Ü’ Small(x))
‚ąÉx Small(x)

First use Taut Con to show that the conclusion is a tautological consequence of the premises.
Having convinced yourself, delete this step and give a proof of the conclusion that uses only
 << ŌūŚšŻšůýŗˇ ŮÚū. 97(ŤÁ 107 ŮÚū.)ő√ňņ¬ňŇÕ»Ň —ŽŚšůĢýŗˇ >>