超限可证逻辑的多拓扑
The polytopologies of transfinite provability logic
摘要：
可证性逻辑是模态或多模态系统，设计用于对算术理论中哥德尔可证性谓词及其自然扩张的行为进行建模。如果Λ是任意序数，则Gödel-Löb演算GLP（Λ）对于每个λ<Λ包含一个模态[λ]，表示强度增加的可证明性谓词。GLP（Λ）没有Kripke模型，但Beklemishev和Gabelaia最近证明了GLP（ω）对于它的拓扑模型类是完备的。本文将Beklemishev和Gabelaia的结果推广到了GLP（Λ），其中对任意的Λ都是如此.我们还介绍了可证明性的环境，这是拓扑模型的公式的估值受到限制。在此基础上，我们证明了基于Icard拓扑的一类可证明性环境的GLP（Λ）的完备性。
英文摘要：
Provability logics are modal or polymodal systems designed for modeling the behavior of Gödel's provability predicate in arithmetical theories and its natural extensions. If Λis any ordinal, the Gödel-Löb calculus GLP(Λ) contains one modality [λ] for each λ<Λ, representing provability predicates of increasing strength. GLP(Λ) has no Kripke models, but Beklemishev and Gabelaia recently proved that GLP(ω) is complete for its class of topological models. In this paper we generalize Beklemishev and Gabelaia's result to GLP(Λ) for arbitrary Λ. We also introduce provability ambiances, which are topological models where valuations of formulas are restricted. With this we show completeness of GLP(Λ) for the class of provability ambiances based on Icard polytopologies.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
