Prove :(P → Q) ∨ (Q → P) using natural deduction

Question

Allowed inference rules: ∨-I, ∨-E, ∧-I, ∧-E, →-I, →-E, ¬-I, ¬-E

I tried to prove a contradiction by assuming $¬ ((P → Q) ∨ (Q → P))$ but got stuck, or am I doing it in the wrong way?

Edit:

My proof attempt

$1.\qquad¬ ((P → Q) ∨ (Q → P))\qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad Assum$

$2.\qquad P → Q\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\ Assum$

$3.\qquad(P → Q) ∨ (Q → P)\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\; ∨-I(2)$

$4.\qquad(¬ ((P → Q) ∨ (Q → P))) ∧ ((P → Q) ∨ (Q → P))\qquad\qquad\qquad\; ∧-I(1,3)$

$5.\qquad ¬ (P → Q)\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\;\;\; ¬-I(2,4)$

$6.\qquad Q → P\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad\qquad\quad\; Assum$

$7.\qquad (P → Q) ∨ (Q → P)\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\;\; ∨-I(6)$

$8.\qquad (¬ ((P → Q) ∨ (Q → P))) ∧ ((P → Q) ∨ (Q → P))\qquad\qquad\qquad\;\; ∧-I(1,7)$

$9.\qquad ¬ (Q → P)\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\; ¬-I(6,8)$

$10.\qquad ¬ (P → Q) ∧ ¬ (Q → P)\qquad\qquad\qquad\qquad\qquad\qquad\;\qquad\qquad\quad\;\;\, ∧-I(5,9)$

Stuck at this line, can't spot any contradiction to line 1

Answer 1

Your start is good:

$1.\qquad¬ ((P → Q) ∨ (Q → P))\qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad Assum$

$2.\qquad \qquad P → Q\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\ Assum$

This second assumption is good too, since you basically want to do a DeMorgan on line 1, and to do those in Natural Deduction, you do a Proof by COntradiction on each of the disjuncts .. so yes, assume the disjunct, but then proceed with getting the full disjunct:

$3.\qquad\qquad (P → Q) ∨ (Q → P) \qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad \lor Intro \: (2)$

and now you can get a contradiction with line 1:

$4.\qquad \qquad\bot \qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad \qquad \qquad\qquad\qquad \bot \: Intro \: (1,3)$

So you can close the subproof and get:

$5.\qquad \lnot(P → Q) \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \lnot Intro \: (2-4)$

OK, same pattern with the other disjunct, i.e. repeat those same 4 lines:

$6.\qquad \qquad Q → P\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\ Assum$

$7.\qquad \qquad (P → Q) ∨ (Q → P) \qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad \lor Intro \: (6)$

$8.\qquad\qquad \bot \qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad \qquad \qquad\qquad\qquad \bot \: Intro \: (1,7)$

$9.\qquad \lnot(Q → P) \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \lnot Intro \: (6-8)$

OK, we know that $\lnot (P \rightarrow Q) \equiv P \land \lnot Q$, so we should be able to get $P$ from 5, and $\lnot P$ from 9, giving us the desired contradiction. How do we prove that? It's not too hard: two more proofs by contradiction! That is, to get $P$, assume the opposite:

$10.\qquad \qquad\lnot P \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\ Assum$

And since we want this to contradict with $\lnot (P \rightarrow Q)$, try and prove $P \rightarrow Q$, which we do with a conditional proof:

$11.\qquad\qquad\qquad P \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\ Assum$

$12.\qquad \qquad\qquad\bot \qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad \qquad \qquad\qquad \bot \: Intro \: (10,11)$

$13.\qquad \qquad\qquad\ Q \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \bot \: Elim \: (12)$

$14.\qquad\qquad P → Q\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\ \rightarrow \: Intro (11-13)$

$15.\qquad\qquad \bot \qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad \qquad \qquad\qquad\qquad \bot \: Intro \: (5,14)$

