Mohammad Golshani, Reihane Zoghifard
Assuming the existence of suitable large cardinals, we show it is consistent that the Provability logic $\mathbf{GL}$ is complete with respect to the filter sequence of normal measures. This result answers a question of Andreas Blass from 1990 and a related question of Beklemishev and Joosten.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
In this paper, we study the provability logic of intuitionistic theories of arithmetic that prove their own completeness. We prove a completeness theorem for theories equipped with two provability predicates $\Box$ and $\triangle$ that prove the schemes $A\to\triangle A$ and $\Box\triangle S\to\Box S$ for $S\inΣ_1$. Using this theorem, we determine the logic of fast provability for a number of intuitionistic theories. Furthermore, we reprove a theorem previously obtained by M. Ardeshir and S. Mojtaba Mojtahedi determining the $Σ_1$-provability logic of Heyting Arithmetic.
We prove a topological completeness theorem for the modal logic GLP containing operators $\langleλ\rangle$ for $λ\in$ Ord intended to capture progressively stronger notions of consistency in mathematical theories. We show that, given a scattered space $X$ of large-enough rank, any sentence $ϕ$ consistent with GLP can be satisfied in a polytopological space based on the finitely many Icard topologies over $X$ that correspond to the finitely many modalities appearing in $ϕ$.
Completeness and Well-Definability of a Provability Degree Measure in Sufficiently Powerful Formal Systems, and Finite-Time Effective Knowers
该研究证明足够强大形式系统中特定可证性程度测度的完备性与良定性，构造出最优有限时间定理认知者φ'，并揭示其与无界归纳计算的关联及对计算过程最终行为的意义。
Provability Models
本文提出名为可证性模型的经典模态逻辑新型克里普克式语义，证明了多类模态逻辑、解释性逻辑ILM对该类模型的可靠性与完全性，并将其改进为谓词可判定版本。
Strong Completeness of Provability Logic for Uncountable Languages
本文利用Erdős-Rado定理证明了对于特定基数的模态语言，GL逻辑在广义Icard拓扑下不满足强完备性，并引入了两种拓扑空间类以证明GL和GL.3在特定语言下满足强完备性。
Provability logic GLP is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces satisfying all the axioms of GLP are called GLP-spaces. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces.
In 1933, Gödel considered two modal approaches to describing provability. One captured formal provability and resulted in the logic GL and Solovay's Completeness Theorem. The other was based on the modal logic S4 and led to Artemov's Logic of Proofs LP. In this paper, we study introduced by the author logic GLA, which is a fusion of GL and LP in the union of their languages. GLA is supplied with a Kripke-style semantics and the corresponding completeness theorem. Soundness and completeness of GLA with respect to the arithmetical provability semantics is established.
Provability interpretation of non-normal modal logics having neighborhood semantics
本文提出了一种基于邻域语义的新方法，用于研究非正则模态逻辑的算术完备性定理。
By Solovay's celebrated completeness result on formal provability we know that the provability logic $\mathrm GL$ describes exactly all provable structural properties for any sound and strong enough arithmetical theory with a decidable axiomatisation. Japaridze generalised this result by considering a polymodal version $\mathrm GLP$ of $\mathrm GL$ with modalities $[n]$ for each natural number $n$ referring to ever increasing notions of provability. Modern treatments of $\mathrm GLP$ tend to interpret the $[n]$ provability notion as "provable in a base theory $T$ together with all true $Π^0_n$…
The branch of provability logic investigates the provability-based behavior of the mathematical theories. In a more precise way, it studies the relation between a mathematical theory $T$ and a modal logic $L$ via the provability interpretation which interprets the modality as the provability predicate of $T$. In this paper we will extend this relation to investigate the provability-based behavior of a hierarchy of theories. More precisely, using the modal language with infinitely many modalities, $\{\Box_n\}_{n=0}^{\infty}$, we will define the hierarchical counterparts of some of the classical…
(Non-)well-founded derivations in the provability logic $\mathsf{GLP}$
本文研究了可证性逻辑 $\mathsf{GLP}$ 中的循环、非良基和良基推导，证明其非良基与良基推导定义了相同的无穷扩张，并确立该扩张及原始系统在广义后承关系下的强代数性与邻域完备性。
A formal proof of modal completeness for provability logic
本研究在HOL Light定理证明器中实现哥德尔-勒布可证性逻辑（GL）模态完备性的形式化证明，介绍实现细节与非标准证明结构选择，并分析该形式化系统推理的优缺点。
Completeness of the Gödel--Löb Provability Logic for Finite Derived Ordinal Topologies
本文在假设 GCH 和存在带相干测度序列的可测基数下，构造保持共尾性和 GCH 的力迫扩张，证明有限导出序数拓扑的 Gödel--Löb 逻辑完备性，并扩展 Beklemishev 定理至双模态逻辑。
In this paper we consider transfinite provability logics where for each ordinal in some recursive well-order we have a corresponding modal provability operator. The modality [xi] will be interpreted as "provable in ACA_0 together with at most xi nested applications of the omega rule". We show how to formalize this in in second order number theory. Next we prove both soundness and completeness under this interpretation. We conclude by showing how one can lower the base theory ACA_0 to theories below RCA_0.
Let $\mathcal{PL}({\sf T},{\sf T}')$ and $\mathcal{PL}_{Σ_1}({\sf T},{\sf T}')$ respectively indicates the provability logic and $Σ_1$-provability logic of ${\sf T}$ relative in ${\sf T}'$. In this paper we characterize the following relative provability logics: $\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…
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 topo…
Abashidze and Blass independently proved that the modal logic $\sf{GL}$ is complete for its topological interpretation over any ordinal greater than or equal to $ω^ω$ equipped with the interval topology. Icard later introduced a family of topologies $\mathcal I_λ$ for $λ< ω$, with the purpose of providing semantics for Japaridze's polymodal logic $\sf{GLP}$ $_ω$. Icard's construction was later extended by Joosten and the second author to arbitrary ordinals $λ\geq ω$. We further generalize Icard topologies in this article. Given a scattered space $\mathfrak X = (X, τ)$ and an ordinal $λ$, we de…
Modal logical aspects of provability predicates and consistency statements
本文通过扩展Solovay方法和改进Arai的Rosser可证性谓词构造，建立了逻辑NP、ND、NP4和ND4的算术完全性。
Modal logics of conjunctively closed provability predicates
研究与满足特定可推导性条件的可证性谓词对应的非正规模态逻辑，引入基于闭包算子的新语义，证明了多个非正规模态逻辑的模态完全性及一些逻辑的算术完全性定理。
Finite Kripke models and provability interpretations in quantified modal logic
本文研究了有限克里普克模型在量化模态逻辑中的算术完备性，通过Artemov和Japaridze的有限模型嵌入技术，构建了两种不同场景下的可证明性谓词和算术解释。
The Modal Logic of Provability and Forcing
本文研究可证性与力迫在模态逻辑中的交互，提出双模态逻辑 PF 及 PF^ω，并分别刻画一般情形与集合论 ω-模型中的对应逻辑。
In this paper we present a new proof of Solovay's theorem on arithmetical completeness of Gödel-Löb provability logic GL. Originally, completeness of GL with respect to interpretation of $\Box$ as provability in PA was proved by R. Solovay in 1976. The key part of Solovay's proof was his construction of an arithmetical evaluation for a given modal formula that made the formula unprovable PA if it were unprovable in GL. The arithmetical sentences for the evaluations were constructed using certain arithmetical fixed points. The method developed by Solovay have been used for establishing similar …
Arithmetical completeness for some extensions of the pure logic of necessitation
本文研究了某些纯必然逻辑扩展的算术完备性，证明了这些扩展作为可证明性逻辑的性质。
Arithmetical completeness theorems for monotonic modal logics
本文研究了满足条件M的可证性谓词的模态逻辑性质，证明了五种单调模态逻辑的算术完全性定理，并从模态逻辑角度区分了一致性陈述的两种不同形式化。
In 1994 Jech gave a model theoretic proof of Gödel's second incompleteness theorem for Zermelo-Fraenkel set theory in the following form: ZF does not prove that ZF has a model. Kotlarski showed that Jech's proof can be adapted to Peano Arithmetic with the role of models being taken by complete consistent extensions. In this note we take another step in the direction of replacing proof-theoretic by model-theoretic arguments. We show, without passing through the arithmetized completeness theorem, that the existence of a model of PA of complexity $Σ^0_2$ is independent of PA, where a model is ide…
Mechanizing Gödel's Incompleteness Theorems and Provability Logic
该研究在Lean 4中形式化验证了哥德尔不完备定理及可证性逻辑GL的Solovay完备性，为数学基础提供机器证明。
A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。
Infinitary provability logic
本文研究Gödel-Löb可证性逻辑的无穷性对应物，提出非良基深层推理系统$\dgla$，证明其相对于良基传递Kripke框架的可靠性与完备性，并借助Kripke-Platek集合论建立无穷可证性解释，表明Hilbert式变体可靠，且在某些条件下无穷可证性逻辑介于两者之间。
Mechanising Gödel-Löb provability logic in HOL Light
该论文在HOL Light中形式化了Gödel-Löb可证性逻辑的元理论，证明可靠性与完备性，并实现了一个基于G3KGL演算的判定算法作为定理证明器策略。
An Escape from Vardanyan's Theorem
针对Vardanyan定理关于皮亚诺算术量化可证性逻辑不可计算公理化的结论在严格正签名下无法证明的问题，研究推广Kripke可靠性与完全性证明得常域完全性，通过Solovay型构造证明QRC₁系统的算术语义完全性，明确其为QGL严格正片段及QPL(PA)的片段。
Strong completeness of the logic J
该研究证明多模态逻辑J相对于J-花束是强完备的，进而得到可证性逻辑GLP的完备性结果，同时通过反例说明GLP相对于Beklemishev-Gabelaia空间不具备强完备性。
An $ω$-rule for the logic of provability and its models
研究配备 $ω$-规则的可证性逻辑证明系统 $\mathsf{NGL}$，区分三类均刻画 GL 的传递 Kripke 框架，并代数证明其完全性及相关模态代数类非簇。
This paper presents the logic QRC$_1$, which is a strictly positive fragment of quantified modal logic. The intended reading of the diamond modality is that of consistency of a formal theory. Predicate symbols are interpreted as parametrized axiomatizations. We prove arithmetical soundness of the logic QRC$_1$ with respect to this arithmetical interpretation. Quantified provability logic is known to be undecidable. However, the undecidability proof cannot be performed in our signature and arithmetical reading. We conjecture the logic QRC$_1$ to be arithmetically complete. This paper takes the …
An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem
本文在直觉主义二阶算术中形式化修改版 Henkin 完备性证明，并借助 Curry-Howard 对应将其刻画为把 Tarski 有效性证明转换为可推导性证明的程序。
Comparing and Contrasting Arrow's Impossibility Theorem and Gödel's Incompleteness Theorem
本文引入自指涉系统这一一般数学对象，通过抽象对角化与不动点论证，形式化阿罗不可能定理与哥德尔第一不完备定理之间的对应关系，并揭示两者产生不可能性机制的细微差异。
Considering classical first-order logic with equality, we give a "fully syntactic" construction of the (weak) syntactic category $\text{Syn}(T)$ associated to a consistent theory $T$; we show it is a consistent coherent category; and we show that a morphism of coherent categories $\text{Syn}(T)\to \bf{Set}$ gives rise to a model $\mathcal{M}$ of $T$ in the usual sense. We then invoke Deligne's theorem on small consistent coherent categories.
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。