I need to prove the following statement in natural deduction:

$$(P\rightarrow Q) \lor (Q\rightarrow P)$$

I tried assuming not (target statement) and assuming the left hand side, but I don't know how to continue.

  • 1
    $\begingroup$ Make the case distinction $P \lor \lnot P$. $\endgroup$ – Magdiragdag Feb 4 at 10:16
  • 1
    $\begingroup$ What do you want to prove? There is no statement, it is just a formula. $\endgroup$ – user376343 Feb 4 at 10:30
  • $\begingroup$ How do you need to demonstrate it? Truth-Table? Short truth-table? Truth-tree? Formal proof? Resolution? Davis-Putnam? Equivalences? ... $\endgroup$ – Bram28 Feb 4 at 16:30
  • $\begingroup$ Natural Deduction $\endgroup$ – user9927059 Feb 4 at 16:33
  • 1
    $\begingroup$ @user9927059 So ... basically what Graham Kemp did in his answer? Does his particular system line up with yours? Because even within Natural Deduction there are many different systems with different notations (e.g. see Taroccoesbrocco's answer for a style that looks a good bit different) and different sets of inference rules. $\endgroup$ – Bram28 Feb 4 at 17:57

$P \rightarrow Q$ is equivalent to $\lnot P \lor Q$. So

$(P \rightarrow Q) \lor (Q \rightarrow P)$

is equivalent to

$(\lnot P \lor Q) \lor (\lnot Q \lor P)$

Using the commutative and associative properties of $\lor$ we can show this is equivalent to

$(P \lor \lnot P) \lor (Q \lor \lnot Q)$

which is always True.

  • $\begingroup$ Hello, thank you for your answer. I'll just point out that P->Q is equals to (not P)V Q. Also, I should be able to prove that using only inference rules, but I don't know where to start. I could try proving the equivalency pointed out. $\endgroup$ – user9927059 Feb 4 at 12:07
  • 3
    $\begingroup$ @user9927059: If you have a particular proof system you want to prove your statement in, you ought to describe that system in your question. Otherwise, it's your own doing that people who answer select a style of proof on their own. $\endgroup$ – Henning Makholm Feb 4 at 12:17
  • $\begingroup$ @user9927059 - Good point - I have fixed my answer. $\endgroup$ – gandalf61 Feb 4 at 12:28
  • 2
    $\begingroup$ Natural deduction doesn't usually involve manipulation of equivalent statements like in Boolean Algebra. $\endgroup$ – Doug Spoonwood Feb 6 at 21:56

I tried assuming not (target statement) and assuming the left hand side , but don't know how to continue.

You want to assume $\lnot((P\to Q)\lor(Q\to P))$ and $\lnot(P\to Q)$ to derive $Q\to P$ ... and hence a contradiction.   Thus building a nest of proofs by reduction to absurdity.

$$\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}} \fitch{}{\fitch{\lnot((P\to Q)\lor(Q\to P))}{\fitch{\lnot(P\to Q)}{\fitch{Q}{~\vdots\\P}\\Q\to P\\(P\to Q)\lor (Q\to P)\\\bot}\\\lnot\lnot(P\to Q)\\P\to Q\\(P\to Q)\lor(Q\to P)\\\bot}\\\lnot\lnot((P\to Q)\lor(Q\to P))\\(P\to Q)\lor(Q\to P)}$$

  • $\begingroup$ How did you find P? $\endgroup$ – user9927059 Feb 4 at 14:20
  • $\begingroup$ hint: Explosion! (aka Ex Falso Quodlibet) $\endgroup$ – Graham Kemp Feb 7 at 11:00

Just to complete Graham Kemp's answer: if you assume $\lnot (P \to Q)$ and $Q$, you can easily derive $P$: indeed, if $Q$ holds, then in particular it holds under the additional assumption $P$, thus from $Q$ you can infer $P \to Q$; so, you get a contradiction with the assumption $\lnot (P \to Q)$ and hence, by the principle of explosion or ex falso quodlibet ($\bot_e$), from such a contradiction you can infer whatever you want, in particular $P$.

Formally, the derivation in natural deduction that I described is the following:

\begin{align} \dfrac{\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\dfrac{\lnot (P \to Q) \qquad \dfrac{Q}{P \to Q}\to_i}{\bot}\lnot_e\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!}{P}\bot_e \end{align}

Hence, by discharging the assumption $Q$, you get a proof of $Q \to P$ from the assumption $\lnot (P \to Q)$. Now, you just have to put this derivation into the derivation sketched by Graham Kemp.

  • $\begingroup$ Can I ask the reason of the downvote? $\endgroup$ – Taroccoesbrocco Feb 4 at 22:56

First off, who gave you this problem? Because, I just don't get why you would want to prove this, or really need to prove it. There's a more general tautology that I think makes the suggested formmula as clear as the noonday sun and not needed to formally prove except, perhaps, to indicate that more particular formulas can proved using natural deduction e. g. proving something particular (P$\rightarrow$(P$\rightarrow$P)) instead of the more general (P$\rightarrow$(Q$\rightarrow$P)). I'll prove the more general formula instead:

Second, I'll assume that you can prove (P $\lor$ $\lnot$ P). If you don't have that axiom or don't know how to prove it for your system, I suggest learning how to do that first.

Alright, here I go:

1 Axiom/Lemma (P $\lor$ $\lnot$ P) {}

2 Hypothesis $\lnot$P {2}

3 Hypothesis P {2, 3}

4 contradiction (2, 3) $\bot$ {2, 3}

5 Falsum (4) Q {2, 3}

6 Conditional Introduction (3-5) (P $\rightarrow$ Q) {2}

7 Conditional Intrdouction (2-6) ($\lnot$P $\rightarrow$ (P $\rightarrow$ Q)) {}

8 Hypothesis P {8}

9 Hypothesis R {8, 9}

10 Repitition (8) P {8, 9}

11 Conditional Introduction (9-10) (R $\rightarrow$ P) {8}

12 Conditional Introduction (8-11) (P$\rightarrow$(R$\rightarrow$P)) {}

13 Disjunction Elimination (1, 7, 2) ((P$\rightarrow$Q) $\lor$(R$\rightarrow$P)) {}

Alright, so your system doesn't have all of the rules that I used in exactly the form specified? And maybe you haven't figured out exactly what my rules of inference used? Well, that's a peril of not stating your rules upfront. "Natural deduction" is a term that varies significantly. The only constant in that term, if any, seems that conditional introduction gets used, and as other answers suggest, that might not even be the case any longer (if it ever was).

If this is not a homework problem where you can't use others work, and the above doesn't provide enough clues to construct a proof in your system, then I suggest that you state ever rule in precise detail. I mean precise detail like how your textbook or instructor states those rules. Without that even use of rules like 'conjunction elimination' can get misused. For instance, in the above at step 13 I use a rule which I called 'disjunction elimination'. My rule says that from having three formulas (A$\lor$B), (A$\rightarrow$C), and (B$\rightarrow$D), we can conclude (C$\lor$D). But, it may not work for your system, because your disjunction elimination probably doesn't allow that to get done exactly. My rule is fine, and I can justify it largely by pointing out that in Polish notation, CAabCCacCCbdAcd is a tautology. However, it won't for a proof in a natural deduction system unless that system's disjunction elimination rule or some other rules allow for the step to get made exactly in the way I did so. So, in the future, please state the rules you used up front and state them as exactly as you can.


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.