$16.\qquad \lnot \lnot P \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \lnot \: Intro \: (10-15)$

$17.\qquad P \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \lnot \: Elim \: (16)$

Almost there! Do a similar pattern to get $\lnot P$ from 9:

$18.\qquad \qquad P \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\ Assum$

$19.\qquad\qquad\qquad Q \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\ Assum$

$20.\qquad \qquad\qquad\ P \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad Reit \: (18)$

$21.\qquad\qquad Q → P\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\ \rightarrow \: Intro (11-13)$

$22.\qquad\qquad \bot \qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad \qquad \qquad\qquad\qquad \bot \: Intro \: (9,21)$

$23.\qquad \lnot P \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \lnot \: Intro \: (18-22)$

And now we're done:

$24.\qquad \bot \qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad \qquad \qquad\qquad\qquad\qquad \bot \: Intro \: (17,23)$

$25.\lnot \lnot ((P → Q) ∨ (Q → P))\qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad\qquad \lnot Intro (1-24)$

$26. (P → Q) ∨ (Q → P)\qquad \qquad\qquad\qquad\qquad\qquad\qquad \qquad\qquad\qquad \lnot Elim (25)$

OK, so it turns out to be a somewhat lengthy proof, but that often happens with Natural Deduction, where we don;t have handy dandy equivalence rules. However, notice that between the set-ups for conditional proof, conditional proof, etc, as well as the repeating patterns for doing things like Demorgan, you end up cranking out these proofs on automatic pilot once you have done them for a while. And finally, oftentimes the instructor, book, or software will start to allow you to simply refer to those patterns as Lemma's, so you don't have to write them out every time.

Answer 2

When you have to prove a disjunction ('or'), there are typically 3 strategies:

1. You already have one of the disjuncts. OK, then use $\lor$ Intro to get the full disjunction.

2. You have some other disjunction to work with. When this is the case, iot often is the case that one of the disjuncts you have will lead to one of the disjuncts you want, while the other disjunct you have will lead to the other disjunct you want. So, a proof by cases (typically captured by the $\lor$ Elim) will be your strategy.

3. If you have neither one of the disjuncts already, nor have a disjunction to work with, then often a proof by contradiction is a good strategy.

You are clearly dealing with case 3, since you don't have anything to work with. So, yes, your idea of doing a proof by contradiction is good. If you tell us how you got stuck, we can help you more. Can you show what you have and where you got stuck?

Answer 3

The formula is valid only in classical logic.

Thus, to prove it we have to use Excluded Middle or Double Negation.

With LEM :

1) $\vdash P \lor \lnot P$

2) $P$ --- assumed [a] from 1) for $\lor$-E

3) $Q \to P$ --- from 2) by $\to$-I

4) $(P \to Q) \lor (Q \to P)$ --- from 3) by $\lor$-I

5) $\lnot P$ --- assumed [b] from 1) for $\lor$-E

6) $P$ --- assumed [c]

7) $\bot$ --- from 5) and 6)

8) $Q$ --- from 7)

9) $P \to Q$ --- from 6) and 8) by $\to$-I, discharging [c]

10) $(P \to Q) \lor (Q \to P)$ --- from 9) by $\lor$-I.

Having derived $(P \to Q) \lor (Q \to P)$ both from 2) and 5) we may conclude with :

$\vdash (P \to Q) \lor (Q \to P)$

by $\lor$-I from 1), discharging [a] and [b].

Answer 4

I am not sure I understand what is done here, but can I prove ├ (A->B) v (B->A like this:

9.[A] (-> introduction, can be canceled from 4.)

8.(B->A) (v introduction)

7.[¬((A->B) v (B->A))] (A->B) v (B->A)

6.⊥

5.B (-> introduction)

4.(A->B) (v introduction)

3.[¬((A->B) v (B->A))] (A->B) v (B->A)

2.⊥ RAA

1.├ (A->B) v (B->A)