Analytic Proofs for Tense Logic
摘要
The first algorithm to transform a proof in Nishimura’s sequent calculus \(\textbf{GKt}\) for tense logic \(\textbf{Kt}\) into an analytic proof of the same sequent is presented. In an analytic proof, every rule instance is analytic i.e., each formula in every premise is a subformula of some formula in its conclusion. We call this algorithm analytic restriction to convey that it extends analytic cut-restriction where just the cut-rule instances are made analytic. This distinction is essential in tense logic since cut and modal rules can both cause non-analyticity. Analytic cut-restriction is itself an extension of cut-elimination so our work contributes to a broader program of transforming arbitrary sequent proofs into ones constructed from a designated set of formulas—not necessarily subformulas. As with cut-elimination, the aim is to limit the proof search space and support proof-theoretic and meta-logical investigations.