Tautology with Natural Deduction

Question

I'm trying to prove (p->q) v (q->p) is a tautology. I need to start with an assumption, I would start with p->q or q->p but I always get stuck in the assumption. I don't find any way to get out of it to have a disjunction as a 'conclusion'.

Answer 1

You have to use Excluded Middle : $q \lor \lnot q$.

From $q$ derive $p \to q$ by $\to$-intro, followed by $(p \to q) \lor (q \to p)$ by $\lor$-intro.

From $\lnot q$, assuming $q$, derive $p$ by EFQ and then $q \to p$ by $\to$-intro, discharging $q$. Then, again, $(p \to q) \lor (q \to p)$ by $\lor$-intro.

The conclusion follows from EM by $\lor$-elim.

Answer 2

HINT

Use a Proof by Contradiction. So, your assumption would be that this statement is not true ... and then show that that assumption leads to a contradiction.

Answer 3

This answer uses the law of the excluded middle as Mauro ALLEGRANZA suggested, but puts a proof in the Fitch-style format.

To use the law of the excluded middle (LEM) in this proof checker I need to consider two contradictory cases, $Q$ and $\lnot Q$, and derive the desired result, $(P \to Q) \lor (Q \to P)$, from both cases in separate subproofs. The first case was considered on lines 1-5 and the second on lines 6-11. After getting the same result I could use the LEM rule on line 12 referencing both subproofs.

In the first case, I used reiteration (R), conditional introduction (→I) and disjunction introduction (vI). In the second case, I used contradiction introduction (⊥I), explosion (X), conditional introduction (→I) and disjunction introduction (vI).

More information about the inference rules and the proof checker can be found in the links below.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018.