(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