The Interpolation Theorem for IL and ILP

C. Areces, D. de Jongh, and E. Hoogland. The Interpolation Theorem for IL and ILP. In Proceedings of AiML98. Advances in Modal Logic, 1998.

Download

[pdf] 

Abstract

In this article we establish interpolation for the minimal system of interpretability logic . We prove that arrow interpolation holds for and that turnstile interpolation and interpolation for the \triangle-modality easily follow from this. Furthermore, these properties are extended to the system . The related issue of Beth De nability is also addressed. As usual, the arrow interpolation property implies the Beth property. From the latter it follows via an argumentation which is standard in provability logic, that has the xed point property. Finally we observe that a general result of Maksimova [11] for provability logics can be extended to interpretability logics, implying that all extensions of have the Beth property.

BibTeX

@InProceedings{Areces1998c,
  author =       "C. Areces and D. {de} Jongh and E. Hoogland",
  booktitle =    "Proceedings of AiML98. Advances in Modal Logic",
  title =        "The Interpolation Theorem for {IL} and {ILP}",
  year =         "1998",
  abstract =     "In this article we establish interpolation for the
                 minimal system of interpretability logic . We prove
                 that arrow interpolation holds for and that turnstile
                 interpolation and interpolation for the
                 \triangle-modality easily follow from this.
                 Furthermore, these properties are extended to the
                 system . The related issue of Beth De nability is also
                 addressed. As usual, the arrow interpolation property
                 implies the Beth property. From the latter it follows
                 via an argumentation which is standard in provability
                 logic, that has the xed point property. Finally we
                 observe that a general result of Maksimova [11] for
                 provability logics can be extended to interpretability
                 logics, implying that all extensions of have the Beth
                 property.",
  organization = "Uppsala University",
}