Minimal difference between classical and intuitionistic sequent calculus

This rings a bell. And ah yes, on p. 48 of Sara Negri and Jan van Plato's admirable book Structural Proof Theory (CUP, 2001), they write

It is not the [general] feature of having a multiset as a succedent that leads to classical logic, but the unrestricted $R\!\supset$ rule,

where by the unrestricted $R\!\supset$ they mean your classical $\to\! R$ rule, and the restricted rule would be your $\to\! R'$ rule.

Then on p. 108, they introduce an intuitionistic multisuccedent calculus they call G3im, which is exactly like a classical multisuccedent calculus except for the $\supset$ rules (though both left and right rules get tinkered with). I guess that the ensuing discussion, and the 1988 book by Dragalin Mathematical Intuitionism to which the calculus is due, would seem to be good starting points for further investigation (and I'd be interested to hear more about how things go!).


Peter Smith found a nice reference which more or less settles the question. Here are some concluding remarks that won't fit as comments:

Knowing that it's true gave me the courage to try proving it, which turned out to be easier than expected. In fact, each of the classical rules except ${\to}R$ (but including ${\to}L$) is actually derivable in the single-succedent calculus (with Cut) if $\Gamma\vdash\varphi,\psi,\ldots,\sigma$ is taken to abbreviate $\Gamma\vdash \varphi\lor\psi\lor\cdots\lor\sigma$. This verification turns out to be completely routine.

This supports my hypothesis that the essential difference between classical and intuitionistic is that the intuitionistic $\varphi\to\psi$ is a stronger claim in the sense of being more difficult to prove (but not easier to conclude something from). Since $\neg$ abbreviates an implication, this also makes negations more difficult to prove in intuitionistic logic.

What prevents the unrestricted ${\to}R$ from being derivable is that deriving it in the same way as the others would require reasoning from $\varphi\to(\psi\lor \sigma)$ to $(\varphi\to\psi)\lor\sigma$, which is not intuitionistically possible.

In the particular case $\psi=\bot$, what this says is that we can't reason from $\varphi\to(\bot\lor\sigma)$ (which is obviously equivalent to $\varphi\to\sigma$) to $\neg\varphi\lor \sigma$. This can look like $\lor$ is harder to prove in intuitionistic logic, but it's really the $\neg$ that makes $\neg\varphi\lor\sigma$ harder to conclude.


As a small addition to the previous answers, the calculus you mention where only the implication right rule has an empty context on the right hand side seems to have been introduced in Maehara: Eine Darstellung der intuitionischen Logik in der klassischen.

Also, it might be interesting to have a look at the nested sequent calculus for intuitionistic logic given by Fitting in Nested Sequents for Intuitionistic Logics. The calculus there can be seen essentially as spelling out a backwards proof search in Maehara's calculus, where the implication right rule creates a new successor, and the so-called lift rule copies all the context on the left hand side into the successor (see, e.g., here). Since the constructed nested sequents are trees of ordinary sequents, they have a natural interpretation as Kripke-models for intuitionistic logic. In contrast, for classical logic the implication right rule would stay completely local and would not create a new successor.