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, ...)
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.
$\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.
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.
