Is negation introduction derivable in the natural deduction system of intuitionistic propositional logic?

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.

1 Answer

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.]

• 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? – j11c Feb 2 '16 at 0:56
• 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? – Rob Arthan Feb 2 '16 at 1:09
• 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. – j11c Feb 2 '16 at 1:35