Natural deduction proof help!

Question

I've gone through about 40 natural deduction proofs in the past couple days, and mostly they are no problem. For some reason, I've been stuck on 1 tedious problem for an entire day. I just can't seem to find the proof. Any help would be greatly appreciated.

∃x∃y∀z(x = z ∨ y = z) ⊢ ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))

My attempt ∃x∃y∀z(x = z ∨ y = z) ⊢ ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))

I figured the best way to begin this problem would be to work backwards from the conclusion, choosing random step-numbers for convenience:

5. a = c ∨ b = c
6. ∀z(a = z ∨ b = z) -- ∀-intro (from 5)
7. ¬a = b → ∀z(a = z ∨ b = z) -- →-intro (from 6)
8. ∀y(¬a = y → ∀z(a = z ∨ y = z)) -- ∀-intro (from 7)
9. ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) -- ∀-intro (from 8)

I know that I can assume ¬a = b at some point. So now I have to arrive at a = c ∨ b = c from ∃x∃y∀z(x = z ∨ y = z).

∃-elim here will be tricky. To eliminate ∃x∃y∀z(x = z ∨ y = z), I have to assume ∃y∀z(a = z ∨ y = z) -- or some constant besides a -- and prove a statement without a. But to do that, I must eliminate the ∃y from ∃y∀z(a = z ∨ y = z). To do so, I must assume ∀z(a = z ∨ b = z) -- or some constant besides b -- and prove a statement without b.

Not sure how to proceed from here.

Answer 1

An earlier version of the question had five parts:

1. ∀x(Px ∨ Q) ⊢ (∀xPx ∨ Q)
2. ∀xPx → Q ⊢ ∃x(Px → Q)
3. ∀x∀y(Rxy → ¬x = y) ⊢ ¬∃xRxx
4. ∀x(∃yPxy → ∀yPyx) ⊢ ∃x∃yPxy → ∀x∀yPxy
5. ∃x∃y∀z(x = z ∨ y = z) ⊢ ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))

What remains in the question is only part 5.

---

Too many...

Hint for 1) :

1) ∀x(Px ∨ Q) --- premise

2) Px ∨ Q --- form 1) by ∀-elim

3) ¬Q --- assumed [a]

4) ∃x¬Px --- assumed [b]

5) Q --- assumed [c] from 2) for ∨-elim

6) ⊥ --- contradiction, from 3) and 5)

7) ¬¬Q --- from 3) and 6) by ¬-intro, discharging [a]

8) Q --- from 7) by ¬¬-elim

9) ∀xPx ∨ Q --- from 8) by ∨-intro

10) Px --- assumed [d] from 2) for ∨-elim

11) ¬Px --- assumed [e] from 4) for ∃-elim

12) ⊥ --- contradiction, from 10) and 11) and discharging [e] by ∃-elim

13) ¬∃x¬Px --- from 4) and 12) by ¬-intro, dicharging [b]

14) ∀Px --- from 13) using the sub-derivation ¬∃x¬ ⊢∀x : assume ¬Px, and then ∃x¬Px by ∃-intro. With contradiction, and double negation, derive Px, discharging the assumption, and conclude with ∀xPx by ∀-intro.

15) ∀Px ∨ Q --- from 14) by ∨-intro

16) ∀Px ∨ Q --- from 2) and 5)-9) and 10)-15) by ∨-elim, discharging [c] and [d].

---

---

Hint for 2) :

1) ∀xPx → Q --- premise

2) Px --- assumed [a]

3) ∃x¬Px --- assumed [b]

4) ¬Px --- assumed [c] from 3) for ∃-elim

5) ⊥ --- contradiction, from 2) and 4)

6) ⊥ --- from 3), 4) and 5) by ∃-elim, discharging [c]

7) ¬∃x¬Px --- from 3) and 6) by ¬¬-elim, dicharging [b]

8) ∀Px --- from 7) using the sub-derivation ¬∃x¬ ⊢∀x

9) Q --- from 1) and 8) by →-elim

10) Px → Q$ --- from 2) and 9) by →-intro, discharging [a]

