\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