Temporal interpretation of intuitionistic quantifiers
我们表明，直觉量词承认以下的时间解释：$\forall x A$是真的，在一个世界$w$当且仅当$A$是真的，在每个对象的域中的每个未来的世界，和$\exists x A$是真的，在$w$当且仅当$A$是真的，在一些对象的域中的一些过去的世界。为此目的，我们工作的谓词版本的著名的时态命题逻辑$\sf S4.t$。谓词逻辑$\sf Q^\circ S4.t$是通过沿着Corsi将$\sf QK$弱化为$\sf Q^\circ K$的路线弱化$\sf S4.t$的标准谓词扩展$\sf QS4.t$的公理来获得的。哥德尔翻译将谓词直觉主义逻辑$\sf IQC$完全忠实地嵌入到$\sf QS4$中。我们提供了一个时间版本的哥德尔翻译，并证明它嵌入$\sf IQC$到$\sf Q^\circ S4.t$充分和忠实的，也就是说，我们表明，一个句子是可证明的$\sf IQC$当且仅当其翻译是可证明的$\sf Q^\circ S4.t$。忠实性证明使用语法的方法，而我们证明丰满利用广义Kripke语义的Corsi。
2020-09-01 math.LO
Negational Fragment of Intuitionistic Control Logic
研究直觉控制逻辑一元纯否定片段的性质。该逻辑是在直觉命题逻辑（IPL）的基础上，通过增加新的伪和常数扩展IPL语言而产生的。有两个不同的假常数可以定义两种形式的否定。我们分析了负一元公式之间的蕴涵关系，并给出了ICL这一片断的非等价公式的偏序集。
2014-08-09 cs.LO math.LO
Quantum monadic algebras
引入了量子一元和量子柱形代数。这些都是适应量子设置的一元代数的哈尔莫斯，和柱形代数的亨金，蒙克和塔斯基，这是用于代数治疗的经典和直觉谓词逻辑。量子环境中的主要例子来自冯诺依曼代数和子因子。在这里，我们开发这些量子一元和柱形代数的基本性质，并将它们与量子谓词逻辑。
2022-03-28 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
Monadic Second Order Logic with Measure and Category Quantifiers
本文研究了在无限词和树上，将一元二阶逻辑扩展为带有基于贝尔范畴和勒贝格测度的广义“几乎全部”量词，探讨其表达能力和性质。
2018-04-09 cs.FL 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
Failure of the Blok-Esakia Theorem in the monadic setting
研究证明Blok-Esakia同构无法扩展到仅含一个固定变量的一元谓词逻辑片段，即其不再是一元直觉逻辑扩张格与一元Grzegorczyk逻辑扩张格的同构，揭示该定理在一元谓词逻辑环境中失效。
2024-12-08 math.LO
MSO logic of the real order with the set quantifiers ranging over the Borel sets
Logique Consult（逻辑咨询）
本文证明了在实数序的MSO逻辑中，允许集量化符范围于Borel集时，该理论是可判定的，并探讨了其在S2S中的可解释性。
2026-01-20 math.LO
Generalized Realizability and Intuitionistic Logic
设V是一组数论函数。我们定义了谓词公式的V -可实现性概念，使得V中函数的下标用于解释蕴涵和全称量词。本文证明了直觉谓词演算关于V -可实现的语义是合理的当且仅当V的某些自然条件成立。
2022-05-17 math.LO
Decidability of quantified propositional intuitionistic logic and S4 on trees
量化命题直觉主义逻辑是由命题直觉主义逻辑通过在命题上添加量词\forall p，\exists p而得到的.在Kripke语义学的上下文中，一个命题是一个向上封闭的模型结构中世界的子集。Kremer（1997）证明了基于所有偏序类的量化命题直觉主义逻辑Hπ+与完全二阶逻辑递归同构。他提出了一个问题，即从限制到树的逻辑是否是可公理化的。事实证明，它是可判定的。所使用的方法也可以用来建立模态S4的可判定性与类似类型的Kripke结构的命题量化。
2002-03-18 math.LO
Quantifier Reasoning and Multiple Generality in Aristotle and Ancient Logic
Centro de Filosofia da Universidade de Lisboa（里斯本大学哲学中心）
本文探讨亚里士多德及古代逻辑理论在处理多重普遍性问题上的能力，挑战传统对单称谓逻辑的不足认知。
2026-01-13 math.LO
The Pseudofinite Monadic Second Order Theory of Linear Order
一元二阶逻辑是一阶逻辑在一元关系上的量词的扩展。本文利用一阶设置研究了有限线性序的共享一元二阶理论，即线性序的伪有限一元二阶理论。我们给出了明确的（和递归的）公理和剩余序列的完成。一个连接profinite代数，特别是与自由profinite幺半群上的一个发电机，建立通过扩展斯通对偶。
2021-05-25 cs.FL cs.LO math.LO
Algebraic results on universal quantifiers in monoidal t-norm based logic
本文通过一个等式描述的一元运算$\forall$扩充了MTL-代数的语言，从而抽象出了全称量词“for any”的原义代数性质。由此得到的代数类称为\emph{MTL-algebras with universal quantifiers}（简称UMTL-代数）。在讨论了UMTL-代数的一些基本代数性质之后，我们开始系统地研究UMTL-代数的主要子类，其中一些子类构成了著名的代数：UMV-代数和一元布尔代数。然后给出了可表示的、单的、半单的UMTL-代数的一些刻画，并得到了UMTL-代数的一些表示。最后，我们建立了基于模态monoidal t-范数的逻辑，并证明了它关于UMTL-代数簇的完备性，从而得到了基于模态monoidal t-范数的逻辑是半线性的一个充要条件.
2019-10-09 math.LO
Short monadic second order sentences about sparse random graphs
本文研究了Erdens-Rényi随机图模型$G(n,p)$在$p = n^{-α}$为$α>0$时的零-一律.对于一个给定的关于图的逻辑语句类$\mathcal{K}$和一个给定的函数$p=p(n)$，我们说$G(n,p)$服从0 - 1定律（w.r.t.类$\mathcal{K}$），如果每个句子$φ\in\mathcal{K}$或者a.a.s.真的还是尽快对于$G(n,p)$为false。本文考虑有界\textit{quantifier depth} $k$的一阶性质和一元二阶性质，即表示该性质的公式中的最长量词嵌套链的长度.量词深度$k$的特性的0 - 1定律我们称之为\textit{zero-one $k$-laws}。本文的主要结果是关于一元二阶性质（MSO性质）的0 - 1 $k$ -律。我们确定所有的值$α>0$，其中0 - 1 $3$ -法律MSO属性不成立。我们还表明，在相反的情况下的$3$ -法律，有无穷多个值的$α$的零-1 $4$ -法律MSO属性不成立。为此，我们分析了$G(n,p)$，可能是独立的利益的某些属性的演变。
2018-10-17 cs.DM math.CO math.LO
Intuitionistic Implication in Elementary Team Logics
University of Gothenburg（哥德堡大学）；University of Helsinki（赫尔辛基大学）
本文研究初等团队逻辑FOT的两种修改：其无包含原子片段的量词消去，以及添加直觉主义蕴涵后表达能力提升至全二阶逻辑，导致有效性等价。
2026-09-15 math.LO
A categorical equivalence for monadic algebras of first-order substructural logics motivated by Kalman's construction
School of Science, Xi’an Shiyou University（西安石油大学理学院）；School of Science, Xi Hang University（西安航天大学理学院）；CONICET and Departamento de Matematica, Facultad de Ciencias Exactas, Universidad Nacional del Centro de la Provincia de Buenos Aires（阿根廷布宜诺斯艾利斯省中部国立大学精确科学学院数学系与阿根廷国家科学研究委员会）
本文通过卡曼构造，研究单子余分配格的范畴等价性，并扩展了相关领域的研究成果。
2026-01-29 math.LO
Calibrating the negative interpretation
一个基于直觉主义逻辑的经典可靠理论S的最小经典扩张S $^{+g}$，通过将其数学公理的根森否定解释加到S上来定义，包含S的经典版本S +（--A -> A）的忠实翻译S $^g$。S $^g$可称为S的经典内容。一阶和二阶直觉算术包含了它们的经典内容，但直觉递归分析不能证明其无量词可数选择公理的否定解释。黑田的双重否定移位原理（包括等价于直觉谓词逻辑的弱完备性的哥德尔-戴森-克赖塞尔公理）和双重否定的特征函数原理的变体，为克莱因的直觉分析I的经典可靠子系统的最小经典扩张提供了简洁的刻画。两类基本构造性递归数学包含着它的经典内容。Bishop的构造性分析与Kleene的I的中性子系统B具有相同的经典内容。根据Vafeiadou的一个结果，相容的、经典上不可靠的理论（如I）的最小经典扩张本质上依赖于它们的经典相容子理论的Ω模型。
2021-09-11 math.LO
Mathematical semantics of intuitionistic logic
这项工作是一个数学家试图理解直觉主义逻辑。它可以从两个方面来阅读：作为一篇研究论文，穿插着对标准材料的反思的冗长离题;或者作为对一阶直觉主义逻辑的基本（但非常非传统）介绍。对于后一个目的，不需要在形式逻辑的培训，但在数学，如拓扑空间和偏序集适度识字，是假设。这项工作的主要主题是寻找一个正式的语义足以Kolmogorov的非正式解释的直觉主义逻辑（其最简单的部分是或多或少相同的所谓BHK解释）。这种搜索超越了通常的模型论，基于塔斯基的语义后果的概念，并超越了通常的形式主义的一阶逻辑，基于图式。因此，我们研究形式语义的简化版本的保尔森的元逻辑，在伊莎贝尔证明。通过构造性地解释元逻辑连接词和量词，我们得到了一个广义的模型论，它特别涵盖了直觉主义逻辑的可实现型解释。另一方面，通过分析Kolmogorov的语义后果概念（它是Tarski标准概念的替代），我们得到了替代的模型论。通过对元逻辑的扩展，我们进一步得到了一个广义的替代模型论，它足以形式化Kolmogorov的语义。另一方面，我们也制定了修改Kolmogorov的解释，这是兼容的通常，塔斯基风格的模型论。也就是说，它可以通过层值模型形式化，这是Palmgren的范畴模型的一个特例;直觉主义逻辑在这个语义上是完备的。
2017-05-01 math.LO
Alternating Set Quantifiers in Modal Logic
我们建立了严格的几个设置量词交替层次结构的模态逻辑的基础上，评估各类有限图。这延伸到模态设置Matz，Schweikardt和Thomas（2002）的著名结果，该结果指出一元二阶逻辑的类似层次是严格的。因此，本文解决了van Bentham（1983）提出的一个问题，ten Cate（2006）重新提出了这个问题，Kuusisto（2008，2015）对此做了部分回答。
2016-02-29 cs.FL cs.LO math.LO
First-order logic in the Medvedev lattice
柯尔莫哥洛夫引入了一种非正式的演算问题，试图为直觉主义逻辑提供一种经典的语义。这后来被梅德韦杰夫和穆奇尼克正式定义为梅德韦杰夫和穆奇尼克晶格。然而，他们只是形式化的命题逻辑，而哥洛夫还讨论了全称量词。我们扩展梅德韦杰夫的工作，一阶逻辑使用的概念，一阶hyperdoctrine从范畴逻辑的结构，我们将呼吁梅德韦杰夫hyperdoctrine。我们还研究了中间的逻辑，梅德韦杰夫hyperdoctrine给我们，在那里我们特别关注的子区间的梅德韦杰夫hyperdoctrine，试图获得一个类似的Skvortsova的结果，有一个因素的梅德韦杰夫格特征直观命题逻辑。最后，我们考虑海廷算术在梅德韦杰夫hyperdoctrine和证明类似的Tennenbaum定理的可计算模型的算术。
2015-07-13 math.LO
Uniform interpolation with constructive diamond
University of Amsterdam（阿姆斯特丹大学）；University of Birmingham（伯明翰大学）；University of Melbourne（墨尔本大学）
本文通过构造性方法证明构造性K（CK）和Wijesekera的K（WK）具有均匀插值性质，填补了直觉主义模态逻辑中独立box和diamond算子均匀插值研究的空白。
2026-05-27 cs.LO math.LO
Ecumenical modal logic
本文扩展Prawitz的普世系统思想至真势K模态，统一经典与直觉主义逻辑连接词，并建立相应的证明论性质。
2020-05-28 cs.LO math.LO
Multidimensional tilings and MSO logic
本文用MSO公式定义无限离散平面上的着色集合，研究判定其是否定义子移位的复杂性，并给出各量词交替类语言的精确分类或上下界。
2025-05-23 cs.FL math.DS math.LO
Skolemization In Intermediate Logics
本文刻画了允许标准及Andrews Skolem化的中间一阶逻辑，并为其他逻辑开发新型Skolem函数，同时证明带量词移位公理的谓词直觉主义逻辑的Kripke框架不完全性，以促进非经典逻辑的消解式定理证明。
2025-01-26 cs.LO math.LO
The square of opposition in orthomodular logic
在亚里士多德逻辑中，直言命题分为普遍肯定命题、普遍否定命题、特殊肯定命题和特殊否定命题。两个上述类型的命题之间的可能关系被编码在对立方中。正方形表达了一元一阶量化的基本性质，在代数方法中，可以考虑一元布尔代数来表示。更确切地说，量词被认为是作用于布尔代数的模态算子，而对立方则由代数结构所用语言的某些项之间的关系来表示。这种表示有时被称为对立的模态方。一元一阶逻辑的几种推广可以通过改变底层布尔结构而得到，另一种布尔结构引起了对平方的新的可能解释。
2014-04-23 math.LO quant-ph
Fundamental Logic Through the Lens of Modality
University of California, Berkeley（加州大学伯克利分校）；Chapman University（查普曼大学）
本文利用模态逻辑，通过Gödel-McKinsey-Tarski和Goldblatt翻译，证明了基础逻辑与正交逻辑、直觉主义逻辑之间的完全忠实嵌入关系。
2026-07-24 cs.LO math.LO
From IF to BI: a tale of dependence and separation
我们需要一个新的眼光在逻辑的信息依赖和独立的Hintikka和Sandu和Vaananen，和他们的组成语义由于霍奇斯。我们如何霍奇斯的语义可以被看作是一个特殊的情况下，一般建设，这提供了一个背景下，一个有用的完整性定理，就更广泛的一类模型。我们对逻辑的每个方面都有一些新的认识。我们表明，自然命题逻辑所携带的语义是捆绑的蕴涵由于Pym和O 'Hearn，它结合了直觉和乘法连接词的逻辑。这引入了几个新的连接词以前没有考虑在逻辑的信息依赖，但我们显示发挥了非常自然的作用，最显着的直觉含义。至于量词，我们表明，他们在霍奇斯语义的解释是被迫的，因为他们是下的图像通常的塔斯基语义的一般建设，这意味着他们是伴随着替代，因此唯一确定。至于依赖谓词，我们表明，这是从一个更简单的谓词，恒常性或依赖于没有定义。这就离不开直觉蕴涵的运用。然后将函数相关的Armstrong公理恢复为直觉蕴涵公理的标准集。我们还证明了Hodges风格的完全抽象结果，其中直觉蕴涵起着非常自然的作用。
2011-02-07 cs.LO math.LO
Mechanised uniform interpolation for modal logics K, GL, and iSL
本文在 Coq 中机械化计算并证明了模态逻辑 K、GL 和 iSL 的命题量词可定义性（一致插值），完善了 GL 的现有证明，实现了 iSL 的首次证明论构造，并提供了经过验证的计算程序。
2024-04-29 cs.LO math.LO
Subshifts, MSO Logic, and Collapsing Hierarchies
我们使用一元二阶逻辑来定义二维子移位，或无限平面的着色集。我们提出了一个自然的家庭的量词交替层次结构，并表明，他们都崩溃到第三级。特别是，这解决了[Jeandel & Theysier 2013]的一个开放问题。这一结果与图画语言形成了鲜明的对比，图画语言的层次结构通常是无限的。
2014-06-27 cs.FL cs.LO math.DS
Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
University of Bamberg（班贝格大学）；Freie Universität Berlin（柏林自由大学）
在Isabelle/HOL中为MSO开发三种嵌入，提出两类替换机制实现自动化忠实性，并机械化证明向下Loewenheim-Skolem定理，区分一般与标准解释，通过经典例子展示差异。
2026-09-23 cs.AI cs.LO math.LO
Completeness of infinitary heterogeneous logic
给定正则基数$κ$使得$κ^{<κ}=κ$（例如，如果广义连续统假设成立），我们开发了一个用于经典无穷逻辑的证明系统，该系统包括异构量化（即，量词的无限交替序列），其中存在至多$\mathcal{L}_{κ^+, κ}$的任何公式的合取和析取，并且量化（包括异构的）被应用于小于$κ$的许多变量。这种类型的量化在$\mathcal{S}et$中使用通常的二阶公式来解释游戏策略，并且公理基于游戏语义的确定性公理的更强变体。在这个公理系统中，我们证明了关于一类集值结构的可靠性和完备性定理，我们称之为良定的。虽然这个类比Takeuti的确定性逻辑中的确定性结构类更具限制性，但完备性定理在我们的情况下适用于更广泛的$\mathcal{L}_{κ^+, κ}$公式，并且异质理论的良好确定模型的范畴是可访问的。我们的系统是制定内的分类逻辑，我们不需要强加任何具体的要求，证明树，从而无视Takeuti的系统所需的特征变量条件。我们还调查了直觉系统的异构量词和证明类似的完备性定理，以及确定的结构在一般的类别，在$κ$ -Grothendieck toses特别是，当$κ^{<κ}=κ$，也在克里普克模型。最后，我们考虑了我们的系统中的异构量化与受囿量词是可表达的扩展，并扩展我们的完整性结果的情况下。
2019-01-31 math.CT math.LO
Interleaving Logic and Counting
本文研究自然语言推理中逻辑与计数的结合，通过带计数的单子一阶逻辑及其强化形式，分析可定义性、公理化与可判定性，并联系语言量词和认知科学。
2025-07-07 cs.CL cs.LO math.LO
