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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Analytic Proofs for Tense Logic

  • Agata Ciabattoni,
  • Timo Lang,
  • Revantha Ramanayake

摘要

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.