A Gentzen-type calculus of sequents for single-operator propositional logic
John Riser · Journal of Symbolic Logic · 1967
The following describes a calculus of sequents (SLK) patterned after the calculus LK of Gentzen in [1] but restricted to the formulas of propositional logic and modified so that the only connective is the Sheffer stroke. The ‘elimination theorem’ (Hauptsatz) is proved for SLK and a decision procedure is specified for determining whether a given formula in stroke notation is tautologous. In addition, SLK is proved consistent and complete. Subsequent remarks indicate briefly how the calculus can be modified so as to employ the dagger as the only connective.