中文

关于 Afshari & Leigh 系统 Clo 不完备性的一则注记

逻辑 2023-07-14 v1

摘要

系统 Clo\mathsf{Clo} 是模态 μ\mu-演算的一个循环、无切割证明系统。它由 Afshari & Leigh 引入,作为其意图证明 Kozen 的模态 μ\mu-演算公理化之完备性的中间系统。我们给出一个不可在 Clo\mathsf{Clo} 中证明的有效相继式,从而证明 Clo\mathsf{Clo} 是不完备的。

关键词

引用

@article{arxiv.2307.06846,
  title  = {A note on the incompleteness of Afshari & Leigh's system Clo},
  author = {Johannes Kloibhofer},
  journal= {arXiv preprint arXiv:2307.06846},
  year   = {2023}
}