Proving $\vdash (p\to q)\lor (q\to r)$ using natural deduction

Question

I'm trying to prove the following:

$\vdash (p\to q)\lor(q\to r)$

using only intuitionistically valid rules. I've tried a few different ways, and I think my problem is that I'm not sure what assumptions to make. Can anyone help? Thanks!

Answer 1

You can prove it in classical logic.

1) $q$ --- assumed [a]

2) $p \to q$ --- $\to$-intro

3) $(p \to q) \lor (q \to r)$ --- $\lor$-intro

4) $\lnot q$ --- assumed [b]

5) $\bot$ --- from 1) and 4)

6) $r$ --- from 5)

7) $q \to r$ --- $\to$-intro

8) $(p \to q) \lor (q \to r)$ --- $\lor$-intro

9) $\vdash q \lor \lnot q$ --- LEM

10) $(p \to q) \lor (q \to r)$ --- from 1)-3) and 4)-8) with 9) by $\lor$-elimination, discharging assumptions [a] and [b].

I suppose that we cannot prove it intuitionistically ...

Answer 2

This statement cannot be shown by intuitionistically valid rules, as it is equivalent to the law of excluded middle, which does not hold intuitionistically.

To be more precise we have:

$~\vdash X \lor \neg X$ for every $X$ is equivalent to having $~\vdash (A \rightarrow B) \lor (B \rightarrow C)$ for every $A, B, C.$

Proof:

• Assume we need to show $~\vdash (A \rightarrow B) \lor (B \rightarrow C)$ then by $\mathsf{LEM}$ we know $\vdash B \lor \neg B$. In the case where $B$ holds, we can certainly show $A \rightarrow B$ and in the other case we can show $\neg B \vdash B \rightarrow C$ since $\neg B, B \vdash \bot$.
• Assume we have $~\vdash (A \rightarrow B) \lor (B \rightarrow C)$ for every $A,B,C$ and try to show $~\vdash X \lor \neg X$ for very $X$. For this we simply choose $A := (X \rightarrow X)$, $B := X$, $C := \bot$.

---

For a list of even more statements that are equivalent to $\mathsf{LEM}$ in intuitionistic logic, have a look at this paper: Classifying Material Implications over Minimal Logic.

Answer 3

@Lereau gives the technical answer why your wff is not intuitionistically provable.

But faced with a question like this, it is always worth stepping back and asking yourself whether a given wff ought to be intuitionistically provable. Does it seem the sort of thing which is constructively provable?

Well obviously not so in this case, for a disjunction is only constructively provable if one of the disjuncts is constructively provable. And evidently in this case $(p \to q)$ is not constructively provable (with no background assumptions to play with). And similarly for the other disjunct. So even in advance of the technical answer you already should know that the wff is not constructively provable. (Though it is classically provable as @Mauro notes, or as immediately follows from @Lereau's answer.)