Stuck at one step on the proof of distributive law of implication over disjunction

Question

I'm working with classic natural deduction system NK and the elimination rule for disjunction is stated as follows (I apologize, I don't know how to express it in tree-form):

$\Gamma \vdash \chi$ is an immediate consequence of the sequents: $\Gamma \vdash \phi \lor \psi \quad \Gamma ,\phi \vdash \chi \quad \Gamma, \psi \vdash \chi$

I'm trying to use that rule to derive $\phi \to \psi \lor \chi \vdash (\phi \to \psi) \lor (\phi \to \chi)$, so I assume I should derive it from the following sequents: $$\ \phi \to \psi \lor \chi \vdash \psi \lor \chi \\ \phi \to \psi \lor \chi,\ \psi \vdash (\phi \to \psi) \lor (\phi \to \chi) \\ \phi \to \psi \lor \chi,\ \chi \vdash (\phi \to \psi) \lor (\phi \to \chi) $$ But the problem is that I can't get to the first sequent, instead of it I get this one:$$ \phi \to \psi \lor \chi, \ \phi \vdash \psi \lor \chi $$ and I don't know how to fix it in order to apply the elimination rule for disjunction.

Any hint, advice or idea is welcome, thanks in advance.

Answer 1

[I'm going to use $A,B,C$ because I see no reason to use greek letters here.] $\def\imp{\rightarrow}$

Here is a natural deduction proof (Fitch-style). It should be easy to convert it into sequent-style.

If $A \imp B \lor C$:

  $B \lor \neg B$.   [Insert your favourite proof of LEM here.]

  If $B$:

    $A \imp B$.   [This should be easy for you to get.]

  If $\neg B$:

    If $A$:

      $B \lor C$.

      If $B$:

        $\neg B$.

        Contradiction.

        $C$.

      If $C$:

        $C$.

      $C$.

    $A \imp C$.

  $( A \imp B ) \lor ( A \imp C )$.   [This should be easy for you.]

I think the use of LEM (law of excluded middle) is necessary, and there is no proof of the theorem you want in intuitionistic logic.