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

Question

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.

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