Restricting left side formulas in sequents

Question

It is well known that if we restrict the right side part of sequents to be single formulas, we obtain intuitionist logic. What happens if we restrict left side part in sequents to have only one formula? Which logic one obtains? Where can I read more about this?

Answer 1

Most of the rules of the classical sequent calculus have exact duals, so it doesn't really matter for them whether it's the left-hand side or the right-hand side of the sequents we restrict.

The exception to this is implication.

In a classical sequent calculus where $\neg$ is a primitive, $A\to B$ behaves exactly like $\neg A \lor B$; the left and right rules for $\to$ both become derived rules if we view $\to$ as an abbreviation.

The reason why intuitionistic logic, where we restrict the right-hand side of the sequent, is interesting is that the restricted $\to$R rule allows us to do something that the restricted $\neg$R and $\lor$R rules cannot be combined to produce. So now $\to$ is actually an interesting connective in its own right.

On the other hand, if we restrict to the left, the problem is to do what to do with the classical $\to$L rule $$ \frac{\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A\rightarrow B \vdash \Delta, \Pi} $$ The only thing that seems to make sense is to replace $\Gamma$ on the upper left with $A\to B$ itself, giving $$ \frac{A\to B \vdash A, \Delta \qquad B \vdash \Pi}{A\rightarrow B \vdash \Delta, \Pi} \qquad\qquad \frac{A \vdash B, \Delta}{C \vdash A \rightarrow B, \Delta} $$ but now both these rules are admissible rules in the left-restricted system if we view $A\to B$ as an abbreviation for $\neg A \lor B$.

So actually what we get is exactly equivalent to the $\to$-less fragment of intuitionistic logic, only with everything replaced by its dual and the sequents written backwards!

And intuitionistic logic without implication is not very interesting at all.