On Logic of Formal Provability and Explicit Proofs
1933年，哥德尔考虑了两种描述可证明性的模态方法。一个捕获了形式可证明性，并导致了逻辑GL和Solovay的完备性定理。另一种是以模态逻辑S4为基础，发展出阿特莫夫的证明逻辑LP。本文研究了作者提出的逻辑GLA，它是GL和LP语言的结合体。GLA具有Kripke风格的语义和相应的完备性定理。建立了GLA关于算术可证性语义的可靠性和完备性。
2014-05-11 cs.LO math.LO
Provability interpretation of non-normal modal logics having neighborhood semantics
Kobe University（神户大学）
本文提出了一种基于邻域语义的新方法，用于研究非正则模态逻辑的算术完备性定理。
2025-11-20 math.LO
Münchhausen provability
由Solovay关于形式可证明性的著名完备性结果可知，可证明性逻辑$\mathrm GL$精确地描述了任何合理且足够强的算术理论的所有可证明的结构性质，并具有可判定的公理化。Japaridze通过考虑$\mathrm GL$的多模态版本$\mathrm GLP$来推广这一结果，其中每个自然数$n$都有模态$[n]$，这是指不断增加的可证明性概念。$\mathrm GLP$的现代处理倾向于将$[n]$可证明性概念解释为“在基础理论$T$中可证明，连同所有真正的$Π^0_n$公式作为神谕”。在本文中，我们将这种解释推广到超限。为了做到这一点，要克服的主要困难是将复杂性$Π^0_n$的甲骨文公式的语法特征推广到超算术层次。本文利用的事实，证明是$Σ^0_1$完成，类似的结果举行更强的证明概念。因此，在$α$层次上定义可证明性的预言语句将被递归地视为在较低层次上的一致性陈述：通过论文名称的可证明性来证明可证明性。本文证明了合理性和完整性的广泛的理论类的建议解释，即任何理论，可以正式的递归上述，并有一些进一步的非常自然的属性。一些评论提供了如何递归可以正式成为二阶算术和降低这些系统的二阶算术的证明理论强度。
2019-08-29 math.LO
Provability Logics of Hierarchies
可证明性逻辑的分支研究数学理论的可证明性行为。更精确地说，通过将模态解释为$T$的可证明性谓词的可证明性解释，研究了数学理论$T$与模态逻辑$L$之间的关系。在本文中，我们将扩展这种关系，以调查的可证性为基础的行为的层次结构的理论。更准确地说，使用具有无限多模态的模态语言$\{\Box_n\}_{n=0}^{\infty}$，我们将定义一些经典模态理论如$\mathbf{K4}$、$\mathbf{KD4}$、$\mathbf{GL}$和$\mathbf{S4}$的层次对应物。然后我们将定义它们的规范可证明性解释和它们相应的可靠性-完备性定理。
2017-04-20 math.LO
(Non-)well-founded derivations in the provability logic $\mathsf{GLP}$
本文研究了可证性逻辑 $\mathsf{GLP}$ 中的循环、非良基和良基推导，证明其非良基与良基推导定义了相同的无穷扩张，并确立该扩张及原始系统在广义后承关系下的强代数性与邻域完备性。
2025-04-02 math.LO
A formal proof of modal completeness for provability logic
本研究在HOL Light定理证明器中实现哥德尔-勒布可证性逻辑（GL）模态完备性的形式化证明，介绍实现细节与非标准证明结构选择，并分析该形式化系统推理的优缺点。
2021-02-11 cs.LO math.LO
Completeness of the Gödel--Löb Provability Logic for Finite Derived Ordinal Topologies
School of Mathematics, Institute for Research in Fundamental Sciences (IPM)（基础科学研究院数学学院）
本文在假设 GCH 和存在带相干测度序列的可测基数下，构造保持共尾性和 GCH 的力迫扩张，证明有限导出序数拓扑的 Gödel--Löb 逻辑完备性，并扩展 Beklemishev 定理至双模态逻辑。
2026-09-25 math.LO
The omega-rule interpretation of transfinite provability logic
在本文中，我们考虑超限可证明性逻辑，其中对于某些递归良序中的每个序数，我们都有一个对应的模态可证明性算子。模态[xi]将被解释为“在ACA_0中可证明的，最多可与omega规则的xi个嵌套应用一起”。我们将展示如何在二阶数论中对此进行形式化。接下来，我们证明在这种解释下的可靠性和完备性。最后，我们展示了如何将基础理论ACA_0降低到低于RCA_0的理论。
2013-02-21 math.LO
Hard Provability Logics
令$\mathcal{PL}({\sf T},{\sf T}')$和$\mathcal{PL}_{Σ_1}({\sf T},{\sf T}')$分别表示${\sf T}'$中${\sf T}$相对的可证明性逻辑和$Σ_1$ -可证明性逻辑。在本文中，我们刻画了以下相对可证性逻辑：$\mathcal{PL}_{Σ_1}({\sf HA},\mathbb{N})$，$\mathcal{PL}_{Σ_1}({\sf HA},{\sf PA})$，$\mathcal{PL}_{Σ_1}({\sf HA}^*,\mathbb{N})$，$\mathcal{PL}_{Σ_1}({\sf HA}^*,{\sf PA})$，$\mathcal{PL}({\sf PA},{\sf HA})$，$\mathcal{PL}_{Σ_1}({\sf PA},{\sf HA})$，$\mathcal{PL}({\sf PA}^*,{\sf HA})$，$\mathcal{PL}_{Σ_1}({\sf PA}^*,{\sf HA})$，$\mathcal{PL}({\sf PA}^*,{\sf PA})$，$\mathcal{PL}_{Σ_1}({\sf PA}^*,{\sf PA})$，$\mathcal{PL}({\sf PA}^*,\mathbb{N})$，$\mathcal{PL}_{Σ_1}({\sf…
2019-11-11 math.LO
The polytopologies of transfinite provability logic
可证性逻辑是模态或多模态系统，设计用于对算术理论中哥德尔可证性谓词及其自然扩张的行为进行建模。如果Λ是任意序数，则Gödel-Löb演算GLP（Λ）对于每个λ<Λ包含一个模态[λ]，表示强度增加的可证明性谓词。GLP（Λ）没有Kripke模型，但Beklemishev和Gabelaia最近证明了GLP（ω）对于它的拓扑模型类是完备的。本文将Beklemishev和Gabelaia的结果推广到了GLP（Λ），其中对任意的Λ都是如此.我们还介绍了可证明性的环境，这是拓扑模型的公式的估值受到限制。在此基础上，我们证明了基于Icard拓扑的一类可证明性环境的GLP（Λ）的完备性。
2013-07-04 math.LO
Strong Completeness of Provability Logic for Ordinal Spaces
Abashidze和Blass分别证明了模态逻辑$\sf{GL}$在任何大于或等于$ω^ω$的序数上的拓扑解释是完备的。Icard后来为$λ< ω$引入了一系列拓扑$\mathcal I_λ$，目的是为Japaridze的多模态逻辑$\sf{GLP}$ $_ω$提供语义。Icard的结构后来被Joosten和第二作者扩展为任意序数$λ\geq ω$。在本文中，我们进一步推广了Icard拓扑。给定一个离散空间$\mathfrak X = (X, τ)$和一个序数$λ$，我们定义一个拓扑$τ_{+λ}$，使得$τ_{+0}$是原拓扑$τ$，当$\mathfrak X$是赋予左拓扑的序数时，$τ_{+λ}$与$\mathcal I_λ$重合.然后证明了，给定任意分散空间$\mathfrak X$和任意序数$λ>0$，使得$(X, τ)$的秩足够大，$\sf{GL}$对于$τ_{+λ}$是强完备的.人们得到原来的Abashidze-Blass定理作为特殊情况的后果，其中$\mathfrak X=ω^ω$和$λ=1$。
2015-11-18 math.LO
Modal logical aspects of provability predicates and consistency statements
Kobe University（神户大学）
本文通过扩展Solovay方法和改进Arai的Rosser可证性谓词构造，建立了逻辑NP、ND、NP4和ND4的算术完全性。
2026-06-12 math.LO
Modal logics of conjunctively closed provability predicates
Graduate School of System Informatics, Kobe University（神户大学系统信息研究生院）
研究与满足特定可推导性条件的可证性谓词对应的非正规模态逻辑，引入基于闭包算子的新语义，证明了多个非正规模态逻辑的模态完全性及一些逻辑的算术完全性定理。
2026-07-10 math.LO
Finite Kripke models and provability interpretations in quantified modal logic
Kobe University（神户大学）
本文研究了有限克里普克模型在量化模态逻辑中的算术完备性，通过Artemov和Japaridze的有限模型嵌入技术，构建了两种不同场景下的可证明性谓词和算术解释。
2026-04-28 math.LO
The Modal Logic of Provability and Forcing
本文研究可证性与力迫在模态逻辑中的交互，提出双模态逻辑 PF 及 PF^ω，并分别刻画一般情形与集合论 ω-模型中的对应逻辑。
2023-11-01 math.LO
Solovay's completeness without fixed points
本文给出了Solovay关于Gödel-Löb可证逻辑GL的算术完备性定理的一个新证明。最初，GL关于$\Box$作为PA中可证明性的解释的完备性由R. 1976年的Solovay。Solovay证明的关键部分是他对给定的模态公式构造了一个算术求值，如果在GL中不可证明，则该公式不可证明PA。使用某些算术不动点构造用于评估的算术语句。Solovay开发的方法已被用于为许多其他逻辑建立类似的语义。在我们的证明中，我们开发了新的更明确的所需评估的结构，在它们的定义中不使用任何不动点。据我们所知，这是第一个替代证明的定理，本质上不同于索洛维的证明在这一关键部分。
2017-05-22 math.LO
Arithmetical completeness for some extensions of the pure logic of necessitation
Graduate School of System Informatics, Kobe University（神户大学系统信息学研究科）
本文研究了某些纯必然逻辑扩展的算术完备性，证明了这些扩展作为可证明性逻辑的性质。
2025-11-20 math.LO
Arithmetical completeness theorems for monotonic modal logics
本文研究了满足条件M的可证性谓词的模态逻辑性质，证明了五种单调模态逻辑的算术完全性定理，并从模态逻辑角度区分了一致性陈述的两种不同形式化。
2023-04-01 math.LO
Provability Logic: models within models in Peano Arithmetic
在1994年杰希给出了模型理论证明哥德尔的第二不完备定理Zermelo-Fraenkel集合论在以下形式：ZF不证明ZF有一个模型。Kotlarski表明，Jech的证明可以适应皮亚诺算术的作用，模型正在采取的完整一致的扩展。在本说明中，我们采取另一个步骤的方向，取代证明理论的模型理论的论点。我们表明，没有通过算术完备性定理，存在的PA的复杂性模型$Σ^0_2$是独立的PA，其中一个模型是确定的一组公式与参数，在模型中。我们的方法是基于一个新的解释证明逻辑的皮亚诺算术与模态算子解释为真理，在每一个$Σ^0_2$模型。
2022-04-16 math.LO
Mechanizing Gödel's Incompleteness Theorems and Provability Logic
Tohoku University（东北大学）；Kobe University（神户大学）
该研究在Lean 4中形式化验证了哥德尔不完备定理及可证性逻辑GL的Solovay完备性，为数学基础提供机器证明。
2026-09-16 cs.LO math.LO
A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。
2025-06-17 cs.LO math.LO
Infinitary provability logic
Ghent University（根特大学）；Steklov Mathematical Institute of the Russian Academy of Sciences（俄罗斯科学院列别捷夫数学研究所）
本文研究Gödel-Löb可证性逻辑的无穷性对应物，提出非良基深层推理系统$\dgla$，证明其相对于良基传递Kripke框架的可靠性与完备性，并借助Kripke-Platek集合论建立无穷可证性解释，表明Hilbert式变体可靠，且在某些条件下无穷可证性逻辑介于两者之间。
2026-09-22 math.LO
Mechanising Gödel-Löb provability logic in HOL Light
该论文在HOL Light中形式化了Gödel-Löb可证性逻辑的元理论，证明可靠性与完备性，并实现了一个基于G3KGL演算的判定算法作为定理证明器策略。
2023-10-12 cs.LO math.LO
An Escape from Vardanyan's Theorem
针对Vardanyan定理关于皮亚诺算术量化可证性逻辑不可计算公理化的结论在严格正签名下无法证明的问题，研究推广Kripke可靠性与完全性证明得常域完全性，通过Solovay型构造证明QRC₁系统的算术语义完全性，明确其为QGL严格正片段及QPL(PA)的片段。
2021-08-31 math.LO
Strong completeness of the logic J
Institute of Discrete Mathematics and Geometry, Vienna University of Technology（维也纳工业大学离散数学与几何研究所）
该研究证明多模态逻辑J相对于J-花束是强完备的，进而得到可证性逻辑GLP的完备性结果，同时通过反例说明GLP相对于Beklemishev-Gabelaia空间不具备强完备性。
2026-08-10 math.LO
An $ω$-rule for the logic of provability and its models
研究配备 $ω$-规则的可证性逻辑证明系统 $\mathsf{NGL}$，区分三类均刻画 GL 的传递 Kripke 框架，并代数证明其完全性及相关模态代数类非簇。
2023-11-02 math.LO
Completeness proof of functional logic, a formalism with variable-binding nonlogical symbols
我们知道一阶逻辑的量词的扩展“有不可数的许多.“，“大多数...新的公理和适当的语义相关的是操作，如“x的集合，这样......“，希尔伯特的$ε$ -算子，丘奇的$λ$ -符号，最小化和类似的，它们也将变量绑定在某个表达式中，然而其含义部分地通过翻译成一阶逻辑的语言来定义。本文提出了一个推广，包括任意变量绑定符号作为非逻辑运算。公理扩展由新的等式公理确定;模型将泛函分配给变量绑定符号。证明了这个所谓的“一阶函数逻辑”系统的完备性。
1995-03-13 math.LO
Quantified Reflection Calculus with one modality
本文提出了QRC逻辑$_1$，它是量化模态逻辑的严格正片段.对菱形模态的预期解读是形式理论的一致性。谓词符号被解释为参数化公理化。我们证明了算术可靠的逻辑QRC $_1$关于这个算术解释。量化的可证明性逻辑是不可判定的。然而，不可判定性证明不能在我们的签名和算术阅读中进行。我们猜想逻辑QRC $_1$是算术完备的.本文采取的第一步，通过提供关系语义QRC $_1$与相应的完整性证明算术的完整性。我们还展示了有限模型的属性，这意味着可判定性。
2020-03-30 math.LO
Dependence Logic with Generalized Quantifiers: Axiomatizations
我们证明了两个完备性结果，一个是关于依赖逻辑由具有弱解释的单调广义量词Q扩展的结果，弱的意思是Q的解释随结构而变化。第二个结果考虑了依赖逻辑的扩展，其中Q被解释为“存在不可数的许多”。“这两个公理化都被证明是健全的，完整的FO（Q）的后果。
2013-04-02 cs.LO math.LO
Lewis and Brouwer meet Strong Löb
本研究在构造性Löb逻辑中考察“强度”原理，给出可证性逻辑核心定理的简化形式，证明两个系统的一致插值性，概述其算术解释并梳理与计算机科学的关联。
2024-04-18 cs.LO math.LO
Independent families in Boolean algebras with some separation properties
证明了任何具有基本完备性的布尔代数都包含一个独立的大小连续族。这改进了80年代Argyros的一个结果，该结果断言存在一个不可数的独立家庭。事实上，我们证明它的一个更大的类布尔代数满足弱得多的性质。因此，所有这样的布尔代数的Stone空间都包含整数的Cech-Stone紧化的一个拷贝，并且它们上的连续函数的巴拿赫空间有$l_\infty$作为商。讨论了巴拿赫空间中的Grothendieck性质。
2012-09-02 math.FA math.GN math.LO
