Rosser provability and normal modal logics
本文研究了可证逻辑为正规模态逻辑的Rosser可证谓词。首先，我们证明了存在一个Rosser可证明性谓词，其可证明性逻辑恰为正规模态逻辑${\sf KD}$。其次，我们引入了一个新的正规模态逻辑${\sf KDR}$，它是${\sf KD}$的一个适当扩展，并证明了存在一个Rosser可证明性谓词，其可证明性逻辑包含${\sf KDR}$。
2019-05-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
Arithmetical completeness for some extensions of the pure logic of necessitation
Graduate School of System Informatics, Kobe University（神户大学系统信息学研究科）
本文研究了某些纯必然逻辑扩展的算术完备性，证明了这些扩展作为可证明性逻辑的性质。
2025-11-20 math.LO
The provability logic of all provability predicates
本文证明所有可证性谓词的可证性逻辑恰为纯必然化逻辑N，并引入其三个扩展N4、NR和NR4，分别刻画满足特定条件的各类可证性谓词，研究其算术语义。
2023-09-01 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
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
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
Modal logical aspects of provability predicates and consistency statements
Kobe University（神户大学）
本文通过扩展Solovay方法和改进Arai的Rosser可证性谓词构造，建立了逻辑NP、ND、NP4和ND4的算术完全性。
2026-06-12 math.LO
Provability Models
Ghent University（根特大学）；University of Bern（伯尔尼大学）
本文提出名为可证性模型的经典模态逻辑新型克里普克式语义，证明了多类模态逻辑、解释性逻辑ILM对该类模型的可靠性与完全性，并将其改进为谓词可判定版本。
2025-11-19 math.LO
Axiomatizing provable $n$-provability
一个公式$ϕ$在形式算术理论$S$中被称为\emph{$n$-provable}，如果$ϕ$在$S$中连同所有真算术$Π_{n}$ -语句一起被证明为附加公理。虽然一般来说，对于固定的$n>0$，所有$n$可证明公式的集合不是递归可证明的，但是其$n$可证明性在给定的r. e.中是可证明的公式的集合$ϕ$是递归可证明的。元理论$T$是r.e.这个集合是演绎封闭的，并且通常是$S$的扩展。我们证明，这些理论可以自然公理化的迭代局部反射原则的进展。特别地，Peano算术PA的可证1-可证语句集可以用PA上的$\varepsilon_0$倍迭代局部反射模式公理化.我们的特征产生额外的信息，这些理论的证明理论的强度（w.r.t.各种措施），并对他们的axiomatizability。我们还研究了问题的加速证明，并表明，在某些情况下，证明$n$证明的句子可以比它的证明迭代反射原则。
2018-05-01 math.LO
On the Provability Logic of HA
Department of Mathematics, Statistics and Computer Science, College of Sciences, University of Tehran（德黑兰大学理学院数学、统计与计算机科学系）；Department of Mathematics WE16, Ghent University（根特大学WE16数学系）
本文研究了HA的可证逻辑，提出了可证模型语义，并证明了其可判定性，同时探讨了扩展iK4的模态逻辑的保持性和相对可接受性关系。
2026-01-02 math.LO
Arithmetical and Hyperarithmetical Worm Battles
Japaridze的可证明性逻辑$GLP$对每个自然数都有一个模态$[n]$，并且已经被Beklemishev用于Peano aritime $(PA)$和相关理论的证明理论分析。除了其他好处之外，这种分析产生了所谓的“每虫都死”$(EWD)$原则，这是一种独立于$PA$的自然组合语句。最近，Beklemishev和Pakhomov研究了$GLP$中超限模态的可证明性概念。我们表明，的确是自然的超限扩展$GLP$是健全的这种解释，并产生独立的组合原则的二阶理论$ACA$的算术理解与充分的感应。我们还提供了与Peano算法的片段$IΣ_n$相关的$EWD$的限制版本。为了证明后者，我们表明，标准的哈代函数优化其变种的基础上树序数。
2022-06-29 math.LO
Provability Logic and the Completeness Principle
在本文中，我们研究证明自己的完备性的算术直觉理论的可证性逻辑。我们证明了一个完备性定理的理论配备了两个证明谓词$\Box$和$\triangle$证明方案$A\to\triangle A$和$\Box\triangle S\to\Box S$为$S\inΣ_1$。利用这个定理，我们确定了一些直觉理论的快速可证性逻辑。此外，我们重新证明了M. Ardeshir和S. Mojtaba Mojtahedi确定Heyting算术的$Σ_1$可证明性逻辑。
2018-06-05 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
Arithmetical completeness theorems for monotonic modal logics
本文研究了满足条件M的可证性谓词的模态逻辑性质，证明了五种单调模态逻辑的算术完全性定理，并从模态逻辑角度区分了一致性陈述的两种不同形式化。
2023-04-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
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
Completeness of the Gödel-Löb provability logic for the filter sequence of normal measures
假设存在合适的大基数，我们证明了可证性逻辑$\mathbf{GL}$关于正规测度的滤子序列是完备的。这个结果回答了Andreas Blass在1990年提出的一个问题，以及Beklemishev和Joosten提出的一个相关问题。
2023-02-23 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
On provability logics with linearly ordered modalities
我们引入了逻辑GLP（Λ），它是贾帕里泽的多模态可证明性逻辑GLP（ω）的推广，其中Λ是表示强度递增的可证明性算子层次的任何线性有序集。我们将提供这些逻辑到GLP（ω）的一个约化，除其他外，给出GLP（Λ）的无变量片段的规范形定理的有限性证明和GLP（Λ）对于递归序Λ的可判定性。进一步，我们给出了GLP（Λ）的无变量片段的限制公理化.
2012-10-17 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 omega-rule interpretation of transfinite provability logic
在本文中，我们考虑超限可证明性逻辑，其中对于某些递归良序中的每个序数，我们都有一个对应的模态可证明性算子。模态[xi]将被解释为“在ACA_0中可证明的，最多可与omega规则的xi个嵌套应用一起”。我们将展示如何在二阶数论中对此进行形式化。接下来，我们证明在这种解释下的可靠性和完备性。最后，我们展示了如何将基础理论ACA_0降低到低于RCA_0的理论。
2013-02-21 math.LO
Interpolation properties for the bimodal provability logic $\mathbf{GR}$
本文研究双模态可证性逻辑GR的内插性质，通过引入新子逻辑GR°及其关系语义，证明了二者满足Lyndon与一致内插性质。
2023-11-17 math.LO
Unification in subsystem J$_2$ of provability logic GLB
本文推广 S. Ghilardi 的方法应用于双模态可证性逻辑 GLB 的子系统 J$_2$，利用 Kripke 语义描述投影公式，证明其具有有限统一类型，并得出其可容许性问题可判定的结论。
2024-03-25 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
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 Topological Completeness Theorem for Transfinite Provability Logic
我们证明了一个拓扑完备性定理的模态逻辑GLP包含运营商$\langleλ\rangle$为$λ\in$ Ord旨在捕捉逐步加强概念的数学理论的一致性。我们表明，给定一个足够大的秩的分散空间$X$，任何句子$ϕ$符合GLP可以满足在一个多拓扑空间的基础上的多个Icard拓扑在$X$，对应于多个模态出现在$ϕ$。
2019-05-06 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
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
Models of transfinite provability logic
对于任何序数Λ，我们可以定义一个多模态逻辑GLP（Λ），对于每个Λ <Λ，都有一个模态[Λ]。这些表示强度增加的可证明性谓词。虽然GLP（Λ）没有Kripke模型，但Ignatiev证明，确实可以用自然数模态构建无变量片段的Kripke模型。后来，Icard为同一片段定义了一个拓扑模型，这与Ignatiev的非常密切相关。在本文中，我们展示了如何推广这些结构任意Λ。更一般地，对于每个Θ，Λ，我们建立了Kripke模型I（Θ，Λ）和拓扑模型T（Θ，Λ），并表明GLP（Λ）的闭合片段对于这两种结构都是合理的，并且是完整的，只要Θ足够大。
2012-04-21 math.LO
Modal logics of conjunctively closed provability predicates
Graduate School of System Informatics, Kobe University（神户大学系统信息研究生院）
研究与满足特定可推导性条件的可证性谓词对应的非正规模态逻辑，引入基于闭包算子的新语义，证明了多个非正规模态逻辑的模态完全性及一些逻辑的算术完全性定理。
2026-07-10 math.LO
(Non-)well-founded derivations in the provability logic $\mathsf{GLP}$
本文研究了可证性逻辑 $\mathsf{GLP}$ 中的循环、非良基和良基推导，证明其非良基与良基推导定义了相同的无穷扩张，并确立该扩张及原始系统在广义后承关系下的强代数性与邻域完备性。
2025-04-02 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
Quantified Reflection Calculus with one modality
本文提出了QRC逻辑$_1$，它是量化模态逻辑的严格正片段.对菱形模态的预期解读是形式理论的一致性。谓词符号被解释为参数化公理化。我们证明了算术可靠的逻辑QRC $_1$关于这个算术解释。量化的可证明性逻辑是不可判定的。然而，不可判定性证明不能在我们的签名和算术阅读中进行。我们猜想逻辑QRC $_1$是算术完备的.本文采取的第一步，通过提供关系语义QRC $_1$与相应的完整性证明算术的完整性。我们还展示了有限模型的属性，这意味着可判定性。
2020-03-30 math.LO
Two series of formalized interpretability principles for weak systems of arithmetic
理论$T$的可证明性逻辑将$T$中形式化可证明性的结构行为捕获为在$T$本身中可证明。像可证明性一样，人们可以形式化相对可解释性的概念，从而产生可解释性逻辑。在可证明性逻辑对于所有适度合理的理论都是相同的情况下，可解释性逻辑确实表现出变化。逻辑IL（All）被定义为模态原则的集合，这些模态原则在任何适度可靠的理论中都是可以证明的。在本文中，我们提出了以前已知的下界IL（所有）展示两个系列的原则，这是证明在任何这样的理论。此外，我们计算这两个系列的框架条件的集合。
2015-03-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
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
The interpretability logic of all reasonable arithmetical theories
2000年的这篇论文是对当时的一个状态问题的介绍，即{ \em all}/合理算术理论的可解释性逻辑问题。我们提出的算术方面和模态方面的问题。
2020-04-27 math.LO
A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。
2025-06-17 cs.LO math.LO
Yablo's Paradox And Arithmetical Incompleteness
在这篇简短的论文中，我提出了几个定理的句子算术这是有关雅布洛的Paradigas哥德尔的第一个不可判定的句子是有关的骗子悖论。特别是，我认为两个不同的arithemetizations雅布洛的句子：一个类似哥德尔的arithemetizations的骗子，与否定外的可证明性谓词，一个类似杰罗斯洛的不可判定的句子，与否定内。这两种算术化的Yablo句子都是不可判定的，并且与环境形式系统的一致性句子的连接方式大致与哥德尔和杰罗斯洛的句子相同。最后，我考虑一个句子，这是相关的亨金句“我是可证明的”，以同样的方式，前两个算术是相关的哥德尔和杰罗斯洛的句子。我证明了这个句子是可证明的，使用Löb定理，就像Henkin句子的标准证明一样。
2011-12-18 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
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
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
Feferman Interpretability
本文引入模态逻辑 FIL 以处理 Feferman 可解释性，通过带标签的模态调整底层理论的公理集，证明了多种可解释性原理在弱算术理论中的可靠性。
2024-06-26 math.LO
Solution of some problems in the arithmetical complexity of first-order fuzzy logics
这篇简短的论文讨论了佛朗哥·蒙塔格纳和卡莱斯·诺盖拉在前一篇论文中留下的开放性问题。除了解决这两个问题外，还对全词汇表（包括函数符号）在证明中的作用作了一些澄清。
2011-11-25 math.LO
