On the Cut Elimination of Weak Intuitionistic Tense Logic

TL;DR

This work tackles cut-elimination for weak intuitionistic tense logic by developing a novel method that splits contraction and Cut rules in the sequent calculus $\mathsf{GwIK}_{t}$, situating the study within the IK$_t$ lineage. It introduces a sequence of refined calculi, notably $\mathsf{GwIK}_{t}^\dagger$ and $\mathsf{GwIK}_{t}^\ddagger$, and replaces the original (Con$_F$) and (Cut) with labeled contractions $\mathrm{Con_A}$, $\mathrm{Con_\sharp}$, $\mathrm{Con_\rightarrow}$ and Cut-like mixes $(Mix_A)$, $(Mix_\sharp)$, $(Mix_\rightarrow)$, $(Cut_\ast)$, proving their equivalence to the base system. The core argument proceeds by induction on cut height and formula complexity, organized into Scenario I–IV, to establish cut-elimination for $\mathsf{GwIK}_{t}$, and further yields Craig’s interpolation for the modified calculus. The approach highlights rule invertibility and mix-rule interactions as key mechanisms, and the authors claim applicability to a broader class of logics, suggesting the development of a general framework for cut-elimination in related systems.

Abstract

In this paper, we use a new method to prove cut-elimination of weak intuitionistic tense logic. This method focuses on splitting the contraction rule and cut rules. Further general theories and applications of this method shall be developed in the future.

Figures (1)

• Figure 1: The proof strategy of $\mathsf{GwIK}_{t}$'s cut-elimination

Theorems & Definitions (25)

• definition 1.1
• definition 1.2
• definition 1.3
• definition 1.4
• definition 1.5
• lemma thmcounterlemma
• proof
• lemma thmcounterlemma
• proof
• lemma thmcounterlemma