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.


[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$.



      If $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.

  • $\begingroup$ Thanks, the reason why I didn't even tried to use the LEM is because we were asked to prove it later in the next excersice, so we were not allowed to assume it and because of that I thought it was not necessary for this proof: big mistake. Now I've wrote a huge tree for this proof wich includes the proof of LEM and DDR... anyway thanks! $\endgroup$ – la flaca May 29 '16 at 16:13
  • $\begingroup$ @Eliana: You're welcome! What is DDR? Do you mean $\neg B, B \lor C \vdash C$? Haha I don't remember these names... Anyway it is also possible to 'not use' LEM. Specifically, under the assumption of $\neg( (A→B) \lor (A→C) )$, you can show both $\neg( A→B )$ and $\neg(A→C)$, but then you can also show $A→C$ by using $A → B \lor C$ and the impossibility of $A→B$. This gives the desired contradiction. The reason I showed you the above proof is because it is usually a more efficient technique; whenever you don't know what to do, split cases cleverly using LEM! $\endgroup$ – user21820 May 30 '16 at 3:26
  • $\begingroup$ @Eliana: Note that this proof by contradiction finally finishes with a double negation elimination, which is somewhat equivalent to LEM. Incidentally, your question sparked of my curiosity about how to prove that LEM is required (in a certain precise sense). I therefore asked a question at math.stackexchange.com/q/1804360. It may be beyond you at the moment, but if you're interested, basically if you discard double negation elimination and add the principle of explosion, you get intuitionistic logic. Also see en.wikipedia.org/wiki/Sequent_calculus (compare LK and LJ). $\endgroup$ – user21820 May 30 '16 at 3:32
  • $\begingroup$ right now I'm working on comparing LK and LJ (it's part of our set of excecises), by DDR I ment the double negation rule but I should have written DNR, I apologize for that, my brain confuses symbols (I think one symbol and I write another one). $\endgroup$ – la flaca May 30 '16 at 23:34
  • $\begingroup$ @Eliana: Ah I see. I'm surprised that your course goes through LK and LJ. When I studied logic even at graduate level there was completely zero mention of these. $\endgroup$ – user21820 May 31 '16 at 8:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.