直觉主义 Gödel-Löb 逻辑，Simpson 风格：标号系统与双关系语义

Anupam Das; Iris van der Giessen; Sonia Marin

直觉主义 Gödel-Löb 逻辑，Simpson 风格：标号系统与双关系语义

计算机科学中的逻辑 2023-09-04 v1 逻辑

作者: Anupam Das , Iris van der Giessen , Sonia Marin

摘要

我们通过证明论技术推导了 Simpson 风格的直觉主义 Gödel-Löb 模态逻辑（ $\sf{GL}$ ）。我们将用于 $\sf{GL}$ 的非良基标号系统限制为右侧仅有一个公式，从而得到标号系统 $\sf{\ell IGL}$ 。后者利用循环证明论的技术获得，规避了 $\sf{GL}$ 通常的框架条件（逆良基性）非一阶可定义的障碍。尽管现有的直觉主义 $\sf{GL}$ 版本通常仅定义于框（而非菱形）之上，我们的表述同时包含两种模态。我们的主要结果是 $\sf{\ell IGL}$ 与双关系语义中相应的语义条件一致：模态关系与直觉主义关系的复合是逆良基的。我们将所得逻辑称为 $\sf{IGL}$ 。可靠性方向使用标准思想证明，而完备性方向更为复杂，需要经过若干中间刻画 $\sf{IGL}$ 的迂回。

关键词

直觉主义 Gödel-Löb 逻辑标号系统双关系语义循环证明模态逻辑

引用

@article{arxiv.2309.00532,
  title  = {Intuitionistic G\"odel-L\"ob logic, \`a la Simpson: labelled systems and birelational semantics},
  author = {Anupam Das and Iris van der Giessen and Sonia Marin},
  journal= {arXiv preprint arXiv:2309.00532},
  year   = {2023}
}

备注

25 pages including 8 pages appendix, 4 figures

直觉主义 Gödel-Löb 逻辑，Simpson 风格：标号系统与双关系语义

摘要

关键词

引用

备注

相关论文