可证性逻辑的一种谓词扩张的无切割证明系统
逻辑
2023-02-22 v1
摘要
本文引入证明系统NQGL,用于可证性逻辑GL(即由K与Löb公式□(□p⊃p)⊃□p定义的命题逻辑)的Kripke完全谓词扩张。NQGL是根岑相继式演算LK的模态扩张。尽管NQGL的命题片断公理化了GL,它并不以Löb公式为公理,而是含有一条非紧致规则,即具有可数多条前提的推导规则。我们证明NQGL具有切割可容许性,且相对于如下Kripke框架类完全:其中每一世界出发的路径长度的上确界有限。
引用
@article{arxiv.1802.10261,
title = {A cut-free proof system for a predicate extension of the logic of provability},
author = {Yoshihito Tanaka},
journal= {arXiv preprint arXiv:1802.10261},
year = {2023}
}