On the Cut Elimination of Weak Intuitionistic Tense Logic

2024/05/16 by Yiheng Wang, Yu Peng, Wang, Yiheng +3
Biochemistry, Genetics and Molecular Biology · #DNA and Biological Computing

paper · pdf · doi:10.48550/arxiv.2405.09970

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.

Related

• On Permuting Cut with Contraction
• Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic
• Syntactic cut-elimination and backward proof-search for tense logic via\n linear nested sequents (Extended version)
• A theory of cut-restriction: first steps
• A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised