3

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:

  1. a = c ∨ b = c
  2. ∀z(a = z ∨ b = z) -- ∀-intro (from 5)
  3. ¬a = b → ∀z(a = z ∨ b = z) -- →-intro (from 6)
  4. ∀y(¬a = y → ∀z(a = z ∨ y = z)) -- ∀-intro (from 7)
  5. ∀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.

  • Comments are not for extended discussion; this conversation has been moved to chat. – Keelan May 30 '18 at 7:26
4

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.

  • Is the move from step 1-2 in problem 3 allowed? I thought that in using ∀-elim, you'd have to choose two different constants--∀x∀y(Rxy → ¬x = y) would go to Rab → ¬a = b and not Raa → ¬a = a; you keep x instead of substituting for a constant, which works exactly the same. So you're allowed to substitute in the same constant when using ∀? – vundabar May 27 '18 at 11:22
  • 2
    @vundabar -Yes, it works. ∀x means "for all" thus ∀x∀yRxy → ∀yRay → Raa. – Mauro ALLEGRANZA May 27 '18 at 11:57
  • That makes me life much easier. I am also curious how your sub-derivation ∀x¬∃x¬ ⊢∀x rule works? I've never seen it before. – vundabar May 27 '18 at 12:00
  • Sorry, I figured you meant ∀x¬ ⊢ ¬∃x but I still don't get how the rule works. It seems like some kind of shortcut, but I don't see how either that or the ¬∃x¬ ⊢∀x rule from problem 2 works. – vundabar May 27 '18 at 12:29
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.


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

enter image description here

enter image description here

enter image description here

enter image description here

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:

enter image description here

or like this:

enter image description here

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

enter image description here

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:

enter image description here

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:

enter image description here

And here is one half worked out:

enter image description here

Tedious, but pretty straightforward. Good luck!

  • I never make use of assume the opposite of what I'm proving and make use of ¬-elim. Thank you, it's a great strategy. Would this help on 4 as well? – vundabar May 27 '18 at 14:33
  • @vundabar Yes, see my edit. – Bram28 May 27 '18 at 14:39
  • I realized how to do 3 right after posting and updated it to ask about number 4. Sorry about that! – vundabar May 27 '18 at 14:45
  • @vundabar Hmm, just glancing at it I think you can do a direct proof for that one .. but let me check the details! – Bram28 May 27 '18 at 14:49
  • thank you! I've updated my original post to show my attempt so far. – vundabar May 27 '18 at 14:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.