Implications-as-rules vs. implications-as-links: an alternative implication-left schema for the sequent calculus (Q626494)

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