A sequent system for the interpretability logic with the persistence axiom
克巳 佐々木 · Institutional Repositories DataBase (IRDB) · 2002
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.