We study modal logics of interpretability. These logics are propositional modal logics with a binary modality \(\vartriangleright \) and a unary modality \(\square \) that model formalised versions of relativized interpretability and provability respectively. The standard relational semantics for interpretability logics goes by the name of Veltman semantics. Veltman models have a unary accessibility relation R to model the unary \(\square \) modality and a ternary accessibility relation S to model the binary modality \(\vartriangleright \) . Models can possess wild behaviour and in a sense cannot be tree-like. In this paper we study if we can tame the complexity of the needed models by resorting to a slightly tweaked notion of semantics. We prove soundness and completeness for this new semantics which follows from the right notion of bisimulation. The motivation for this study is rooted in a long-standing open question to determine \(\textbf{IL}\) (All), the interpretability logic of all reasonable arithmetical theories. In this paper we strengthen a conjecture formulated in [5] and show that the new conjecture is consistent with the literature so far.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On Tame Semantics for Interpretability Logic

  • Vicent Navarro Arroyo,
  • Joost J. Joosten

摘要

We study modal logics of interpretability. These logics are propositional modal logics with a binary modality \(\vartriangleright \) and a unary modality \(\square \) that model formalised versions of relativized interpretability and provability respectively. The standard relational semantics for interpretability logics goes by the name of Veltman semantics. Veltman models have a unary accessibility relation R to model the unary \(\square \) modality and a ternary accessibility relation S to model the binary modality \(\vartriangleright \) . Models can possess wild behaviour and in a sense cannot be tree-like. In this paper we study if we can tame the complexity of the needed models by resorting to a slightly tweaked notion of semantics. We prove soundness and completeness for this new semantics which follows from the right notion of bisimulation. The motivation for this study is rooted in a long-standing open question to determine \(\textbf{IL}\) (All), the interpretability logic of all reasonable arithmetical theories. In this paper we strengthen a conjecture formulated in [5] and show that the new conjecture is consistent with the literature so far.