A sequent system for a sublogic of the smallest interpretability logic
克己 佐々木 · Institutional Repositories DataBase (IRDB) · 2003
An interpretability logic is an extension of provability logic GL with a binary modal operator £.The smallest interpretability logic IL is obtained by adding axioms concerning £ to GL (cf.Visser [Vis97] and Japaridze and de Jongh [JJ98]).The logic IK4 is a sublogic of IL and is obtained by adding the same axioms to normal modal logic K4 as the addtional axioms of IL.[Sas02] gave a cut-free sequent system for IK4 (see also [Sas01]).Here we give another cut-free sequent system for IK4.Both of the system in [Sas02] and the system here satisfy kinds of subformula property, however, our new system has nicer one.In the system in [Sas02], a formula B £ D possibly occurs in a cut-free proof figure for A £ B → C £ D, while in the new system doesn't.南山大学紀要『アカデミア』数理情報編 第3巻，1-17，2003年3月