Natural Deduction: Prove $⊢ (A → B) ∨ (B → C)$

Question

Target: Prove $⊢ (A → B) ∨ (B → C)$ without using LEM.

I may be way off here, but is it valid to solve the above with the following or-elimination pattern:
Answer: No, it is not possible to prove without LEM.

1   A → B             (assumption)
2     A                 (assumption)
3     B                 (implication elimination 1,2)
4  (A → B) ∨ (B → C)  (or-introduction 1 1)

...

9 (A → B) ∨ (B → C) (or-elimination 1-4, ...)

Answer 1

You cannot prove this without the law of the excluded middle, since the law of the excluded middle follows from this statement. Just instantiate $A$ with True and $C$ with False and you get $B \lor \lnot B$.

With the law of the excluded middle, you can prove it by case distinction on $B \lor \lnot B$. From $B$ you derive $A \to B$ and from $\lnot B$ you derive $B \to C$, so in both cases you have $(A \to B) \lor (B \to C)$.

In your reasoning, you're never discharging assumptions 1 and 5, so you're effectively proving $A \to B \vdash (A \to B) \lor (B \to C)$ and $B \to C \vdash (A \to B) \lor (B \to C)$.

After the edit, which added line 9, the question looks more like a complex and incomplete way of deriving $(A \to B) \lor (B \to C) \vdash (A \to B) \lor (B \to C)$; that also doesn't get you anywhere.

Answer 2

It is not valid to solve $⊢ (A ⇒ B) ∨ (B ⇒ C)$ with or-elimination (which I assume it's the rule of elimination of disjunction), simply because there is no disjunction to eliminate. Your step 4 only works under the assumption of step 1 and 2, and your step 9 is redundant because you already have $(A ⇒ B) ∨ (B ⇒ C)$ in step 4, so you basically proved identity (you derived $(A ⇒ B) ∨ (B ⇒ C)$ from $(A ⇒ B) ∨ (B ⇒ C)$).

When you make an assumption you must discharge it, and after your step 9 you still have two assumptions to discharge. Note that if you first assumption is $(A ⇒ B)$ you can only conlude $1): ¬(A ⇒ B)$ by $I¬$ after you derivate a contradiction, or $2): ((A ⇒ B) ⇒ X)$ by $I⇒$ or $EFSQ$. So your first assumption will not lead to your goal.

The only way I see that a non-classic derivation can work is like this:

$1). A - assumption$

$2-?). ⊥$

$?). B - EFSQ - Close-assumption -1$

$?). (A ⇒ B) - I⇒ $

$?). ((A ⇒ B) ∨ (B ⇒ C)) - I∨ $

But this looks impossible (this literaly means that a contradiction folows from any formula)

The only way it seems this formula can be derived is by assuming $¬((A ⇒ B) ∨ (B ⇒ C))$ as your first step and then derivate a contradiction so that way you conclude $¬¬((A ⇒ B) ∨ (B ⇒ C))$ and then you can use $E¬¬$. But this is a classic derivation.

Answer 3

$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}$Of course, any LEM-disjunction elimination proof can be rewritten as a RAA proof.

When $P$ may be derived under an assumption of either $Q$ or $\neg Q$, then a contradiction may be derived under an assumption of $\neg P$, so therefore $\neg\neg P$ may be derived under no assumptions at all.

$$\fitch{}{Q\vee\neg Q\\\fitch{Q}{~\vdots\\ P}\\\fitch{\neg Q}{\vdots\\P}\\P}\qquad\lower{1.5ex}{\fitch{}{\fitch{\neg P}{\fitch{Q}{~\vdots\\ \bot}\\\neg Q\\~\vdots\\\bot}\\\neg\neg P\\P}}$$

Thus we have:...

$$\fitch{}{\fitch{\neg((a\to b)\vee(b\to c))\hspace{10ex}\textsf{Assume}}{\fitch{b\hspace{28ex}\textsf{Assume}}{\fitch{a\hspace{25.5ex}\textsf{Assume}}{b\hspace{26ex}\textsf{Reiterate}}\\a\to b\hspace{23.5ex}\textsf{Conditional Introduction}\\(a\to b)\vee (b\to c)\hspace{11.5ex}\textsf{Disjunction Introduction}\\\bot\hspace{27.5ex}\textsf{Negation Elimination}\\c\hspace{28.5ex}\textsf{Explosion}}\\ b\to c\hspace{26ex}\textsf{Conditional Introduction}\\(a\to b)\vee(b\to c)\hspace{14ex}\textsf{Disjunction Introduction}\\\bot\hspace{30ex}\textsf{Negation Elimination}}\\\neg\neg((a\to b)\vee(b\to c))\hspace{11ex}\textsf{Negation Introduction}\\(a\to b)\vee(b\to c)\hspace{16ex}\textsf{Double Negation Elimination}}$$

---

Remark: However, the rule of Double Negation Elimination is exactly as non-constructive as the Law of Excluded Middle.   So although this avoids explicitly invoking LEM it is still not Intuitionistic.