Scholarlink

We provide a simple cut elimination proof for the interpretability logic of \(\textsf{IL}\) . To achieve this, we introduce a traditional Gentzen-style sequent calculus for \(\textsf{IL}\) and a non-wellfounded version of it. The non-wellfounded calculus makes it possible to avoid diagonal formulas. Hence, we can give a simple argument based on a general proof-theoretic method for calculi of this kind. Our results provide a useful basis for further research; in particular, they will allow us to establish uniform interpolation for \(\textsf{IL}\) .

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

Non-wellfounded Proof Theory for Interpretability Logic

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年

查看全文
  • Sebastijan Horvat,
  • Borja Sierra Miranda,
  • Thomas Studer

摘要

We provide a simple cut elimination proof for the interpretability logic of \(\textsf{IL}\) . To achieve this, we introduce a traditional Gentzen-style sequent calculus for \(\textsf{IL}\) and a non-wellfounded version of it. The non-wellfounded calculus makes it possible to avoid diagonal formulas. Hence, we can give a simple argument based on a general proof-theoretic method for calculi of this kind. Our results provide a useful basis for further research; in particular, they will allow us to establish uniform interpolation for \(\textsf{IL}\) .