\input zb-basic
\input zb-ioport
\iteman{io-port 05852854}
\itemau{Schroeder-Heister, Peter}
\itemti{Implications-as-rules vs. implications-as-links: an alternative implication-left schema for the sequent calculus.}
\itemso{J. Philos. Log. 40, No. 1, 95-101 (2011).}
\itemab
The author proposes an alternative left-introduction schema for implication in Gentzen's sequent calculus for propositional intuitionistic logic which he considers ``conceptually more basic''. The original implication rule $(\to L)$ $$\frac{\Gamma\vdash A\quad\Delta,B\vdash C}{\Gamma,\Delta,A\to B\vdash C}$$ is replaced by the rule $(\to L)^\circ$ $$\frac {\Gamma\vdash A}{\Gamma,A\to B\vdash B}$$ postponing the cut with $\Delta,B\vdash C$. The resulting system no longer enjoys cut elimination, but only what the author calls ``cut elimination in a weak form'': the cuts that one cannot eliminate are those introduced when translating a cut-free derivation of the original system in the obvious way.  It is argued that the $(\to L)^\circ$-rule captures precisely the essence of implication in that $A\to B$ allows to transform a proof of $A$ into a proof of $B$, while the $(\to L)$-rule additionally contains some sort of cut which is revealed when considering the following instance $$\frac {\Gamma\vdash A\quad\Delta,A\vdash C}{\Gamma,\Delta,A\to A\vdash C}: $$ the power of cut in the system with the $(\to L)$-rule reduces to the elimination of trivial assumptions $A\to A$.
\itemrv{Dieter Probst (Bern)}
\itemcc{}
\itemut{implication; sequent calculus; cut elimination}
\itemli{doi:10.1007/s10992-010-9149-z}
\end