<<

. 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 .)



>>