Find in Library

The cut-free single-succedent Gentzen sequent calculus <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><msub><mi mathvariant="sans-serif">GK</mi><mi>t</mi></msub></semantics></math></inline-formula> for the minimal tense logic <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><msub><mi mathvariant="sans-serif">K</mi><mi>t</mi></msub></semantics></math></inline-formula> is introduced. This sequent calculus satisfies the displaying property. The proof proceeds in terms of a Kolmogorov translation and three intermediate sequent systems. Finally, we show that tense logics axiomatized by strictly positive implication have cut-free Gentzen sequent calculi uniformly.