Minimal difference between classical and intuitionistic sequent calculus

Question

Consider propositional logic with primitive connectives $\{{\to},{\land},{\lor},{\bot}\}$. We view $\neg \varphi$ as an abbreviation of $\varphi\to\bot$ and $\varphi\leftrightarrow\psi$ as an abbreviation of $(\varphi\to\psi)\land(\psi\to\varphi)$, etc.

The classical sequent calculus LK has rules such as

$$\frac{\Gamma, \varphi\vdash \Pi \qquad \Sigma, \psi\vdash \Pi} {\Gamma, \Sigma, \varphi\lor\psi \vdash \Pi}{\lor}L \qquad \frac{\Gamma\vdash\varphi,\Delta}{\Gamma\vdash\varphi\lor\psi,\Delta}{\lor}R_1 \qquad \frac{\Gamma \vdash \psi, \Delta}{\Gamma\vdash\varphi\lor\psi,\Delta}{\lor}R_2 $$ $$ \frac{\Gamma\vdash\varphi,\Delta \qquad \Sigma,\psi\vdash\Pi} {\Gamma, \Sigma, \varphi\to\psi \vdash \Delta,\Pi}{\to}L \qquad \frac{\Gamma,\varphi\vdash \psi,\Delta}{\Gamma\vdash\varphi\to\psi,\Delta}{\to}R $$ and so forth, where $\Gamma$, $\Sigma$, $\Pi$, and $\Delta$ are finite multisets of formulae.

It is well known that if we restrict the shape of all sequents to have exactly one formula to the right of the $\vdash$, we get a proof system LJ for intuitionistic propositional logic. This corresponds to requiring that every $\Delta$ is empty and every $\Pi$ is a singleton in the formulations of the rules above.

Do we still get intuitionistic logic if the only rule we make this change to is ${\to}R$? In other words, we have $$\frac{\Gamma,\varphi\vdash\psi}{\Gamma\vdash\varphi\to\psi}{\to}R'$$ together with all of the other rules in their classical formulation, including structural rules with long $\Delta$s and $\Pi$s.

---

(Motivation: I'm trying, yet again, to wrap my head around what the essential difference between intuitionistic and classical logic is. It's often said that intuitionistic logic grew out of Brouwer's stricter demands on how a disjunction can be proved, but that can't be the whole story because there's a difference even for the implicational fragment (with no disjunctions). Now I'm wondering whether disjunction is actually part of the story at all. Kripke semantics treats it completely classically, and intuitionistic logic becomes fully classical if we add Peirce's law as an axiom (which again does not mention disjunction). The above conjecture is inspired by the Curry-Howard isomorphism where Peirce's law maps to call/cc, more or less. Therefore it would make sense that we can get intuitionistic logic simply by forbidding lambda abstractions from capturing continuation variables.)

Answer 1

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!).

Answer 2

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.

Answer 3

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.