Axioms (Jun 2023)
Cut-Free Gentzen Sequent Calculi for Tense Logics
Abstract
The cut-free single-succedent Gentzen sequent calculus GKt for the minimal tense logic Kt 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.
Keywords