11) ∃x(Px → Q) --- from 10) by ∃-intro.

---

---

Hint for 3) :

1) ∀x∀y(Rxy → ¬x = y) --- premise

2) Rxx --- assumed [a]

3) Rxx → ¬ x = x --- from 1 by ∀-elim

4) ¬ x = x --- from 2) and 3) by →-elim

5) x = x --- axiom for equality

6) ¬Rxx --- from 2) and contradiction, by ¬-intro, discharging [a]

7) ∀x¬Rxx --- from 6) by ∀-intro

Now we have to add the sub-derivation : ∀x¬ ⊢ ¬∃x.

---

---

The last one is long and tedious, but quite straightforward.

Hint for 5) :

1) ∃x∃y∀z(x = z ∨ y = z) --- premise

2) ¬∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- assume the negation of the conclusion and search for a contradiction: if found, the result will follow by ¬¬-elim

3) ∀z(a = z ∨ b = z) --- assumed from 1) for ∃-elim twice

4) ∃x∃y ¬(¬x = y → ∀z(x = z ∨ y = z)) --- from 2), playing again with the quantifiers equivalence

5) ¬(¬c = d → ∀z(c = z ∨ d = z)) --- assumed from 4) for ∃-elim twice

6) ¬c = d ∧ ¬∀z(c = z ∨ d = z) --- from 6) by tautological equivalence

7) ¬c = d --- from 6) by ∧-elim

8) ¬∀z(c = z ∨ d = z) --- from 6) by ∧-elim

9) ∃z ¬(c = z ∨ d = z) --- from 9) again by quantifiers equivalence

10) ¬(c = e ∨ d = e) --- assumed from 9) for ∃-elim

11) ¬c = e ∧ ¬d = e --- from 10) by tautological equivalence

12) ¬c = e --- from 11) by ∧-elim

13) ¬d = e --- from 11) by ∧-elim

Now we have to instantiate 3) ∀z(a = z ∨ b = z) trice, with c,d,e respectively, to get :

14) a = c ∨ b = c

15) a = d ∨ b = d

16) a = e ∨ b = e

and finelly get the desired contradiciton with 7), 12) and 13) (simple but boring application of ∨-elim).

What we get is :

20) ⊥

that closes all the ∃-elim's above, discharging the corresponding assumptions.

21) ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- from 2) and 20) by ¬¬-elim.

Answer 2

An earlier version of the question had five parts:

1. ∀x(Px ∨ Q) ⊢ (∀xPx ∨ Q)
2. ∀xPx → Q ⊢ ∃x(Px → Q)
3. ∀x∀y(Rxy → ¬x = y) ⊢ ¬∃xRxx
4. ∀x(∃yPxy → ∀yPyx) ⊢ ∃x∃yPxy → ∀x∀yPxy
5. ∃x∃y∀z(x = z ∨ y = z) ⊢ ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))

What remains in the question is only part 5.

---

The specifics of your proof will depend on how exactly the prooof system you are working with has defined the rules.

Here are the proofs for 1), 2), 3), and 4) using the Fitch proof system as defined in Language, Proof, and Logic (this is a book and software package):

For 5), you clearly need to do an ∃ Elim on the premise, and a ∀ Intro for the conclusion. For this problem, it actually does not matter in what order you do them. That is, you can either set this up like this:

or like this:

OK, let's just work with the latter. Now, since we're looking for another ∀, we'll do another ∀ Intro:

Now, to get that disjunction, we'll do a proof by Contradiction. Why? Because if you think conceptually about this problem: we know that every object equals either a or b (or both, since a and b may be the same object). So, we know that there are at most two objects in the domain. Therefore, the conclusion makes sense: if there are two different objects c and d, then everything must equal either the one or the other. OK, but how to prove that? Well, take any object e. We know e equals a or b or both. Now, typically, when you go from a disjunction P v Q to a disjunction R v S, you can trace one of the disjunct you want (R) to one of the disjuncts you have (say, Q), while the other disjunct you want (S) comes from the other one you have (P). So, you can do a Proof by cases (v Elim) to do this. But here, that strategy is not going to work: if e = a, can we say that e = c? No. Nor that e = d. Yes, it definitely has to be one or the other, but we just can't tell which one. OK, so a direct Proof by Cases is not going to work. Well, in that case use the other common strategy to prove disjunction: Proof by Contradiction:

