Completeness and Well-Definability of a Provability Degree Measure in Sufficiently Powerful Formal Systems, and Finite-Time Effective Knowers
该研究证明足够强大形式系统中特定可证性程度测度的完备性与良定性，构造出最优有限时间定理认知者φ'，并揭示其与无界归纳计算的关联及对计算过程最终行为的意义。
2024-11-27 math.LO
Provability Models
本文提出名为可证性模型的经典模态逻辑新型克里普克式语义，证明了多类模态逻辑、解释性逻辑ILM对该类模型的可靠性与完全性，并将其改进为谓词可判定版本。
2025-11-19 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
Proof Theory for Bimodal Provability Logics
University of Bern（伯尔尼大学）
本文首次为双模可证逻辑设计非标记的序列表演算，涵盖CS、CSM和ER逻辑，并通过非非Wellfounded版本建立切消过程，证明了这些逻辑具有统一的Lyndon插值性质。
2026-05-14 math.LO
The Modal Logic of Provability and Forcing
本文研究可证性与力迫在模态逻辑中的交互，提出双模态逻辑 PF 及 PF^ω，并分别刻画一般情形与集合论 ω-模型中的对应逻辑。
2023-11-01 math.LO
Provability Interpretation of Propositional and Modal Logics
1933年，哥德尔引入了命题直觉主义逻辑的可证明性解释，为BHK解释建立了形式化。他使用模态系统$\mathbf{S4}$作为可证明性的直观概念的形式化，然后将$\mathbf{IPC}$翻译为$\mathbf{S4}$。他的工作建议的问题，找到一个具体的可证明性解释的模态逻辑$\mathbf{S4}$。在本文中，我们将试图回答这个问题。事实上，我们将推广Solovay对模态逻辑$\mathbf{GL}$的可证明性解释，以捕获其他模态逻辑，如$\mathbf{K4}$，$\mathbf{KD4}$和$\mathbf{S4}$。然后，我们将使用这些结果来找到一个形式化的BHK解释，我们将表明，与不同的解释的BHK解释，我们可以捕获一些命题逻辑，如直觉主义逻辑，最小逻辑和Visser-Ruitenburg的基本逻辑。此外，我们将表明，没有证明性解释的任何扩展$\mathbf{KD45}$，也没有BHK解释的经典命题逻辑。
2017-08-31 math.LO
Embeddings of Propositional Logics into the Provability Logics $\mathbf{S}$ and $\mathbf{D}$
Graduate School of System Informatics, Kobe University（神户大学系统信息研究生院）
本文修正彼得鲁欣的证明，将命题逻辑嵌入可证性逻辑的结果扩展至$\boldsymbol{D}$，提出可嵌入$\boldsymbol{D}$的命题逻辑$\boldsymbol{DPL}$。
2026-08-07 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
The $Σ_1$-Provability Logic of HA*
对于Heyting算术HA，HA* 被定义为理论$\{A\mid {\sf HA}\vdash A^{\Box}\}$，其中$A^{\Box}$被称为$A$的盒翻译。我们将HA* 的$Σ_1$可证明性逻辑刻画为一个模态理论${\sf iH}_σ^*$ .
2018-08-27 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
Semantical cut-elimination for the provability logic of true arithmetic
本文针对形式化算术真理的可证性逻辑GLS，引入其语义刻画并给出了切消定理的语义证明，该刻画可推广至其他拟正规模态逻辑。
2023-09-12 math.LO
On provability logics with linearly ordered modalities
我们引入了逻辑GLP（Λ），它是贾帕里泽的多模态可证明性逻辑GLP（ω）的推广，其中Λ是表示强度递增的可证明性算子层次的任何线性有序集。我们将提供这些逻辑到GLP（ω）的一个约化，除其他外，给出GLP（Λ）的无变量片段的规范形定理的有限性证明和GLP（Λ）对于递归序Λ的可判定性。进一步，我们给出了GLP（Λ）的无变量片段的限制公理化.
2012-10-17 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
On the complexity of the closed fragment of Japaridze's provability logic
我们考虑著名的可证明性逻辑GLP。我们证明了无变量多峰公式的GLP-可证性问题是PSPACE-完全的。对于一个数n，设L^n_0表示所有无模态的多模态无变量公式的类<n>，<n+1>，. .我们证明了，对于任何数n，来自L^n_0的公式的GLP-可证明性问题在PTIME中。
2013-05-26 math.LO
Effectively constructible fixed points in Sacchetti's modal logics of provability
本文给出了Sacchetti的模态逻辑${\bf K} + \Box(\Box^n p \to p) \to \Box p$（$n \geq 2$）可证性不动点定理的一个纯语法证明.从我们的证明中，得到了构造这些逻辑中不动点的有效方法。我们还证明了特定模态公式的简单不动点的存在性。
2021-09-13 math.LO
Uniform Interpolation in provability logics
本文利用模态可证逻辑GL和Grz的解析演算和终止演算，用证明理论的方法证明了这两类逻辑的一致内插定理. Gödel-Löb的逻辑GL的演算是标准循环演算的一个变体，在Grzegorczyk的逻辑Grz的情况下，演算实现了一个显式的循环防止机制，灵感来自Heuerding的工作。
2022-11-04 math.LO
Relative Unification in Intuitionistic Logic: Towards provability logic of HA
该研究将直觉主义逻辑的统一性与可容许性结果推广到 NNIL(par) 命题，用以刻画 HA 的可证性逻辑并证明其可判定性。
2025-10-06 math.LO
The $Σ$_1 Provability Logic of HA
本文介绍了一种模态理论$H_σ$，它对于${\bf HA}$中的算术$Σ$ _1置换是可靠的和完备的，即证明了$H_σ$是${\bf HA}$的$Σ$ _1-可证逻辑.此外，我们将证明$H_σ$是可判定的。作为这些结果的副产品，我们证明了${\bf HA} + \Box\bot$具有de Jongh性质。
2017-11-02 math.LO
The omega-rule interpretation of transfinite provability logic
在本文中，我们考虑超限可证明性逻辑，其中对于某些递归良序中的每个序数，我们都有一个对应的模态可证明性算子。模态[xi]将被解释为“在ACA_0中可证明的，最多可与omega规则的xi个嵌套应用一起”。我们将展示如何在二阶数论中对此进行形式化。接下来，我们证明在这种解释下的可靠性和完备性。最后，我们展示了如何将基础理论ACA_0降低到低于RCA_0的理论。
2013-02-21 math.LO
Strong Completeness of Provability Logic for Uncountable Languages
School of Mathematics, Institute for Research in Fundamental Sciences (IPM)（基础科学研究所数学学院）；Institut für diskrete Mathematik und Geometrie, TU Wien（维也纳工业大学离散数学与几何研究所）
本文利用Erdős-Rado定理证明了对于特定基数的模态语言，GL逻辑在广义Icard拓扑下不满足强完备性，并引入了两种拓扑空间类以证明GL和GL.3在特定语言下满足强完备性。
2026-05-13 math.LO
Topological completeness of the provability logic GLP
众所周知，GLP的可证明性逻辑是不完整的。Kripke语义学GLP的自然拓扑语义将模态解释为多拓扑空间的导算子。满足GLP所有公理的空间称为GLP-空间。我们开发了一些建设，以建立非平凡GLP-空间，并表明GLP是完全的w.r.t.所有GLP-空间的类。
2011-06-28 math.GN math.LO
Finite Kripke models and provability interpretations in quantified modal logic
Kobe University（神户大学）
本文研究了有限克里普克模型在量化模态逻辑中的算术完备性，通过Artemov和Japaridze的有限模型嵌入技术，构建了两种不同场景下的可证明性谓词和算术解释。
2026-04-28 math.LO
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
Interpolation properties for the bimodal provability logic $\mathbf{GR}$
本文研究双模态可证性逻辑GR的内插性质，通过引入新子逻辑GR°及其关系语义，证明了二者满足Lyndon与一致内插性质。
2023-11-17 math.LO
Provability and interpretability logics with restricted realizations
理论T的可证明性逻辑是在任何算术实现下都可在T中证明的模态公式的集合。我们稍微修改了这个概念，要求算术实现来自一个指定的集合$Γ$。我们对可解释性逻辑做了类似的修改。这是2012年的一篇论文。我们首先研究了具有限制实现的可证明性逻辑，并表明对于理论T和限制集$Γ$的各种自然候选者，其中$Γ$中的每个句子在T中具有很好理解的（Meta）数学内容，结果是线性框架的逻辑。然而，对于理论原始递归算术（PRA），我们定义了一个片段，通过利用PRA和I $Σ_1$之间的良好研究关系，产生了一个更有趣的可证明性逻辑。然后，我们研究可解释性逻辑，获得IL（PRA）的一些上界，其特征仍然是一个主要的开放问题，在可解释性逻辑。同样，这个上界与线性标架密切相关。该技术也被应用于产生IL（PRA）$\subset$ ILM的非平凡结果。
2020-06-18 math.LO
Unification in subsystem J$_2$ of provability logic GLB
本文推广 S. Ghilardi 的方法应用于双模态可证性逻辑 GLB 的子系统 J$_2$，利用 Kripke 语义描述投影公式，证明其具有有限统一类型，并得出其可容许性问题可判定的结论。
2024-03-25 math.LO
Provability interpretation of non-normal modal logics having neighborhood semantics
本文提出了一种基于邻域语义的新方法，用于研究非正则模态逻辑的算术完备性定理。
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
A cut-free proof system for a predicate extension of the logic of provability
本文介绍了一个证明系统$\mathsf{NQGL}$，它是由$\mathbf{K}$和Löb公式$\Box(\Box p\supset p)\supset\Box p$定义的逻辑$\mathbf{GL}$的Kripke完全谓词扩展，即可证性逻辑. $\mathsf{NQGL}$是Gentzen微积分$\mathsf{LK}$的模态扩展。虽然$\mathsf{NQGL}$的命题片段公理化了$\mathbf{GL}$，但它没有Löb公式作为它的公理。相反，它有一个非紧规则，即一个具有可数个前提的推导规则。我们证明了$\mathsf{NQGL}$具有割容许性，并且对于Kripke框架类是完备的，使得对于每个世界，从世界出发的路径长度的上确界是有限的。
2018-02-28 math.LO
Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic
本文确定了海廷算术量词可证性逻辑的严格正片段，证明其可判定且与皮亚诺算术的对应片段一致，并给出了严格正片段的简单公理化，解决了先前猜想。
2023-12-22 math.LO
Positive provability logic for uniform reflection principles
我们处理的片段模态逻辑组成的公式的影响，建立了从变量和常数“真”的合取和钻石。较弱的语言允许人们将菱形解释为算术中的统一反射模式，可能具有不受限制的逻辑复杂性。我们用自然数和ω表示一个算术完全演算，其中ω对应于完全一致反射模式，而n<ω对应于它对算术n+1公式的限制.这种演算被证明是完整的w.r.t.一个合适的类有限Kripke模型和可判定的多项式时间。
2013-07-15 math.LO
(Non-)well-founded derivations in the provability logic $\mathsf{GLP}$
本文研究了可证性逻辑 $\mathsf{GLP}$ 中的循环、非良基和良基推导，证明其非良基与良基推导定义了相同的无穷扩张，并确立该扩张及原始系统在广义后承关系下的强代数性与邻域完备性。
2025-04-02 math.LO
Models of transfinite provability logic
对于任何序数Λ，我们可以定义一个多模态逻辑GLP（Λ），对于每个Λ <Λ，都有一个模态[Λ]。这些表示强度增加的可证明性谓词。虽然GLP（Λ）没有Kripke模型，但Ignatiev证明，确实可以用自然数模态构建无变量片段的Kripke模型。后来，Icard为同一片段定义了一个拓扑模型，这与Ignatiev的非常密切相关。在本文中，我们展示了如何推广这些结构任意Λ。更一般地，对于每个Θ，Λ，我们建立了Kripke模型I（Θ，Λ）和拓扑模型T（Θ，Λ），并表明GLP（Λ）的闭合片段对于这两种结构都是合理的，并且是完整的，只要Θ足够大。
2012-04-21 math.LO
A formal proof of modal completeness for provability logic
本研究在HOL Light定理证明器中实现哥德尔-勒布可证性逻辑（GL）模态完备性的形式化证明，介绍实现细节与非标准证明结构选择，并分析该形式化系统推理的优缺点。
2021-02-11 cs.LO math.LO
Monadic Intuitionistic and Modal Logics Admitting Provability Interpretations
哥德尔翻译提供了一种将直觉主义逻辑$\mathsf{IPC}$嵌入模态逻辑$\mathsf{Grz}$的方法，然后模态逻辑通过分裂翻译嵌入模态逻辑$\mathsf{GL}$。结合Solovay定理，$\mathsf{GL}$是Peano算术$\mathsf{PA}$的可证性谓词的模态逻辑，$\mathsf{IPC}$和$\mathsf{Grz}$都允许算术解释。当试图将这些结果“提升”到这些逻辑的一元扩展$\mathsf{MIPC}$、$\mathsf{MGrz}$和$\mathsf{MGL}$时，相同的技术不再起作用。根据Esakia的猜想，我们将Casari公式的适当版本添加到这些一元扩展中（用"+“表示），得到哥德尔翻译将$\mathsf{M^{+}IPC}$嵌入$\mathsf{M^{+}Grz}$，分裂翻译将$\mathsf{M^{+}Grz}$嵌入$\mathsf{MGL}$。正如Japaridze所证明的那样，Solovay的结果扩展到一元系统$\mathsf{MGL}$，这使我们对$\mathsf{M^{+}IPC}$和$\mathsf{M^{+}Grz}$都有了算术解释。
2021-03-21 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
Modal logics of conjunctively closed provability predicates
Graduate School of System Informatics, Kobe University（神户大学系统信息研究生院）
研究与满足特定可推导性条件的可证性谓词对应的非正规模态逻辑，引入基于闭包算子的新语义，证明了多个非正规模态逻辑的模态完全性及一些逻辑的算术完全性定理。
2026-07-10 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
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
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
Two series of formalized interpretability principles for weak systems of arithmetic
理论$T$的可证明性逻辑将$T$中形式化可证明性的结构行为捕获为在$T$本身中可证明。像可证明性一样，人们可以形式化相对可解释性的概念，从而产生可解释性逻辑。在可证明性逻辑对于所有适度合理的理论都是相同的情况下，可解释性逻辑确实表现出变化。逻辑IL（All）被定义为模态原则的集合，这些模态原则在任何适度可靠的理论中都是可以证明的。在本文中，我们提出了以前已知的下界IL（所有）展示两个系列的原则，这是证明在任何这样的理论。此外，我们计算这两个系列的框架条件的集合。
2015-03-31 math.LO
Deducibility and Independence in Beklemishev's Autonomous Provability Calculus
Beklemishev基于可证代数的自治展开为Feferman-Schütte序数$Γ_0$引入了一个序数记号系统。在本文中，我们提出的逻辑$\textbf{BC}$（为微积分）。$\textbf{BC}$的语言将所述序数记号法系统扩展到严格肯定模态语言。因此，与其他可证明性逻辑不同，$\textbf{BC}$基于自包含签名，该自包含签名产生序数记号系统，而不是由先验给定的某个序数索引的模态。证明了该逻辑等价于$\textbf{RC}_{Γ_0}$，即等价于$\textbf{GLP}_{Γ_0}$的严格正片段.然后，我们定义了一个组合语句的基础上$\textbf{BC}$和证明它是独立的理论$\textbf{ATR}_0$的算术超限递归，一个理论的二阶算术远比皮亚诺算术更强大。
2020-08-31 math.LO
Nested Sequents for Provability Logic GLP
本文提出了一种基于嵌套相继式的可证性逻辑GLP证明系统，证明了切消定理，并以此在语法上将GLP归约为其重要片段J。
2014-10-24 cs.LO math.LO
Topological interpretations of provability logic
可证明性逻辑关注模态$\Box$作为形式系统（如皮亚诺算法）中的可证明性的研究。自然的，虽然相当令人惊讶，拓扑解释的可证明性逻辑已经发现在1970年的哈罗德西蒙斯和利奥Esakia。他们观察到，对偶$\Diamond$模态，对应于形式算术中的一致性，具有作用于离散空间的拓扑导数算子的所有基本性质。这个主题已经成为由埃萨基亚领导的格鲁吉亚逻辑学派的一个长期项目，偶尔也会有其他地方的贡献。最近，一个新的动力来自于对多模态可证明性逻辑GLP的研究，该逻辑被认为是Kripke不完全的，并且通常具有比其单峰对应物更复杂的行为。拓扑语义提供了一个更好的替代Kripke模型的意义上，GLP被证明是拓扑完整的。与此同时，与集合论和大基数的新的迷人的联系已经出现。我们给出了一个调查的结果，拓扑语义的可证明性逻辑从第一个贡献的Esakia。然而，一个特别的重点放在最近的工作多模态可证明性逻辑的拓扑模型。我们还包括一些迄今为止尚未发表的结果，最值得注意的是第6节（由于第二作者）和第10节，第11节（由于第一作者）的结果。
2012-10-27 math.GN math.LO
A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。
2025-06-17 cs.LO math.LO
A Many-Sorted Variant of Japaridze's Polymodal Provability Logic
我们考虑了Japaridze的多模态可证明性逻辑$\mathsf{GLP}$的一个多排序变体。在这个变体中，它被表示为$\mathsf{GLP}^\ast$，命题变元被分配排序$α\leq ω$，其中有限排序的变量$n < ω$被解释为算术层次的$Π_{n+1}$ -语句，而排序为$ω$的变量在任意的语句上变化。我们证明了$\mathsf{GLP}^\ast$是算术完全的关于这个解释。此外，我们将$\mathsf{GLP}^\ast$与它的单排序对应物$\mathsf{GLP}$联系起来，并证明了前者继承了后者的一些众所周知的性质，如Craig插值和PSpace可判定性。我们还研究了$\mathsf{GLP}^\ast$的一个积极的变体，它允许更丰富的算术解释-变量被允许在理论范围内，而不是单个句子。这种解释反过来又允许引入一种对应于完全一致反射原理的模态。我们证明了$\mathsf{GLP}^\ast$的正变体是算术完全的。
2019-06-21 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
本文研究了某些纯必然逻辑扩展的算术完备性，证明了这些扩展作为可证明性逻辑的性质。
2025-11-20 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
Arithmetical completeness theorems for monotonic modal logics
本文研究了满足条件M的可证性谓词的模态逻辑性质，证明了五种单调模态逻辑的算术完全性定理，并从模态逻辑角度区分了一致性陈述的两种不同形式化。
2023-04-01 math.LO
An $ω$-rule for the logic of provability and its models
研究配备 $ω$-规则的可证性逻辑证明系统 $\mathsf{NGL}$，区分三类均刻画 GL 的传递 Kripke 框架，并代数证明其完全性及相关模态代数类非簇。
2023-11-02 math.LO
The many faces of omega-logic
我们考虑了“公式$ϕ$是$ω$ -逻辑的一个定理”的二阶算术语言的几种形式化，包括一些文献中已经研究过的形式化和一个通过最小不动点定义的新变体.我们分析了这些不同的形式化之间的关系，在标准理论的反向数学的可证明性。有了这个，我们研究了各种反射原理的强度所产生的这些概念的可证明性，调查已知的结果，并建立一些新的等价，包括一个表征的$Π^1_1$ - ${\sf CA}_0$在我们的不动点形式化的$ω$ -逻辑。
2022-03-22 math.LO
The modal logic of forcing
在集合论中，关于强制性和真的最一般的原则是什么？与索洛维著名的可证明性分析一样，这个问题和它的答案都是用模态逻辑自然形成的。我们的目标是为可强制性做索洛维为可证明性做的事情。一个集合理论断言psi是可强制的或可能的，如果psi在某个强制扩张中成立，并且是必要的，如果psi在所有力迫扩张中成立。在这种对模态逻辑的强制解释中，我们建立了，如果ZFC是相容的，那么强制的ZFC可证明原则就是模态理论中被称为S4.2的那些原则。
2005-09-27 math.LO
Refinements of provability and consistency principles for the second incompleteness theorem
本文延续先前研究，证明受非正规模态逻辑启发的弱原理足以推导第二不完备定理的精化形式，并确立了特定原理集合能证明一致性陈述的不可证性及形式化的 $Σ_1$-完备性。
2025-08-11 math.LO
