Craig interpolation theorem fails in bi-intuitionistic predicate logic
本文通过改编Mints等人的反例，证明双直觉谓词逻辑缺乏Craig插值性质，并澄清该结果与Rauszer的“演绎插值”定理不矛盾。
2022-06-07 math.LO
An interpolant in predicate Gödel logic
一个逻辑满足插值性质，只要一个公式Δ是另一个公式Γ的推论，那么这由一个公式Θ证明，该公式θ只涉及Γ和Δ共有的语言。也就是说，出现在Θ中的关系（和函数）符号出现在Γ和Δ中，Γ具有Θ作为结果，并且Θ具有Δ作为结果。经典谓词逻辑和直觉谓词逻辑都具有插值性质，但中间谓词逻辑如何具有插值性质是一个长期悬而未决的问题，2013年Mints，Olkhovikov和Urquhart证明了常数域直觉主义逻辑不具有插值性质，而谓词哥德尔逻辑是否具有插值性质则是一个悬而未决的问题。在这篇短文中，我们证明了他们关于常域直觉主义逻辑的反例在谓词哥德尔逻辑中确实允许内插。虽然这对解决谓词哥德尔逻辑的问题没有影响，但它使人们相信它确实满足插值。此外，我们的方法是基于Olkhovikov的语义工具的分析，我们希望这可能最终有助于解决这个问题。
2019-02-12 math.LO
Intuitionistic Existential Instantiation and Epsilon Symbol
本文给出了一个具有存在\实例化规则的直觉谓词逻辑的自然演绎系统，它使用了Hilbert的$\e$ -符号.它相对于直觉谓词逻辑是保守的。我们提供了一个合适的Kripke语义的完整性证明，勾勒出一个正规化证明的方法，调查相关的工作和状态一些开放的问题。我们的系统扩展了直觉系统，由于A. Dragalin和Sh.前原
2012-08-03 cs.LO math.LO
Generalizations of Mezhirov's game semantics to predicate superintuitionistic logics and the Casari formula
本文将Mezhirov提出的命题直觉主义逻辑博弈语义推广至谓词直觉主义逻辑及其扩展，并建立博弈与无限公式集推导之间的联系。
2023-10-24 math.LO
On certain constructive predicate calculus
构造性算术或马尔可夫算术MA是从直觉算术HA通过添加以下两个原则获得的：马尔可夫原则M，它区分了构造主义和直觉主义，以及所谓的扩展丘奇命题ECT，它区分了构造性语义学和经典语义学。第一个原则是由一个谓词公式表示，但ECT是作为一个计划制定的算术语言。作者以前的一些结果使得用一个纯谓词公式代替ECT方案成为可能。这给出了一个谓词演算MQC，它可以作为构造性算术的逻辑基础。即以MQC和佩亚诺公理为基础的算术理论证明了MA中可推导的所有公式。注意，MQC不是直觉主义和经典逻辑之间的中间演算：它证明了一些在经典谓词演算中不可推导的公式。参考书目：12项。
2022-09-22 math.LO
Categorical and Algebraic Aspects of the Intuitionistic Modal Logic $\operatorname{IEL}^{-}$ and its predicate extensions
直觉模态逻辑系统${\bf IEL}^{-}$是S. Artemov和T. Protopescu作为信念逻辑\cite{Artemov}的直觉主义版本。我们构造的模态lambda演算是Curry-Howard同构的${\bf IEL}^{-}$作为应用计算的类型理论表示广泛的功能性编程。我们还提供了一个范畴的解释，这模态lambda演算考虑coalgebras与一个monoidal函子上的一个carbohydrate闭范畴。最后，我们研究了Heyting代数和具有相应算子的locale。这种运算符也用于无点拓扑中。我们使用Goldblatt \cite{goldblatt2011cover}引入的Dedekind-MacNeille完备化和模态覆盖系统研究${\bf IEL}^{-}$及其相关逻辑的谓词扩展的完全Kripke-Joyal风格语义。本文扩展了发表在LFCS'20卷\cite{rogozin2020modal}的会议论文。
2020-12-07 math.CT math.LO
Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter
本文证明了一阶直觉逻辑的正片段在具有两个变量和一个一元谓词字母的语言中是不可判定的，没有常数和等式。无论我们考虑的是扩展域还是常量域的语义，这都是正确的。然后，我们将这一结果推广到区间[QBL，QKC]和[QBL，QFL]，其中QKC是弱排中律的逻辑和QBL和QFL是一阶对应的维塞尔的基本和形式逻辑，分别。我们还表明，对于大多数“自然”的一阶模态逻辑，两个变量片段与一个单一的一元谓词字母，没有常数和平等，是不可判定的，无论我们是否考虑语义与扩展或常数域。这些包括QKTB、QGL和QGrz的所有子逻辑，其中包括QK、QT、QKB、QD、QK4和QS4。
2022-06-12 cs.LO math.LO
Recursive inseparability of classical theories of a binary predicate and non-classical logics of a unary predicate
本文通过骨牌问题提取递归不可分性，间接证明了有界语言中经典与非经典一阶逻辑各种片段的不可判定性，涵盖二元谓词经典逻辑、模态及超直觉主义谓词逻辑的单调片段。
2025-05-01 math.LO
A joint logic of problems and propositions
Steklov Mathematical Institute of Russian Academy of Sciences（俄罗斯科学院斯捷克洛夫数学研究所）
本文提出QHC逻辑系统，结合问题与命题的两种解释方法，扩展了直觉逻辑和经典逻辑。
2025-12-02 math.LO
Continuation-passing Style Models Complete for Intuitionistic Logic
一类模型，在连续单子的形式多态的一阶个人，这是健全的和完整的最小直觉谓词逻辑。证明的健全性和完整性是建设性的，其组成的计算内容，特别是一个$β$ -规范化的评估程序简单类型的lambda演算和类型。虽然灵感来自Danvy的类型导向部分求值器，但避免了分隔控制运算符（即计算效果）的必要使用。多态性的作用是至关重要的--去掉它可以让我们获得经典谓词逻辑的模型完备的概念。我们的模型和克里普克模型之间的联系是通过加强双重否定转移图式来实现的。
2011-03-03 cs.LO cs.PL math.LO
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
本文提出首个针对递增域一阶双直觉逻辑的可靠且完备的多树相继式演算证明系统，通过显式本征变量上下文避免域坍缩并揭示驻留原则与存在谓词的依赖关系。
2024-11-19 cs.LO math.LO
Delimited control operators prove Double-negation Shift
我们提出了一个扩展的最小的直觉谓词逻辑，基于分隔的控制运算符，可以得到的谓词逻辑版本的双否定移位模式，同时保持析取和存在属性。
2011-03-11 cs.LO math.LO
Following all the rules: Intuitionistic completeness for generalised proof-theoretic validity
普拉维茨指出，证明理论上有效的逻辑是直觉主义逻辑。最近的工作证明理论的有效性已经推翻了这一点。事实上，它已经表明，证明理论的有效性甚至不是封闭的替代。在本文中，我们对Prawitz（1973）中发现并由Schroeder-Heister（2006）完善的证明理论有效性的定义进行了微小的修改。我们将把这个新概念称为广义证明理论有效性，并证明广义证明理论有效性的逻辑是直觉主义逻辑。
2022-11-22 math.LO
Model-theoretic characterization of intuitionistic propositional formulas
k-asimitation和asimitation的概念被引入作为k-互模拟和互模拟的非对称对应物。证明了一个一阶公式等价于一个直觉命题公式的标准平移当且仅当它对于某个k是关于k-模拟不变的，然后证明了一个一阶公式等价于一个直觉命题公式的标准平移当且仅当它对于模拟不变.最后，证明了一阶公式与直觉命题公式的标准翻译是直觉等价的，当且仅当它对于直觉模型之间的模拟是不变的.
2012-07-18 math.LO
A completeness theorem in proof-theoretic semantics via set-theoretic semantics
本文以原子二阶直觉主义命题逻辑为系统，借助 Okada 与 Takemura 的带证明项相语义构造闭项论域模型，从而证明直觉主义逻辑相对于 Prawitz 证明论有效性的完备性。
2025-05-16 math.LO
Heyting Algebra and Gödel Algebra vs. various Topological Systems and Esakia Space: a Category Theoretic Study
本文介绍了直觉拓扑系统及其性质。Heyting代数，Gödel代数，Esakia空间和直觉拓扑系统之间的范畴关系也得到了详细的研究。
2020-05-03 math.LO
Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation
本文首先证明了直觉主义逻辑中几种经典逻辑公式（非数据第三定律、反证法、皮尔斯定律）之间的等价性。然后，它建立了正确的哥德尔-柯尔莫哥洛夫翻译，其限制的命题的情况下，是由于格利文科。这种转换将一阶逻辑的公式$F$映射为公式$F^{\lnot\lnot}$，使得$F$在经典逻辑中可证明当且仅当$F^{\lnot\lnot}$在直觉主义逻辑中可证明。所有的形式证明都是在自然演绎中提出的。这些问题是众所周知的证明理论事实，但在教科书中，它们往往被忽略或留给读者。由于组合困难的一些必要的正式证明，我们希望这份报告可能是有用的，特别是学生和同事从其他领域。
2016-02-25 math.LO
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
本文首次探索子结构逻辑的证明论语义，提出直觉主义乘法线性逻辑（IMLL）的基础扩展语义，其中逻辑常量定义均采用消去规则形式，并证明了其可靠性与完备性。
2024-11-12 cs.LO math.LO
Modal Dependence Logics: Axiomatizations and Model-theoretic Properties
模态依赖逻辑是基于团队语义定义的模态逻辑，具有向下封闭性。在本文中，我们介绍了健全的和完整的演绎系统的主要模态依赖逻辑，特别是那些在其语言中的直觉连接词。我们还建立了一个具体的团队语义和单世界语义之间的联系，并表明，模态依赖逻辑可以解释为直觉模态逻辑的变种。
2017-06-03 math.LO
The Order-Theoretic Structure of Free Heyting Algebras
我们发现了n元直觉命题逻辑的Lindenbaum代数的序论刻画。
2007-03-28 math.LO
From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
本文针对直觉主义命题逻辑，论证其基扩展语义涵盖了一种基于消去规则的证明论有效性版本的陈述内容，既阐释了基扩展语义的运作原理，也证明了该版本证明论有效性的完备性。
2024-09-12 cs.LO math.LO
Base-extension Semantics for Intuitionistic Modal Logics
本文为Simpson直觉主义模态逻辑建立基扩展语义，并证明其相对自然演绎系统的可靠性与完备性。
2025-07-09 cs.LO math.LO
The proof theory and semantics of second-order (intuitionistic) tense logic
本文提出二阶直觉时逻辑的公理化、证明论和模型论定义，并证明其一致性，同时通过证明搜索论证建立了标签序列演算的完备性。
2026-02-05 cs.LO math.LO
The additive groups of $\mathbb{Z}$ and $\mathbb{Q}$ with predicates for being square-free
我们考虑四个结构$(\mathbb{Z}; \mathrm{Sqf}^\mathbb{Z})$、$(\mathbb{Z}; <, \mathrm{Sqf}^\mathbb{Z})$、$(\mathbb{Q}; \mathrm{Sqf}^\mathbb{Q})$和$(\mathbb{Q}; <, \mathrm{Sqf}^\mathbb{Q})$，其中$\mathbb{Z}$是整数的加法群，$\mathrm{Sqf}^\mathbb{Z}$是$a \in \mathbb{Z}$的集合，使得对于每个素数$v_{p}(a) < 2$和相应的$p$ -进赋值$v_{p}$、$\mathbb{Q}$和$\mathrm{Sqf}^\mathbb{Q}$，$<$同样地被定义为有理数，并且$<$表示这些域中的每个域上的自然序。我们证明了第二种结构是模型理论上的野生，而其他三种结构是模型理论上驯服。此外，所有这些结果都可以被看作是数论随机性产生模型理论结果的例子。
2021-03-14 math.LO
On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
本文研究了命题直觉主义逻辑、一阶非常数论域直觉主义逻辑和一阶常数论域直觉主义逻辑的标号演算和套演算之间的关系。它示出，拟合的嵌套结石自然产生于其相应的标记结石-为上述每一个逻辑-通过消除标记派生的结构规则。这两种类型的系统之间的平移对应关系被用来表明嵌套演算从其相关的标记演算中继承了证明理论属性，例如规则的完整性，可逆性和切割容许性。由于标记的演算很容易通过逻辑的语义，本文提出的方法可以被看作是一个，从而细化版本的标记演算（包含嵌套的演算片段）具有良好的性能直接从逻辑的语义。
2021-04-19 cs.LO math.LO
A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
本文比较可归约性语义与基语义（含Sandqvist变体）三种单调证明论语义，建立二者间的转换条件，并据此讨论直觉主义逻辑的基完备性问题。
2025-11-08 cs.LO math.LO
A Topos-Theoretic Semantics of Intuitionistic Modal Logic with an Application to the Logic of Branching Spacetime
本文在任意 elementary topos 内部构造 Alexandrov 拓扑语义以发展直觉主义命题模态逻辑，通过内部算子对 S4 和 S5 的 B 公理进行建模，并将其应用于分支时空逻辑，结合认识论不可区分性解释及 Barcan formula 证伪了形而上学现实论。
2024-10-16 math.CT math.LO
Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic
证明理论语义学（Proof-theoretical Semantics，P-tS）是一种语义学范式，其中逻辑中的意义基于证明（而不是真理）。直觉命题逻辑（IPL）的P-tS的一个特殊实例是它的基扩展语义（B-eS）。这种语义由一个称为支持的关系给出，解释逻辑常数的含义，它由称为基础的规则系统参数化，提供原子命题的语义。在本文中，我们解释的基础上收集的明确的公式，并使用统一的证明搜索-逻辑编程（LP）的证明理论的基础-提供后者的操作视图-建立完整的IPL的B-eS。这种观点允许否定，P-tS中的一个微妙的问题，被理解为在LP中的否定失败协议。具体地说，虽然对命题的否定在传统上被理解为对命题否定的断言，但在B-eS中，我们可以将对命题的否定理解为未能找到对命题的证明，这样，断言和否定都是P-tS中的基本概念。
2023-03-28 cs.LO math.LO
Model Theory for Real-valued Structures
我们考虑一般的结构，公式的真假值在实单位区间连续模型论，但其谓词和功能不需要一致连续的距离谓词。每个一般结构都可以通过增加一个距离谓词扩展为一个预度量结构，该距离谓词是公式的一致极限。此外，该距离谓词在一致等价之前是唯一的。我们利用这一点将度量结构的模型论中的中心概念扩展到一般结构，并表明有关度量结构的文献中的许多模型论结果与一般结构具有自然的相似之处。
2020-10-26 math.LO
Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism
本文在范畴论的框架内，通过对基于Curry-Howard同构的一阶直觉主义逻辑的计算解释，提出了一种新的可靠而完备的语义.此外，一个健全的和完整的语义相应的Alzoda-calculus的派生，太。这种语义学在某种程度上扩展了由Heyting范畴、拓扑理论解释和Kripke模型给出的更传统的意义。证明引入这种新颖语义的特征是它是“无点”的事实，即，没有一个宇宙的元素被用来解释逻辑术语。换句话说，术语并不表示某些集合的个体，而是表示将语句的解释保持在一起的“胶水”，类似于形式拓扑中发生的情况。由于所提出的语义学可以平凡地扩展到所有基于直觉主义系统的一阶逻辑理论（并且，稍微注意一下，也可以扩展到最小系统），所以语义学也涵盖了所有的谓词理论，即使这些理论的一些特殊方面应该被注意到。
2013-06-29 cs.LO math.LO
An ecumenical view of proof-theoretic semantics
本文将逻辑普世主义与证明论语义学相结合，构建了一个经典逻辑与直觉主义逻辑及其证明概念能够共存的统一框架，为解决两者的哲学争议提供了新视角。
2025-04-03 cs.LO math.LO
On generalized Van-Benthem-type characterizations
本文继续了作者以前所取得的直觉主义逻辑的模型论刻画，进一步推广了它们。这导致在一个模型理论表征的表达能力的任意有限集的保护连接度不超过1和定期连接度2的语言有界格。
2016-02-16 math.LO
A Brief History of Future Set Theory
数学家们在生成集合时仍然使用朴素集合论，而不会产生任何矛盾。因此，他们的工作方法可以被认为是一个具有100多年经验的一致推理系统。我的猜想是，这种方法工作得很好，因为数学家只使用那些谓词来形成集合，这些集合产生封闭的遗传一致谓词扩展。对于他们在构造某个（特殊）集合（自底向上）的过程中使用的每个开放公式，我们总是可以找到一个“几乎封闭”的公式（即只有自由变元“x”的无参数公式），它产生与之前在自底向上过程中构造的相同的作为谓词扩展的某个（特殊）集合。因此，在理解方案中使用带有自由参数的谓词不会引起任何困难，并且可以通过元数学考虑来“提升”。关键词：朴素集合论，奎因，新基础，NF，泛集合，理解模式，谓词扩展，集合论哲学，策梅洛，弗伦克尔，ZF，补集。CT是类理论框架：逻辑+“=”+丘奇图式+外延公理。
2008-07-27 math.LO
The Borel Complexity of Isomorphism for Complete Theories of Linear Orders With Unary Predicates
证明了如果A是线性序，则Th（A）是$\aleph_0$ -范畴的或Borel完全的（在Friedman和Stanley的意义下）.我们对此进行概括;如果A有可数个一元谓词，则Th（A）是$\aleph_0$ -范畴的，有可数个模型（至少三个），是Borel等价于实数上的相等，是Borel等价于“实数的可数集”，或者是Borel完全的。此外，这些情况中的每一个都以自然的方式对应于所有大小的模型的计数，直到来回等价。所有这些情况下都是可能的，我们计算精确的模型理论条件表明，这种情况下发生。这补充了O-极小理论的工作，其中类似的结果被证明。大部分的机器下的证明是基于工作的Matatyahu鲁宾在“理论的线性秩序”，其中表明，这样的理论满足沃特的猜想，不能有精确的$\aleph_0$可数模型。
2016-03-30 math.LO
Proof-Theoretic Soundness and Completeness
我们给出了一个演算推理的一阶片段的经典逻辑，这是足够的直觉Kripke框架的真值条件，并概述了证明理论的合理性和完整性证明，我们相信这是有利于自动化。
2022-04-27 cs.LO math.LO
A translation of Maehara's "Eine Darstellung der Intuitionistischen Logik in der Klassischen"
本文翻译了Maehara 1954年关于直觉主义逻辑嵌入经典模态逻辑的论文，该工作独立于Gödel，使用证明论方法扩展了嵌入到一阶直觉主义模态逻辑。
2026-09-24 cs.LO math.LO
On abstract F-systems. A graph-theoretic model for paradoxes involving a falsity predicate and its application to argumentation frameworks
Universidad Nacional del Sur（南大国立大学）
F-系统是一种有向图，它能够对断言其他句子的虚假性的句子进行建模。像Liar和Yablo这样的Parases可以用这个工具来分析，以找到图论模式。在本文中，我们提出了F-系统模型抽象的所有功能的语言中表示的句子。所有这一切都是假设存在的句子和二元关系'.证实了...的虚假性”其中。非指称句的可能存在也被认为是。为了对所有可以共同被认为是真的句子的集合进行建模，我们引入了聚合的概念，它的存在保证了悖论的存在。聚合也能够表征指称矛盾，即由于与模型中其他句子的相互作用，在经典估值下只能是假的句子。一个克里普克的风格固定点表征的复杂性提供和不动点是完整的（意味着每个句子被认为是真或假）和一致的（意味着没有句子被认为是真和假）放在对应的企业集团。此外，论证框架是F-系统的特殊情况。我们展示了当地企业集团和容许的参数集之间的关系，并认为论证理论的概念的有用性。
2020-05-14 cs.AI math.LO
Proof-theoretic Semantics for First-order Logic
本文为一阶经典逻辑的证明论语义提供了一种初等、构造性且原生的完备性证明，并同时给出一阶直觉主义逻辑的可靠性与完备性证明。
2025-07-17 cs.LO math.LO
A Proof-Theoretic Approach to the Semantics of Classical Linear Logic
University College London（伦敦大学学院）
本文提出通过基础扩展语义（BeS）和基础支持的概念，从证明论角度研究经典线性逻辑的乘法-加法片段（MALL）语义学。
2026-02-27 cs.LO math.LO
Model Theory of Monadic Predicate Logic with the Infinity Quantifier
本文建立了模型理论性质的$\mathrm{FOE}^{\infty}$，一元一阶逻辑的变化，具有广义量词$\exists^\infty$（“有无限多”）。我们提供了语法定义的片段$\mathrm{FOE}^{\infty}$表征四个不同的语义属性的$\mathrm{FOE}^{\infty}$ -句子：（1）是单调的和（2）（斯科特）连续在一个给定的一元谓词集;（3）有真理下保持采取子模型或（4）不变量下采取继承。在每一种情况下，我们产生一个有效定义的映射，将任意句子$φ$翻译成属于相应句法片段的句子$φ^{p}$，其属性是$φ$等同于$φ^{p}$，当它具有相关的语义属性时。我们的方法是首先提供这些结果在更简单的设置一元一阶逻辑（$\mathrm{FOE}$）和（$\mathrm{FO}$）的平等，然后移动到$\mathrm{FOE}^{\infty}$包括广义量词$\exists^\infty$到图片。作为我们的推论，我们得到了上述四个语义性质对于$\mathrm{FOE}^{\infty}$ -语句是可判定的。此外，我们的结果是直接相关的自动机和表达模bisimilirity的一元二阶逻辑的变种的特征。该应用程序是在一个配套文件中开发的。
2018-09-10 cs.LO math.LO