OK, and now it should be fairly straightforward. We know that c,d, and e are all a or b, and now it's just a matter of going through all those disjunctions, proving a contradiction each time. Here is the basic set-up:

And here is one half worked out:

Tedious, but pretty straightforward. Good luck!

Answer 3

The premise ∃x∃y∀z(x = z ∨ y = z) says that there exists at most two distinct values in the domain.

The conclusion ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) says that for any two distinct values in the domain, there does not exist a third.

Clearly we need to utilise existential elimination and universal introduction.

∃-elim here will be tricky.

The 'trick' is to use five assumed terms. Two terms as witnesses for the existential eliminations (a, b), and three arbitrary terms for the introductions (c, d, e).

To prove the conclusion from the premise: take the witness for the premise (assume a and b where ∀z(a = z ∨ b = z), take arbitrary values (c, d, and e) and (using universal elimination to each) show that when b, and c are assumed distinct, that it follows that e must be one or the other of those, via some nested disjunction eliminations (and equality eliminations).

In short: Since (a = c ∨ b = c), (a = d ∨ b = d), and (a = e ∨ b = e) via universal elimination, therefore (c = e ∨ d = e)

---

In long: It is tedious and repetitive, but ...

    |_ ∃x∃y∀z(x = z ∨ y = z)                P
    |  |_ [a,b] ∀z(a = z ∨ b = z)           H
    |  |  |_ [c,d]                          H
    |  |  |  a = c ∨ b = c                 ∀E
    |  |  |  a = d ∨ b = d                 ∀E
    |  |  |  |_ ¬c = d                      H
    |  |  |  |  |_ [e]                      H
    |  |  |  |  |  a = e ∨ b = e           ∀E
    |  |  |  |  |  |_ a = e                 H
    |  |  |  |  |  |  |_ a = c              H
    |  |  |  |  |  |  |  c = e             =E
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨I
    |  |  |  |  |  |  +
    |  |  |  |  |  |  |_ b = c              H
    |  |  |  |  |  |  |  |_ a = d           H
    |  |  |  |  |  |  |  |  d = e          =E
    |  |  |  |  |  |  |  |  c = e ∨ d = e  ∨I
    |  |  |  |  |  |  |  +
    |  |  |  |  |  |  |  |_ b = d           H
    |  |  |  |  |  |  |  |  c = d          =E
    |  |  |  |  |  |  |  |  #              ¬E
    |  |  |  |  |  |  |  |  c = e ∨ d = e   X
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨E
    |  |  |  |  |  |  c = e ∨ d = e        ∨E
    |  |  |  |  |  +
    |  |  |  |  |  |_ b = e                 H
    |  |  |  |  |  |  |_ a = c              H
    |  |  |  |  |  |  |  |_ a = d           H
    |  |  |  |  |  |  |  |  c = d          =E
    |  |  |  |  |  |  |  |  #              ¬E
    |  |  |  |  |  |  |  |  c = e ∨ d = e   X
    |  |  |  |  |  |  |  +
    |  |  |  |  |  |  |  |_ b = d           H
    |  |  |  |  |  |  |  |  d = e          =E
    |  |  |  |  |  |  |  |  c = e ∨ d = e  ∨I
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨E
    |  |  |  |  |  |  +
    |  |  |  |  |  |  |_ b = c              H
    |  |  |  |  |  |  |  c = e             =E
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨I
    |  |  |  |  |  |  c = e ∨ d = e        ∨E
    |  |  |  |  |  c = e ∨ d = e           ∨E
    |  |  |  |  ∀z (c = z ∨ d = z)         ∀I
    |  |  |  ¬c = d → ∀z (c = z ∨ d = z)   →I
    |  |  ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) ∀I 
    |  ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))    ∃E