A Cut-Free Sequent System for the Smallest Interpretability Logic

In [Sas01], it was given a cut-free sequent system for the smallest interpretability logic IL. He first gave a cut-free system for IK4, a sublogic of IL, whose -free fragment is the modal logic K4. Here, using the method in [Sas01], we give sequent systems for the interpretability logic ILP obtained by adding the persistence axiom P : (p q) (p q) to IL and for the logic IK4+P obtained by adding P to IK4. We also prove a cut-elimination theorem for the system for IK4P.

• Type: Journal
• Year: 2002
• Where: SLOGICA
• Authors: Katsumi Sasaki
• Keywords: Interpretability Logic, Interpretability Logic Ilp, SLOGICA 2002, Smallest Interpretability Logic