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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .