无穷性可证性逻辑

中文摘要 AI 辅助

Gödel-Löb可证性逻辑$\GL$是一个命题模态系统，一方面它相对于逆良基Kripke框架具有完备性，另一方面它刻画了所有在$\PA$自身中可证明的关于$\PA$-可证性的模态原则。在本文中，我们对$\GL$的无穷性对应物是什么这一问题进行了初步研究。我们为具有至多可数无穷合取和析取的模态语言发展了一个非良基深层推理证明系统$\dgla$。我们证明了该演算对于良基传递Kripke框架是可靠且完备的。利用Kripke-Platek集合论，我们以可容许集上的无穷可证性来发展无穷模态语言的解释。然后我们证明了无穷性$\GL$的一个自然Hilbert式变体对于该解释是可靠的。然而，我们留下了一个开放问题：$\dgla$是否比Hilbert式演算证明了任何额外的定理。尽管如此，在某些条件下，我们确实证明了由某些可容许集产生的无穷可证性逻辑介于Hilbert式演算的定理集与非良基深层推理系统之间。

英文摘要

Gödel-Löb provability logic $\GL$ is a propositional modal system that on one hand enjoys completeness with respect to conversely well-founded Kripke frames and on the other hand captures all modal principles about $\PA$-provability that are provable in $\PA$ itself. In the present paper we carry out an initial investigation into the question of what the infinitary counterpart of $\GL$ is. We develop a non-well-founded deep inference proof system $\dgla$ for the modal language with at most countably infinite conjunctions and disjunctions. We show that the calculus is sound and complete for well-founded transitive Kripke frames. Using Kripke-Platek set theory we develop an interpretation of the infinitary modal language in terms of infinitary provability over admissible sets. Then we show that a natural Hilber-style variant of infinitary $\GL$ is sound for this interpretation. We leave open, however, the question if $\dgla$ proves any additional theorems in comparison with the Hilbert-style calculus. Nevertheless, under certain conditions we do show that the infinitary provability logic arising from certain admissible sets lies between the set of theorems of the Hilbert-style calculus and the non-well-founded deep inference system.

发表机构

• Ghent University（根特大学）
• Steklov Mathematical Institute of the Russian Academy of Sciences（俄罗斯科学院列别捷夫数学研究所）

机构由 AI 辅助整理，请以论文原文为准。