Proof systems for super-strict implication

This paper studies proof systems for the logics of super-strict implication ST2–ST5, which correspond to C.I. Lewis’ systems S2–S5 freed of paradoxes of strict implication. First, Hilbert-style axiomatic systems are introduced and shown to be sound and complete by simulating STn in Sn and backsimulating Sn in STn, respectively (for n = 2, ..., 5). Next, G3-style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are distinctive of G3-style calculi, that they are sound and complete, and it is shown that the proof search for G3.ST2 is terminating and therefore the logic is decidable.