If I have a natural deduction system for intuitionistic propositional logic, is it possible to derive the following rule?

$$\frac{\Gamma \vdash \phi \Rightarrow \psi \quad \Gamma \vdash \phi \Rightarrow \neg \psi}{\Gamma \vdash \neg \phi}$$

($\neg \phi$ is shorthand for $\phi \Rightarrow \bot$)

My suspicion is that it isn't possible, because deriving the implication in the conclusion would require a use of the implication introduction rule, whose premise would have an expanded context $\Gamma, \phi$:

$$\frac{\Gamma, \phi \vdash \bot}{\Gamma \vdash \phi \Rightarrow \bot}$$

Since there are no rules whose premises have smaller contexts than their conclusion, there doesn't seem to be any way to derive $\Gamma, \phi \vdash \bot$ from the hypotheses. Of course, you could do it with a weakening rule, but that would only be admissible, not derivable.

Is the above reasoning correct? Or is there another approach that allows you to derive the rule?

EDIT: The rules of the natural deduction system I'm using are given below.

The natural deduction rules


1 Answer 1


Your system of natural deduction expressed as a sequent calculus is much less liberal than the usual presentation of natural deduction using proof trees. However, your rule is still derivable, in the sense that there is a fixed proof schema that can be instantiated to give your rule. Given $\Gamma$, $\phi$ and $\psi$ as in the antecedents of your rule, then with four $\mathbf{start}$s and three ${\Rightarrow}\mathbf{E}$s, you get: $$ \Gamma, \phi \Rightarrow \psi \Rightarrow \bot, \phi \Rightarrow \psi, \phi \vdash \bot $$ (with the same context in all the sequents involved). Then with three ${\Rightarrow}\mathbf{I}$s, you get: $$ \Gamma \vdash (\phi \Rightarrow \psi \Rightarrow \bot) \Rightarrow (\phi \Rightarrow \psi) \Rightarrow \phi \Rightarrow \bot $$ Given that $\lnot\phi$ is just an abbreviation for $\phi \Rightarrow \bot$, an ${\Rightarrow}\mathbf{E}$ with each of your premisses completes the derivation. Note this makes no use of $\bot\mathbf{E}$: the same schema will derive $\phi \Rightarrow \chi$ from $\phi \Rightarrow \psi$ and $\phi \Rightarrow \psi \Rightarrow \chi$.

[Aside: your system is the same as the system NJ in Sorensen and Urzyczyn's Lectures on the Curry-Howard Isomorphism. The above proof schema corresponds to an application of the $S$-combinator $\lambda f\lambda g\lambda x(f x)(g x)$ to the proofs of the premisses of the rule.]

  • $\begingroup$ Are you suggesting that I use implication-elimination on $\Gamma \vdash \phi \Rightarrow \psi$ and $\phi \vdash \phi$ (and similarly with $\Gamma \vdash \phi \Rightarrow \neg \psi$)? How can I do that when the contexts don't match? $\endgroup$
    – j11c
    Feb 2, 2016 at 0:56
  • $\begingroup$ You need to tell us exactly what rules you are using (as I suspected you would when I read your comment about admissibility v. weakening). There are several ways of setting up the details of natural deduction in a sequent style. In the one I have in mind, there is no requirement for contexts in the premisses to match and contexts are combined by union in the conclusion of a rule. This approach corresponds best to the proof tree formulation of natural deduction. If you aren't using this approach, then what are your rules? $\endgroup$
    – Rob Arthan
    Feb 2, 2016 at 1:09
  • 1
    $\begingroup$ It did occur to me that I ought to mention the precise rules - I don't know why I didn't do that, sorry. I've updated the question to include the rules in full. $\endgroup$
    – j11c
    Feb 2, 2016 at 1:35

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.