Feferman's completeness theorem
本文旨在通过提供Feferman完备性定理的两个新证明来阐明该结果，并结合可计算结构理论为算术层级各层完备性所需的良序序型给出精确界限。
2024-09-23 math.LO
Cartesian closed varieties I: the classification theorem
1990年，Johnstone给出了方程理论的一个句法特征，其相关的变量是Carnival封闭的。在这些理论中，所有的一元理论--其模型是由幺半群M赋予作用的集合--和所有的超仿射理论--其模型是由布尔代数B赋予作用的集合。我们改进Johnstone的结果表明，一个方程的理论是carnival封闭的，只是当它的操作有一个独特的超仿射一元分解。由此可以得出，任何非退化的卡氏闭簇都是由幺半群M和布尔代数B装配有相容作用的集合的簇;这是标题的分类定理。
2023-02-10 math.CT math.LO
A Topological Completeness Theorem for Transfinite Provability Logic
我们证明了一个拓扑完备性定理的模态逻辑GLP包含运营商$\langleλ\rangle$为$λ\in$ Ord旨在捕捉逐步加强概念的数学理论的一致性。我们表明，给定一个足够大的秩的分散空间$X$，任何句子$ϕ$符合GLP可以满足在一个多拓扑空间的基础上的多个Icard拓扑在$X$，对应于多个模态出现在$ϕ$。
2019-05-06 math.LO
Strong standard completeness theorems for S5-modal Lukasiewicz logics
本文研究基于Łukasiewicz t-范数的逻辑的S5模态扩张，通过构造有穷命题演算并引入无穷规则，借助monadic MV-代数的函数表示与有限嵌入性质，证明了有限强完备性与强完备性定理，并推广到有界论域模型。
2024-08-08 math.LO
A completeness theorem in proof-theoretic semantics via set-theoretic semantics
本文以原子二阶直觉主义命题逻辑为系统，借助 Okada 与 Takemura 的带证明项相语义构造闭项论域模型，从而证明直觉主义逻辑相对于 Prawitz 证明论有效性的完备性。
2025-05-16 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
On the Multicategorical Meta-Theorem and the Completeness of Restricted Algebraic Deduction Systems
该研究在代数理论框架下建立8个范畴可靠性与完备性定理，构造上下文结构与结构范畴的双射对应及相关等式演绎系统，证明其在对应多范畴模型下的语义性质可转移。
2024-06-21 math.CT math.LO
Generalized effective completeness for continuous logic
本文给出了连续逻辑的一个广义有效完备性定理。主要的结果是，任何连续理论都满足于一个结构，它允许相同的图灵度的介绍。因此，任何可判定的理论都可以由一个可计算的可表示结构来满足。这修改和扩展了以前的部分有效完整性定理的连续逻辑给出的卡尔弗特和Didehvar，Ghasemloo，和Pourmahdian。
2022-02-22 math.LO
On the Blok-Esakia theorem for universal classes
Blok-Esakia定理指出，存在从中间逻辑格到Grzegorczyk模态逻辑的正规扩张格的同构。Emil Jeábek作为典范规则的一个应用得到了多结论推论关系的推广。我们表明，Jeanábek的结果如下已经从布洛克的代数证明。我们还证明了强结构完备性和强泛完备性的性质被保持并反映在上述同构中。这些性质分别与单结论推论关系的结构完备性和泛完备性相一致，特别是对于逻辑。
2018-10-22 math.LO
An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem
本文在直觉主义二阶算术中形式化修改版 Henkin 完备性证明，并借助 Curry-Howard 对应将其刻画为把 Tarski 有效性证明转换为可推导性证明的程序。
2024-01-24 math.LO
Classical theorems in the Implicational Propositional Calculus
对于经典命题演算（PC）的定理，我们证明了PC证明产生IPC证明的隐含命题演算（IPC）的公式。因此，PC的完备性产生IPC的完备性。
2016-02-06 math.LO
Constructive completeness and non-discrete languages
我们给出了一个分析和推广的一些长期建立的建设性完备性结果的范畴逻辑和预层和层语义。其目的在很大程度上是概念性的和组织性的：从一些基本成分中产生了一个更统一的画面，它将关于塔斯基语义的构造性完备性与关于预层和层语义的各种完备性定理（从而与克里普克和贝思语义）联系起来。从这幅图中获得了（“逆数学”）等价结果和新的构造性完备性定理;特别是，基本设置足够灵活，可以为任意大小的语言和签名元素之间的等式不可判定的语言获得强构造性完备性结果。
2017-09-18 math.LO
Completeness of the primitive recursive $ω$-rule
Shoenfield的完备性定理（1959）指出，每一个真正的一阶算术语句都有一个递归的$ω$ -证明，可以通过使用$ω$ -规则的递归应用进行编码。对于一个合适的编码根岑风格的$ω$ -证明，我们表明，Shoenfield的完整性定理适用于削减免费$ω$ -证明编码使用原始递归应用程序的$ω$ -规则。我们还表明，一套代码的$ω$证明，无论是基于递归或原始递归应用程序的$ω$规则，是$Π^1_1$完成。相同的$Π^1_1$完备性结果适用于无割$ω$证明的代码。
2021-10-04 math.LO
Effective Completeness for S4.3.1-Theories with Respect to Discrete Linear Models
针对Ganguli和Nerode的有效Henkin型构造无法证明S4.3.1理论关于ω序型线性序模型的有效完全性问题，提出改编自该构造的新方法，证明了该定理的有效化版本。
2025-04-16 math.LO
On structural completeness vs almost structural completeness problem: A discriminator varieties case study
我们研究以下问题：确定哪些几乎结构完备拟簇是结构完备的。我们提出了一个一般的解决方案，这个问题，然后在半简单的情况下的解决方案。作为一个结果，我们得到了一个结构完整的类簇的特征。逻辑中一个有趣的推论如下：设$L$是语言中一个相容的命题逻辑/演绎系统，其中包含用于真的公式，这是一个定理，而假的不是一个定理。还假定$L$具有由一个簇给出的适当语义。则$L$是结构完备的当且仅当它是极大的。所有这样的逻辑/演绎系统在结构上几乎是完整的。
2014-08-20 math.LO
A Completeness Theorem for "Total Boolean Functions"
Christine Tasson在向量空间范畴中为线性逻辑的指称模型引入了一个总体的代数概念。全布尔函数的概念在某种程度上是非常直观的。本文对布尔质心演算的完备性问题给出了肯定的回答。布尔函数
2009-11-03 cs.LO math.LO
A Completeness Theorem for Topological Doctrines
本文为带逐纤维内部与闭包算子的逻辑范畴建立完备性结果，证明在 Kuratowski 闭包、乘积独立性及环路收缩公理下可嵌入拓扑空间范畴的幂。
2025-07-28 math.CT math.LO
The doctrinal Gödel's completeness theorem and the type space functor
Université catholique de Louvain（天主教鲁汶大学）；Université Savoie Mont Blanc（萨瓦勃朗峰大学）
研究在一阶布尔教义形式体系内自证哥德尔完备性定理，表明该定理使一阶布尔教义的纤维式斯通对偶成为类型空间函子，阐述了公式布尔代数对偶与模型斯通空间的关系。
2026-07-24 math.CT math.LO
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
我们研究各种配方的完整性一阶逻辑措辞建设性类型论和机械化的Coq证明助手。具体而言，我们研究的经典和直觉主义的自然演绎和微积分的变种模型论，代数和博弈论语义的完整性。作为完整性方面的标准模型理论语义的塔斯基和Kripke是不容易建设性的，我们分析连接的完整性定理，马尔可夫原理和弱柯尼希引理，并讨论非标准的语义承认无故障的完整性。我们贡献了一个可重用的Coq库一阶逻辑包含本文所涉及的所有结果。
2021-12-14 cs.LO 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
Completeness and interpolation for intuitionistic infinitary predicate logic, in connection to finitizing the class of representable Heyting polyadic algebras
研究了Heyting多进代数的各种约简的表示定理。超合并证明了几个（自然约简）和我们的结果进行了比较，在经典代数逻辑处理圆柱和polyadic（布尔代数）的有限性问题。我们还证明了几个新的整齐嵌入定理，并得到了基于（广义）Kripke语义的可表示代数类与具有整齐嵌入性质的代数类，即那些代数是具有$ω$额外维数的代数的次整齐约化.
2013-04-04 math.LO
Completeness and Well-Definability of a Provability Degree Measure in Sufficiently Powerful Formal Systems, and Finite-Time Effective Knowers
该研究证明足够强大形式系统中特定可证性程度测度的完备性与良定性，构造出最优有限时间定理认知者φ'，并揭示其与无界归纳计算的关联及对计算过程最终行为的意义。
2024-11-27 math.LO
A Syntactic and Categorical Derivation of Gödel's Completeness Theorem
考虑到经典的一阶逻辑与平等，我们给出了一个“完全句法”的建设（弱）的语法范畴$\text{Syn}(T)$与一致的理论$T$，我们表明它是一个一致的连贯范畴，我们表明，态射的连贯范畴$\text{Syn}(T)\to \bf{Set}$产生的模型$\mathcal{M}$的$T$在通常意义上。然后，我们调用Deligne的小一致连贯范畴定理。
2021-11-11 math.CT math.LO
Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
通过对模型的操作，我们展示了如何将允许标称模型的完备性与有限支持的标称模型的完备性联系起来。有限支集模型是容许名义模型的一种特殊情况，因此构造取决于从后者的一个实例生成前者的某个实例，其中元素之间保留了足够多的不等式。我们这样做使用一个无限的广义的名义原子抽象。结果本身就很有趣，但我们也考虑了数学因素，以便最大限度地提高它也可以用于其他名义推理系统的机会。具有无限支撑的模型可以更容易地工作，因此有一个半自动定理将结果从无限支撑的名义模型类转移到具有有限支撑的更具限制性的模型类是有用的。最后，我们考虑不同的允许名义语法和名义模型，并讨论它们如何与这里证明的结果。
2011-12-05 cs.LO math.LO
Godel's Completeness Theorem and Deligne's Theorem
这些笔记是为2012年1月在巴黎第七大学的一次演讲而写的。其目的是解释一个著名的定理证明P.德利涅有关连贯拓扑（连贯拓扑有足够的点），并显示这个定理是如何等价于哥德尔的完备性定理的一阶逻辑。因为不可能在三个小时内涵盖所有内容，所以重点放在巴尔定理和德利涅定理上。这就解释了为什么对相应的章节给予了更多的关注。增加第1节和附录是为了使本文件自成一体，并使具有良好拓扑理论知识的读者能够理解。相干拓扑是等价于Grothendieck拓扑的拓扑，其允许一个站点$(C,J)$使得$C$具有有限极限并且存在具有有限覆盖族的$J$的基。为了证明任何相干拓扑都有足够的点，只要证明对于任何相干拓扑$\mathcal{E}$，有一个从有足够点的拓扑到$\mathcal{E}$的满射几何态射就足够了。当拓扑空间上的层拓扑有足够的点时，从某个$Sh(X)$到$\mathcal{E}$的任何满射几何态射都是充分的，其中$X$是拓扑空间。这是由巴尔定理提供的。这就是我们在这里所要采取的方法（遵循MacLane和Moerdijk的《几何和逻辑中的层组》）。
2013-09-02 math.CT math.LO
Beth definability and the Stone-Weierstrass Theorem
紧T2空间的Stone-Weierstrass定理是泛函分析的一个基本结果，具有深远的影响。我们介绍了一个方程逻辑$\vDash_Δ$与一个无限品种$Δ$和表明，斯通-维尔斯特拉斯定理是一个后果的贝思可定义性属性的$\vDash_Δ$，说明每一个隐式定义可以明确。进一步，我们定义了一个无穷命题逻辑$\vdash_Δ$，并证明了一个强完备性结果，由此与$\vdash_Δ$相关的结果的语义概念与$\vDash_Δ$一致.
2021-05-06 math.FA math.GN math.LO
A formal proof of modal completeness for provability logic
本研究在HOL Light定理证明器中实现哥德尔-勒布可证性逻辑（GL）模态完备性的形式化证明，介绍实现细节与非标准证明结构选择，并分析该形式化系统推理的优缺点。
2021-02-11 cs.LO math.LO
