Algebraic analysis of temporal and topological finite variable fragments, using cylindric modal algebras
我们研究我们称之为拓扑柱形代数和紧张柱形代数定义的每一个序数$α$。前者是以$α$为索引的$\sf S4$模态展开的维数为$α$的柱形代数。可表示拓扑代数的语义是由定义在其基上的拓扑的内部运算导出的。时态柱形代数是由模态$F$（未来）和$P$（过去）代数谓词时态逻辑扩展的柱形代数。我们证明了有限维$n>2$的紧张和拓扑柱形代数的无限多个变种包含和包括各种各样的维数$n$的可表示代数不是原子标准的。我们表明，任何类包含类的完全表示代数有一个弱整洁嵌入性质是不是小学。从这两个结果中，我们得出了谓词拓扑和时态逻辑的有限变量片段的省略类型相同的结论。我们表明，通常版本的省略类型定理限制到这样的片段时，变量的数量是$>2$显着失败，即使我们大大拓宽了类模型允许省略一个单一的非主要类型的可数原子理论，即非主要类型consting的co原子。
2014-02-02 math.LO
On the multi dimensional modal logic of substitutions
本文证明了状态不是抽象实体而是具有内部结构的多维模态逻辑的完备性、内插性、可判定性和一个省略型定理。状态将是序列。我们的方法是代数寻址（品种产生）复杂代数的Kripke语义，这样的逻辑。元素为状态集的代数是圆柱代数和多进代数的公共约简
2013-02-13 math.LO
Atom-canonicity, relativized representations and omitting types for clique guarded semantics and guarded logics
研究了适当地包含可表示代数簇的几类圆柱代数的原子正则性。这些代数具有相对化的表示，从而得到了许多关于有限变量片断和/或一阶逻辑的修正的省略型定理，既有否定的，也有肯定的.当我们保持通常的句法和相对化模型（使它们只在局部见证量词的可交换性）时，得到的是否定的结果;当我们在句法中弱化“量词的可交换性”并对语义进行不同的相对化时，得到的是肯定的结果。这样的代数也有弱的整齐嵌入性质，在这个意义上，它们嵌入到可能有限的高维代数的整齐约简中。在本文的第二部分中，最初为原子结构制定的各种可表示性概念以一种明显的方式提升到代数水平，如弱可表示性和强可表示性。这类代数（是原子的）完全通过整齐嵌入来刻画。最后，几个模型理论的问题，这样的类组成的代数具有弱整洁嵌入性能和相对化的表示，如可判定性的方程或普遍的理论，其有限axiomatizability，如果一阶可定义的，提出和回答。
2013-08-27 math.LO
On algorithmic expressivity of finite-variable fragments of intuitionistic modal logics
本文证明了直觉主义模态逻辑FS和MIPC可多项式时间嵌入其正单变量片段，揭示了其算法表达力。
2023-06-27 math.LO
Complexity of the variable-free fragments of non-normal modal logics (extended version)
本文研究了非正规模态逻辑的无变元片段的复杂性，证明了包含经典命题逻辑且包含于弱Grzegorczyk逻辑的模态逻辑的可满足性问题是NP难的，并指出E、EM、EN和EMN的无变元片段是coNP完全的。
2025-07-12 math.LO
On completions, neat embeddings and omittings types, yet again
本文利用代数逻辑的方法论和深层代数结果证明了一阶逻辑有限变片断的三个新的省略型定理。作为一个例子，我们证明了T是L_n理论，且|T| = λ，λ是正则基数，如果T允许消去量词，则T省略< 2^λ的许多非孤立的{ \it极大}型.这基本上是Shelah局限于L_n的结果。这是不能完全代表的。我们还证明了，使用柱代数的彩虹结构，省略类型定理失败L_n，即使我们考虑集团保护语义。这是通过构造一个原子\A \in \PEA_n与可数许多原子（这是有色图）谁Sc（品特）约简是不是在S_c \Nr_n \Sc_{n+3}，但$A$是初等等价于可数完全表示（polyadic平等）代数。强可表示性和完全可表示性的概念之间的各种联系是在整齐的嵌入。给出了彩虹结构和Monk-like代数的几个例子，证明了我们的结果是最好的。作为一个例子，我们证明了，假设存在一定的有限关系代数，对任意k个\in ω，存在\A \in { \sf RPEA}_n \cap \Nr_n \PEA_{n+k}使得Rd_{\sf Sc} \Cm \At \A \notin S \Nr_n \Sc_{n+k+1} .这意味着对任何有限n \geq 3，对任何k \geq 0，存在一个L_n理论和一个类型Γ，使得Gamma在每个n+k+1相对化光滑模型中实现，但不能被使用n+k个变量的见证者隔离.
2013-07-02 math.LO
Kripke trick and decidability of monadic fragments of modal and superintuitionistic logics
本文研究 Kripke 技巧在模拟二元谓词时的修改与失效条件，并据此给出若干模态和超直觉主义一阶逻辑一元片段的算法上界结果。
2023-07-06 math.LO
Expressive power of basic modal intuitionistic logic as a fragment of classical FOL
本文讨论了模态直觉主义逻辑的Kripke式语义的四种不同版本所导出的一阶逻辑片断。为了捕捉这些片段，asimulation的概念进行了修改和扩展，以产生Van Benthem类型的语义表征各自的表达能力。它示出，进一步，这种特征可以很容易地进行到任意一阶可定义的子类的经典一阶模型。
2015-11-06 math.LO
Space and time via Topological and Tense cylindric algebras
设$α$为任意序数，$2<n<ω$。在被《数学学报》接受出版的\cite{3}中，我们简要地研究了用$α$多变量进行拓扑逻辑的代数逻辑、插值、合并和$α$多变量$\sf TopL_α$。这是一个续集\cite{3} ;第二部分模态柱形代数，在那里我们研究代数其他属性的$\sf TopL_α$。模态柱形代数是无限维的柱形代数，用一元模态扩展，从单峰逻辑$\sf L$（如$\sf K5$或$\sf S4$）继承其语义。使用代数逻辑的方法，我们研究符号$\sf TCA_α$中的拓扑（当$\sf L=S4$时）。研究了$\sf TopL_ω$和$\sf TenL_ω$的完备性和省略型$\sf OTT$ s，证明了局部有限的这类代数的几个表示性结果.此外，我们研究了原子规范性的概念，为${\sf TCA}_{n}$和${\sf TenL}_n$，一个众所周知的持久性属性模态逻辑，在$\sf OTT$的${\sf TopL}_n$和${\sf TeLCA}_n$，分别。研究了拓扑柱形代数的可表示性、省略类型、插值和复杂性问题（如不可判定性）.在本文的续集中，我们介绍了时间cylindric代数，并指出如何合并代数的空间（拓扑代数）和代数的时间（时间代数）形成拓扑-时间柱形代数，使自己包含时空gemetries，在一个纯粹的代数方式。
2020-05-18 math.LO
A Godel Modal Logic
在本文中，我们考虑一种方法，命题和可达关系是无限多值的哥德尔代数。特别地，我们分别考虑了哥德尔模态逻辑的$\Box $ -片段和$\Diamond $ -片段，并证明了这两种逻辑对于值在线性Hetying代数[0，1]中的模型类都是完备的.此外，我们证明了第一个片段是唯一确定的一类模型具有清晰的可达性关系，但它没有有限的模型属性。相反，第二个片段的特点是不清晰的可达性模型，但它有有限的模型属性。最后，我们表明，该方法可以扩展到包括许多合理的真值la Pavelka。
2009-03-16 math.LO
Modal Fragments
University of Amsterdam（阿姆斯特丹大学）；ILLC, University of Amsterdam（阿姆斯特丹大学信息、逻辑与计算综合研究所）；Umeå Universitet（于默奥大学）；Leibniz Universität Hannover（汉诺威莱布尼茨大学）
本文探讨了命题逻辑和模态逻辑基限制片段的系统方法，分析了表达能力和复杂性依赖关系，并提出了简单模态片段的参数化方法及可判定性结果。
2026-03-05 cs.LO math.LO
One-variable fragments of first-order logics
本文为一阶逻辑单变量片段提出了一种基于超融合性质和泛函表示定理的公理化充分准则，并提供了针对次结构逻辑的证明论策略。
2023-10-24 math.LO
Complexity of finite-variable fragments of propositional modal logics of symmetric frames
虽然命题模态逻辑S5的有限变量片段--相对于自反、对称和传递框架是完备的--是多项式时间可判定的，但对自反和传递框架逻辑的有限变量公式的限制产生了仍然“难以处理”的片段。“对称条件在这方面的作用还没有被研究过。我们表明，对称性本身或结合自反性产生的逻辑，就像逻辑的自反和传递框架，即他们的有限变量片段仍然难以处理，即PSPACE硬。这就提出了这样一个问题：有限变量片段易于处理的模态逻辑和其他模态逻辑之间的边界究竟在哪里。
2019-10-05 cs.LO math.LO
Moving up and down in the generic multiverse
我们简要介绍了一般多重宇宙的模态逻辑，它是一个双模态逻辑，其运算符对应于关系“是的力迫扩张”和“是的基模型”。第一个关系的片段被称为强制的模态逻辑，我们在早期的工作中研究过。第二个关系的片段被称为根据的模态逻辑，这里将首次研究。此外，我们还讨论了这两个片段的模态逻辑的组合是可能的。
2012-08-24 math.LO
A proof system for the positive fragment of GL
Kyushu Sangyo University（九州产业大学）
本文提出一个基于Dunn给出的sequent系统K_+^{\top\bot}的证明系统GL_+^{\top\bot}，用于处理GL正片段中的模态公式，这些公式不含否定和蕴含符号，主要由逻辑连接词\lor, \land, \Diamond, \Box, \bot, \top和命题变量构成。GL是最小的正则模态逻辑，包含K和洛布公式\Box(\Box p\supset p)\supset\Box p。本文证明了该系统能够将sequent的可证性等价于GL中公式可证性。
2026-05-19 math.LO
On provability logics with linearly ordered modalities
我们引入了逻辑GLP（Λ），它是贾帕里泽的多模态可证明性逻辑GLP（ω）的推广，其中Λ是表示强度递增的可证明性算子层次的任何线性有序集。我们将提供这些逻辑到GLP（ω）的一个约化，除其他外，给出GLP（Λ）的无变量片段的规范形定理的有限性证明和GLP（Λ）对于递归序Λ的可判定性。进一步，我们给出了GLP（Λ）的无变量片段的限制公理化.
2012-10-17 math.LO
Algebraisable versions of predicate topological logic
动机是这样的问题：哪些空间结构可以通过模态逻辑来表征，什么是空间逻辑，如何在模态逻辑中编码不同的几何关系，拓扑逻辑基于拓扑空间而不是Kripke框架提供了用于研究$\sf S4$模态的拓扑语义的汇合的框架。继Sgro的研究和Georgescu的代数研究之后，我们证明了谓词拓扑逻辑和Chang的模态逻辑的各种扩展的一个内插定理和一个省略类型定理。我们的证明是柱形代数分别使用内部算子和盒子的代数寻址展开。然后，我们像抽象代数逻辑一样，研究这两种逻辑的可代数扩展;获得有关其代数对应物的各个子类（这些子类是变种）的合并性质的大量结果。讨论了有限维拓扑柱形代数的原子正则性和完备表示等概念。我们的代数结果的逻辑后果仔细制定了张的谓词模态逻辑和有限版本的无限扩展，通过限制$n$变量，$n$有限的，被视为一个命题多维模态逻辑，和$n$产品的双峰，其框架的形式是$(U, U\times U, R)$其中$R$是一个前序，赋予对角常数。
2014-01-06 math.LO
Computational complexity of one-variable fragments of products with T
我们证明，包含自反框架T逻辑作为因子的命题模态逻辑的积可以嵌入到它们的单变量片段中。证明是一个简化版本的证明，出现，一个类似的结果，产品和扩大相对化产品包含作为一个因素的逻辑KTB的自反和对称克里普克框架。
2021-12-07 math.LO
Characterization and definability in modal first-order fragments
模型论的结果，如特征和可定义性，提供了关于不同逻辑的重要信息。众所周知，这些结果的几个模态逻辑的证明，不知何故，相同的“味道”。对于一阶以下的大多数模态逻辑的一般证明仍然过于雄心勃勃。在这篇论文中，我们计划隔离充分条件的特征和定义定理，以保持在广泛的逻辑。随着这些条件，我们将证明，无论哪个逻辑满足它们，满足这两个定理。因此，人们可以用已知的结果给出逻辑的统一证明。此外，人们将能够证明尚未研究的逻辑的特征和可定义性结果。在这两种情况下，只需要检查逻辑是否满足自动导出所需结果的要求。
2010-11-22 cs.LO math.LO
Towards a Proof Theory of Gödel Modal Logics
针对基本模态模糊逻辑的盒形和菱形片段引入了分析证明演算，该演算将模态逻辑K的Kripke语义与哥德尔逻辑的多值语义相结合.演算用于建立这些片段的完整性和复杂性结果。
2011-05-14 cs.LO math.LO
Bundled fragments of first-order modal logic: (un)decidability
Institute of Mathematical Sciences, Homi Bhabha National Institute（数学科学研究所，霍米·巴巴国家研究所）；Peking University（北京大学）
量化模态逻辑为模态态度的推理提供了一种自然的逻辑语言，即使在保留量化的丰富性的同时，也可以引用域上的谓词。但是，在许多模型类上，逻辑的大多数片段都是不可判定的。多年来，只有少数片段（例如单声部）被证明是可判定的。在本文中，我们研究的片段，捆绑量词和模态在一起，知识/为什么/什么的认知逻辑的早期工作的启发。与量化模态逻辑一样，域是否在世界上保持相同会产生重大差异。特别是，我们表明，束$\forall \Box$是不可判定的恒定域的解释，即使只有一元谓词，而$\exists \Box$束是可判定的。另一方面，在增加域解释，我们得到的可判定性与$\forall \Box$和$\exists \Box$束与不受限制的谓词。在这些情况下，我们还获得了在\PSPACE中运行的基于tableau的过程。我们进一步表明，$\exists \Box$束不能区分恒定域和增加域的解释。
2018-03-28 cs.AI cs.LO math.LO
A universal Kripke frame for the variable-free fragment of RC$^\nabla$
本文刻画了具有保守性算子RC $^\nabla$的反射演算的无变量片段的泛Kripke框架。这里的框架是从Ignatiev RC $^\nabla$ -代数上的所有滤子的集合中得到的，该代数是RC $^\nabla$的无变量片段的Lindenbaum-Tarski代数的同构表示。我们给出了一个建设性的“coordinatewise”表征的过滤器和框架关系的代数模态。
2018-04-08 math.LO
Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions
Free University of Bozen-Bolzano（博尔扎诺自由大学）；King's College London（伦敦国王学院）；Birkbeck, University of London（伦敦大学伯贝克学院）；University of Liverpool（利物浦大学）
本文系统研究一阶模态逻辑中非刚性常项、限定摹状词和计数特征对可判定性的影响，证明若干一元片段可判定并给出紧致复杂度界，同时指出一种扩展逻辑的Ackermann困难性。
2026-11-02 cs.LO math.LO
Models of transfinite provability logic
对于任何序数Λ，我们可以定义一个多模态逻辑GLP（Λ），对于每个Λ <Λ，都有一个模态[Λ]。这些表示强度增加的可证明性谓词。虽然GLP（Λ）没有Kripke模型，但Ignatiev证明，确实可以用自然数模态构建无变量片段的Kripke模型。后来，Icard为同一片段定义了一个拓扑模型，这与Ignatiev的非常密切相关。在本文中，我们展示了如何推广这些结构任意Λ。更一般地，对于每个Θ，Λ，我们建立了Kripke模型I（Θ，Λ）和拓扑模型T（Θ，Λ），并表明GLP（Λ）的闭合片段对于这两种结构都是合理的，并且是完整的，只要Θ足够大。
2012-04-21 math.LO
Modal meet-implication logic
本文扩展命题直觉主义逻辑的 meet-implication 片段，引入保持 meet 的模态，基于半格给出语义并建立对偶性，获得完备性，识别共同模态片段，并证明其为 dialgebraic 逻辑，进而获得某处可表达性。
2022-07-13 cs.LO 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
Algebraic semantics for one-variable lattice-valued logics
任何一阶逻辑的单变量片段都可以被认为是模态逻辑，其中全称量词和存在量词分别被盒模态和菱形模态所取代。在一些情况下，这些逻辑的代数语义的公理化已经得到：最值得注意的是，分别为一阶经典逻辑和直觉主义逻辑的单变量片段的模态对应物S5和MIPC。然而，在一阶中间逻辑的设置之外，缺乏一种通用的方法。本文提供了这样一种方法的基础上设置的一阶格值逻辑，其中公式解释的代数结构与格约简。特别是，公理化得到的模态对应的一个广泛的家庭这些逻辑的一个变量片段通过推广的功能表示定理Bezhanishvili和哈丁一元Heyting代数。一个替代的证明理论的证明也提供了一个变量片段的一阶子结构逻辑，有一个切自由的插值演算，并承认一定的有界插值性质。
2022-09-18 cs.LO math.LO
Towards a Denotational Semantics for Proofs in Constructive Modal Logic
本文给出了构造模态逻辑CK和CD中证明的两种新语义。第一个语义是通过扩展命题直觉逻辑的组合证明的语法给出的，其中证明被分解为线性片段（竞技场网）和并行的弱化收缩片段（斜纤维化）。特别是，我们提供了一个编码的模态公式通过有向图（模态竞技场），和一个编码的线性证明作为模态竞技场配备满足拓扑标准的顶点分区。第二个语义是通过赢得无辜的策略，两个球员的游戏模式舞台。这是通过在Hyland-Ong竞技场中扩展直觉组合证明和获胜无辜策略之间的Heijltjes-Hughes-Straßburger对应关系给出的。使用我们的第一个结果，我们提供了一个表征的获胜策略的游戏模式舞台上对应的模态证明。
2021-04-19 cs.LO math.LO
Axiomatization of crisp Godel modal logic
本文研究了由具有清晰可达性的Kripke模型产生的同时具有Box和Diamond的模态逻辑，其命题取值于标准Godel代数[0，1]G上.本文从正模态逻辑出发，利用Dunn公理，对[3]中的公理系统进行了扩充，得到了一个关于可达性的公理系统，并证明了它在语义上是强完备的.对最常见的框架限制也给出了公理化。我们还证明了在所研究的逻辑中不可能得到Box作为Diamond的缩写，反之亦然，这表明我们所提出的公理系统实际上与文献中任意一个被公理化的单峰片段都不一致。
2020-04-30 math.LO
Non-finitely axiomatisable modal product logics with infinite canonical axiomatisations
我们关心的是模态和代数逻辑的公理化问题，对应于各种片段的两个变量的一阶逻辑计数量词。特别是，我们认为模态产品与Diff，命题单峰逻辑的差异运营商。我们证明了二维乘积逻辑Diff x Diff是不可公理化的，但可以被无穷多个Sahlqvist公理公理化.我们还表明，它的“平方”版本（模态对应的替代和平等免费片段的两个变量的一阶逻辑计数为2）是非非线性axiomatisable在Diff x Diff，但可以通过添加无穷多个Sahlqvist公理公理。这些是第一个例子的产品的axiomatisable模态逻辑是不是axiomatisable，但axiomatisable由明确的无限套规范公理。
2020-01-28 cs.LO math.LO
Correspondence Theory for Modal Fairtlough-Mendler Semantics of Intuitionistic Modal Logic
我们在模态Fairtlough-Mendler语义学（模态FM语义学）\cite{FaMe97}中研究直觉模态逻辑的对应理论，它是可能性语义学\cite{Ho16}的直觉模态版本。我们识别了该语言中的归纳公式片段\cite{GorankoV06}，并在此语义环境下给出了算法$\mathsf{ALBA}$ \cite{CoPa12}.论文有两大特点：一个是在扩展模态语言中，被解释为完美布尔代数中的原子、完美分配格中的完全并素元和完美格中的完全并不可约元的名义变量在本设置中被解释为单例的精化正则开闭包，与经典的正规模态逻辑\cite{Zh21d}的可能性语义相似;另一个特点是我们不使用同形或菱形，这大大限制了归纳公式的碎片。我们证明了健全的$\mathsf{ALBA}$相对于模态FM帧，并表明$\mathsf{ALBA}$成功的归纳公式，类似于现有的设置，如\cite{CoPa12,Zh21d,Zh22a}。
2022-10-05 cs.LO math.LO
The Monadic Grzegorczyk Logic
New Mexico State University（新墨西哥州立大学）
通过强化描述性MGrz-框架中最大点的概念并改进选择性过滤方法，证明了MGrz的有限模型性质，从而确立了MGrz公理化谓词Grzegorczyk逻辑QGrz的单变量片段。
2026-06-23 math.LO
Reflection calculus and conservativity spectra
严格正逻辑由于其有效性和充分表达性的结合，最近在描述逻辑和可证明性逻辑界引起了人们的注意。反射演算RC的语言由公式之间的含义组成，这些公式是由命题变元和常数“真”组成的，只使用合取和菱形模态，这些模态在皮亚诺算术中被解释为受限的一致反射原理。我们扩展的语言RC的另一系列的模态代表运营商与一个给定的算术理论T的片段公理化的所有定理T的算术复杂性$Π^0_n$，对于所有n>0。我们注意到，这样的操作符，在精确的意义上，不能表示在模态逻辑的完整语言。我们制定了一个正式的系统RC $^\nabla$扩展RC是健全的，我们猜想，在这种解释下完成。我们表明，在这个系统中，一个是能够表示迭代的反射原则的任何顺序$<ε_0$。另一方面，我们提供了它的无变量片段的规范形式。因此，无变量片段被证明是可判定的和完整的w.r.t.它的自然算术语义。而RC的无变量公式的规范形式以一种独特的方式对应于$ε_0$以下的序数，RC $^\nabla$的规范形式更一般。事实证明，它们以规范的方式与每个复杂性水平$Π^0_{n+1}$的（有界）算术理论的证明论序数集合相关。最后，基于Ignatiev的Kripke框架，给出了RC $^\nabla$的无变量片段的代数万有模型.我们的主要定理陈述了这个代数的几个自然表示的同构。
2018-05-11 math.LO
Realizability Semantics for Quantified Modal Logic: Generalizing Flagg's 1985 Construction
基于Kleene的可实现性概念，给出了量化模态逻辑的语义.这种语义概括了Flagg在1985年构建的Church论文和一阶算术的模态版本的模型。虽然大部分的文件是致力于发展的语义细节，以说明这种方法的范围，我们表明，建设产生（i）一个模型的模态版本的教会的论文和一个变种的模态集合论由于古德曼和Scedrov，（ii）一个模型的模态版本的Troelstra的广义连续性原则连同一个片段的二阶算术，以及（iii）基于Scott的图模型（用于无类型lambda演算）的模型，该模型见证了非同一性的稳定性的失败。
2016-03-01 math.LO
Characterizing Relative Frame Definability in Team Semantics via the Universal Modality
设ML（U^+）表示用普适模态扩展的模态逻辑的片段，其中普适模态只肯定地出现。我们在著名的Goldblatt-Schlason定理的精神下刻画了ML（U^+）相对于有限传递框架的相对可定义性。我们证明了一类Kripke框架在ML（U^+）中相对于有限传递框架是可定义的当且仅当F在取生成子帧和有界形态像下是闭的。此外，我们还研究了团队逻辑中的模态可定义性。我们研究（扩展）模态依赖逻辑，（扩展）模态包含逻辑和模态团队逻辑。关于全局模型的可定义性，我们得到一个二分法和相对于框架的可定义性。作为一个推论，我们得到了上面所列的每一个逻辑的相对戈德布拉特-卡森式定理.
2018-02-22 math.LO
Intuitionistic and Constructive Modal Logics for Classical Modal Logicians
本文面向经典模态逻辑研究者，综述直觉主义框架下的两类命题模态逻辑，研究介于两者间的新逻辑$\textbf{KI}$并证其完备性，还指出$\textbf{CK}$语义缺陷并证明$\textbf{CK}$、$\textbf{WK}$的Lyndon插值定理。
2026-10-12 math.LO
Modal Translation of Substructural Logics
在1992年的一篇文章中，Kosta Došen发起了一个子结构逻辑中的模态翻译项目，旨在将著名的Gödel-McKinsey-Tarski直觉主义逻辑推广到{ \bf S4}。Došen的翻译对于{ \bf BCI}（的变体）和更强的系统（{ \bf BCW}、{ \bf BCK}）都很有效，但对于{ \bf BCI}以下的系统就不行了。丢弃结构规则会导致逻辑系统没有分布。在这篇文章中，我们表明，通过翻译，每一个子结构（实际上，每一个非分配）逻辑是一个片段的相应排序，剩余（多）模态逻辑。在概念和哲学层面上，翻译提供了一个经典的解释的意义的逻辑运算符的各种非分配命题演算。从技术上讲，它允许毫不费力地转移结果，如紧致性，Löwenheim-Skolem性质和可判定性。
2018-12-17 math.LO
Tableaux for multi-modal hybrid logic with binders, transitive relations and relation hierarchies
在以前的文件中，已经提出了一个表演算，它构成了一个决策过程的混合逻辑与逆向和全球的模态和限制使用的粘合剂。这项工作扩展了这样的演算多模态逻辑与传递关系和关系包含断言。单独添加传递关系或关系层次到所考虑的可判定片段的多模态混合逻辑可以很容易地保持可判定的，通过诉诸已经在文献中证明的结果。然而，这样的结果并不直接允许得出结论，包括这两个功能的逻辑是否仍然是可判定的。所考虑的逻辑的终止，声音和完整的演算的存在证明，除了传递关系和关系层次，这样一个表达的可判定的片段的混合逻辑产生可判定的逻辑。
2013-12-10 cs.LO math.LO
Algebras and relational frames for Gödel modal logic and some of its extensions
哥德尔模态逻辑可以看作是直觉模态逻辑在预线性公理下的扩展。在本文中，我们专注于哥德尔模态逻辑的代数和关系语义，利用有限哥德尔代数和有限森林之间的对偶，即有限偏序集的主下集是全序的。我们考虑具有两个模态算子的哥德尔代数的基本簇的不同子簇（简称GAO）及其相应的森林框架类，它们具有一个或两个可达关系.这些关系结构可以被认为是直觉模态逻辑的通常关系语义的预线性版本。更确切地说，我们考虑有限哥德尔代数的两个主要扩展：一个是通过添加Dunn公理获得的，通常在正经典（和直觉主义）逻辑的片段中研究，另一个是通过添加Fischer Servi公理确定的。我们目前的Jónsson-Tarski像表示定理的不同类型的有限GAO考虑的文件。
2021-12-06 math.LO
The Complexity of the Constructive Master Modality
本文提出了两种构造性主模态逻辑，并证明其复杂性为 EXPTIME，同时解决了相关逻辑的有效性问题
2026-07-22 cs.LO math.LO
$\aleph_1$ and the modal $μ$-calculus
本文研究模态 μ-演算公式的 κ-连续性，定义片段 C_ℵ₁(x)，证明其所有公式 ℵ₁-连续，并给出判定准则，进而刻画闭包序数，证明 ω₁ 是闭包序数且闭包序数对加法封闭。
2019-10-03 cs.LO math.LO
Non-distributive positive logic as a fragment of first-order logic over semilattices
我们把非分配正逻辑看作是一个单排序的一阶语言的片段，它被一个新的模拟概念所保存，称为满足模拟。相遇模拟与模拟的区别在于它们将一个模型的状态对与另一个模型的单个状态联系起来。在这个结果的途中，我们使用一个更传统的模拟概念，并证明了它的Hennessy-Milner风格的定理，使用类似的模态饱和称为满足紧凑性。
2023-02-06 cs.LO math.LO
An algebraic study of S5-modal Gödel logic
本文继续研究一元Gödel代数簇$\mathbb{MG}$.这些代数是哥德尔逻辑的S5-模态展开的等价代数语义，它等价于一阶哥德尔逻辑的单变量单子片段。给出了$\mathbb{MG}$的三个局部有限子簇族，并给出了它们的方程基.我们还引入了一元Gödel代数的拓扑对偶，作为这个表示定理的应用，我们刻画了同余，并借助于它们的对偶空间给出了上述局部有限子簇的刻画.最后，我们研究了由一元Gödel链生成的子簇的一些性质：给出了该簇的特征链，证明了Glivenko型定理对这些代数成立，刻画了$n$生成元上的自由代数.
2020-06-17 math.LO
Graded modal logic and counting bisimulation
本文将互模拟不变片段的刻画定理推广到分级多模态逻辑，证明其在所有及有限点态 Kripke 结构上恰好对应计数互模拟等价下保持的一阶性质。
2023-07-18 cs.LO math.LO
Intrinsic and relative characterization results for logics with negative modalities
Mathematical Institute, University of Bern（伯尔尼大学数学研究所）；Universidade Federal de Santa Catarina（圣卡塔琳娜联邦大学）
本文研究了具有非经典否定的模态逻辑的内在和相对特征化结果，通过模拟和充分性定理分析了其表达能力。
2026-08-17 cs.LO 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
One-dimensional fragment of first-order logic
本文提出了一种新的一阶逻辑的可判定片段。片段是一维的，在这个意义上，量化是有限的存在（通用）量词块的应用程序，使最多一个变量保持自由的量化公式。片段在布尔运算下是封闭的，但额外的限制（称为一致性条件）适用于具有两个或更多变量的原子公式的组合。我们认为，一维性和一致性的概念一起提供了一个新的视角的鲁棒判定的模态逻辑。我们还建立了轻微的修改的限制的语法的一维片段导致不可判定的形式主义。也就是说，二维和非均匀的一维碎片被证明是不可判定的。最后，我们证明了在表达性方面，一维片段与守护否定片段和带计数的二元逻辑是不可比拟的。我们证明的一维片段的可判定性是基于一种技术，涉及直接减少到一元类的一阶逻辑。新技术本身是一个独立的数学兴趣。
2014-04-15 cs.LO math.LO
Modelling of logical systems by means of their fragments
Московский физико-технический институт (национальный исследовательский университет)（莫斯科物理技术学院（国立研究型大学)）
本文通过研究逻辑系统的片段归约，揭示了非经典逻辑的算法复杂性，并提供了新的复杂性界限和克里普克不完全性结果。
2025-12-29 cs.LO math.LO
Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic
University of Bern（伯尔尼大学）；Universidade Federal de Santa Catarina（圣卡塔琳娜联邦大学）
定义直觉主义模态逻辑IK的关系语义上的IK-双模拟，证明IK是直觉主义一阶逻辑的IK-双模拟不变片段，并给出内在刻画及Hennessy-Milner型定理，发展直觉主义一阶模型论。
2026-07-01 cs.LO math.LO
A Characterization Theorem for a Modal Description Logic
模态描述逻辑的特点是模态，它捕获知识对诸如时间、地点或代理的信息状态等参数的依赖性。例如，在一个示例中，逻辑S5-ALC将标准描述逻辑ALC与可以被理解为认知算子或表示（无向）变化的S5模态相结合。该逻辑嵌入到相应的模态一阶逻辑S5-FOL中。我们证明了一个模态特征定理的嵌入，在类比的结果由范Bentham和罗森有关ALC标准的一阶逻辑：我们表明，S5-ALC只有局部角色是，无论是在有限的和无限制的模型，正是互模拟不变片段的S5-FOL，从而给出了一个精确的描述的表达能力的S5-ALC只有局部角色。
2017-05-23 cs.LO math.LO
Existential and positive games: a comonadic and axiomatic view
本文将共单子方法从一阶逻辑扩展到存在性与正性片段，用路径嵌入刻画存在性片段保持性，并引入正互模拟刻画正性片段，从而给出多模态逻辑等资源 Lyndon 正性定理的新证明。
2025-05-06 cs.LO math.LO
Intuitionistic Non-Normal Modal Logics: A general framework
我们定义了一类直觉非正规模态逻辑，它们可以被看作是经典模态逻辑的直觉对应物。我们首先考虑单峰逻辑，它只包含必然性和可能性之间的一个。然后，我们考虑更重要的情况下，双峰逻辑，其中包含两个模态算子。在这种情况下，我们定义了几个必要性和可能性之间的相互作用，尽管比对偶性弱。对于所有的逻辑，我们提供了一个希尔伯特公理化和一个切自由的代数演算，在此基础上，我们还证明了它们的可判定性。然后，我们给我们的逻辑在邻域模型的语义特征。我们的语义框架捕获模块化不仅我们的系统，但也已经知道的直觉非正常模态逻辑，如建设性K（CK）和Wijesekera的建设性并发动态逻辑的命题片段。
2019-01-28 cs.LO math.LO
The modal logic of Reverse Mathematics
反求数学中各子系统之间的蕴涵关系有一个内在逻辑，可以利用这个内在逻辑从已有的反求数学结果中常规地推导出新的反求数学结果。我们使用模态逻辑技术将逆向数学的逻辑形式化为一个系统，我们称之为s-逻辑。我们认为，S-逻辑捕捉正是“逻辑”的内容，在反向数学的子系统之间的蕴涵和非蕴涵关系。我们提出了一个健全的，完整的，可判定的，紧凑的表格式演绎系统的s-逻辑，并详细探讨了两个片段，特别是相关的逆向数学实践和自动定理证明的逆向数学结果。
2014-01-03 cs.LO math.LO
The Modal Logic of Stepwise Removal
我们调查模态逻辑的逐步删除的对象，既为它的内在利益作为一个逻辑的量化没有替换，并作为一个试点研究，以更好地了解动态认知逻辑的模型转换和逻辑的自由选择的图形变化，得到登记在不断增长的内存之间的复杂性跳跃。在介绍了这种逻辑（$\textsf{MLSR}$）及其相应的移除模态之后，我们分析了它的表达能力，并证明了一个互模拟特征定理。然后，我们提供了一个完整的希尔伯特式公理化的逻辑逐步删除的混合语言丰富的名词和公告运营商。接下来，我们证明了$\textsf{MLSR}$的模型检测是PSPACE完备的，而它的可满足性问题是不可判定的。最后，我们考虑一个精细结构的问题：通过将逐步移除模态添加到一阶逻辑片段中获得的表达能力。
2021-03-08 cs.LO math.LO
