Given the premise P ∨ ¬ Q by natural deduction prove (P → Q) → ((¬ P → Q) → Q)

I am trying to prove this using a Case Proof in Fitch

For my initial subproof, would I be correct in assuming P ∨ Q. I want to deduce implication of P → Q but I am not sure which rule to site. Do I have to break P ∨ Q into Cases of P ∨ Q and cite by elim before I can conclude P → Q.

I think the gap here is how to get from ∨ to → .


  • $\begingroup$ @GitGud I have posted the question the wrong way round. Thanks for your advice re the title. Let me edit my post. $\endgroup$ – Metamorphosis Sep 11 '15 at 14:18

"For my initial subproof, would I be correct in assuming $P \lor Q$?"

This is legal, but I don't see how it could help.

"I want to deduce implication of $P \to Q$".

You can't infer this from $P\lor \neg Q$, nor from $P\lor Q$.

The formula $(P \to Q) \to ((\neg P \to Q) \to Q)$ is a known tautology, therefore you don't need any premises to prove it, (though premises might help shorten the proof). Below I give a proof of this without premises and you can work your way towards shortening it using the given premise.

enter image description here

  • 1
    $\begingroup$ The software I used to write the proof doesn't show all the numbers on row 17, but you can guess what's missing. $\endgroup$ – Git Gud Sep 11 '15 at 14:47
  • $\begingroup$ Thank you very much for this. I am going to spend some time working through this and if I have any questions I will post these all the same. $\endgroup$ – Metamorphosis Sep 11 '15 at 14:50
  • $\begingroup$ @TahliaElcome No problem, ask away. Let me suggest, however, that since you haven't worked through my answer yet, you unaccept it for now. By accepting too early you might discourage other people from answering, perhaps from even giving answers you might like better. After some time, you can and should accept an answer. $\endgroup$ – Git Gud Sep 11 '15 at 14:53
  • $\begingroup$ Valid suggestion. Thanks! $\endgroup$ – Metamorphosis Sep 11 '15 at 15:05

I assume the logic under consideration is classical propositional logic. Since the classical derivability relation is monotone ($S \vdash \varphi, S \subseteq S' \Rightarrow S' \vdash \varphi$) and the empty set is included in every set it, suffices to show that the conclusion is derivable from the empty set

This is easy:

1(1) $P\rightarrow Q$, Assumption

2(2) $\neg P \rightarrow Q$, Assumption

3(3) $\neg Q$, Assumption

4(1,3) $\neg P$, MT 1,3

5(1,2,3) Q, $\rightarrow$-elim 2, 4

6(1,2,3) $Q \wedge \neg Q$, $\wedge$-intro 3, 5

7(1,2) $Q$, RAA, 3, 6

8(1) $(\neg P \rightarrow Q) \rightarrow Q$, $\rightarrow$-intro 2, 7

9( ) $(P\rightarrow Q) \rightarrow ((\neg P \rightarrow Q) \rightarrow Q)$, $\rightarrow$-intro 1, 8

  • $\begingroup$ Thank you for posting this. It is most useful. So this is then a direct proof as oppose to a case proof? $\endgroup$ – Metamorphosis Sep 11 '15 at 17:08

Another approach:

  1. $P\lor \neg Q $ (Premise, 2 cases)

  2. $P\implies Q$ (Premise)

  3. $\neg P \implies Q$ (Premise)

  4. $P$ (Premise, Case 1)

  5. $Q$ (Detach, 2, 4)

  6. $P\implies Q$ (Conclusion, Case 1)

  7. $\neg Q$ (Premise, Case 2)

  8. $\neg Q \implies \neg P$ (Contrapositive, 2)

  9. $\neg P$ (Detach, 8, 7)

  10. $Q$ (Detach, 3, 9)

  11. $\neg Q \implies Q$ (Conclusion, Case 2)

  12. $P \implies Q \implies Q$ (Cases, 1, 6, 11)

  13. $P\implies Q \implies [\neg P \implies Q \implies Q]$ (Conclusion, 2)

  14. $P\lor \neg Q \implies [P\implies Q \implies [\neg P \implies Q\implies Q]$ (Conclusion, 1)


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.