1
$\begingroup$

I'm just starting out in natural deduction. So I have a question now how to prove the following.

Prove that $\vdash (P \Rightarrow Q) \lor (Q \Rightarrow P)$

I'm finding this rather difficult cause, normally I would know what to assume to get to my goal. But in this case I do not know how to even proceed. Any help or insights is deeply appreciated.

Thank you for reading my post

$\endgroup$
  • 1
    $\begingroup$ Here's a hint, the proposition is not provable in constructive logic. $\endgroup$ – Derek Elkins Jan 31 '16 at 5:01
  • $\begingroup$ @DerekElkins: Intuitionistic logic you mean, but that's almost surely not helpful. The asker said he's "just starting out". To user2875613: What Derek is referring to is that the law of excluded middle is not provable in intuitionistic logic, nor is double negation elimination, both of which I used in my answer. $\endgroup$ – user21820 Jan 31 '16 at 5:05
  • $\begingroup$ @user21820 I use "constructive logic" as a near synonym of intuitionistic logic that's slightly less specific. Indeed the first line of the Wikipedia article is "Intuitionistic logic, sometimes more generally called constructive logic". Also, while user2875613 may not immediately know the reference, a quick google search would turn it up and the significance, and then the OP would be aware of it in the future. $\endgroup$ – Derek Elkins Jan 31 '16 at 5:10
  • $\begingroup$ @DerekElkins: Sure, but my opinion is that it's better not to introduce too many different formal systems when one hasn't even gotten used to one. $\endgroup$ – user21820 Jan 31 '16 at 5:15
  • $\begingroup$ I proved something similar to this result here: math.stackexchange.com/a/3124414/312852 $\endgroup$ – Frank Hubeny Feb 24 at 3:42
1
$\begingroup$

In general, when you don't know how to begin, for classical logic you can use law of excluded middle. The exact details depend on which particular version of natural deduction you have, but it should be easy to translate. $\def\imp{\Rightarrow}$

Solution

If $P$:

  If $Q$:

    $P$.

  $Q \imp P$.

If $\neg P$:

  If $P$:

    Contradiction.

    If $\neg Q$:

      Contradiction.

    $\neg \neg Q$.

    $Q$.

  $P \imp Q$.

[I've left the easy remainder for you to fill in.]

Proof of Law of Excluded Middle

If $\neg (P \lor \neg P)$:

  If $P$:

    $P \lor \neg P$.

    Contradiction.

  $\neg P$.

  $P \lor \neg P$.

  Contradiction.

$\neg \neg (P \lor \neg P)$.

$P \lor \neg P$.

$\endgroup$
  • $\begingroup$ Sorry, I'm abit confused here. So first you assume P and at the end of the assumption, you concluded P => (Q=>P). Then you assume ¬P and concluded ¬P => (P => Q). but P and ¬P came to a different conclusion. I'm not sure how to proceed from there. Also in your assumption of ¬P, you arrived at a contradiction of ¬Q, could you explain that part too ? $\endgroup$ – some1fromhell Jan 31 '16 at 9:57
  • $\begingroup$ @user2875613: Well what did you want the prove in the first place? Wasn't it $(P \imp Q) \lor (Q \imp P)$? Can you see what to fill in to the solution to get it? Of course you'd have to do something under each of "If $P$" and "If $\neg P$" so that you can pull the conclusion out using disjunction elimination and law of excluded middle. $\endgroup$ – user21820 Jan 31 '16 at 11:30
  • $\begingroup$ @user2875613: For your other question, once you get a contradiction it means that the currently active assumptions cannot hold so under any further assumption it is still impossible. It fits with the intuition that you can pull any assertion into any inner assumption, including a false assertion, which you can consider "Contradiction" to denote. $\endgroup$ – user21820 Jan 31 '16 at 11:31
  • $\begingroup$ @user2875613: So do you get it or not? $\endgroup$ – user21820 Feb 2 '16 at 12:31

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.