On the quantified version of the Belnap-Dunn modal logic and some extensions of it
我们考虑一个量化版本的(命题)模态逻辑$\mathsf{BK}$,提出了较早的S。P. Odintsov和H. Wansing;该版本将用$\mathsf{QBK}$表示。利用规范模型方法,我们证明了$\mathsf{QBK}$关于一个合适的可能世界语义的强完备性。对于某些自然的$\mathsf{QBK}$ -扩张也得到了类似的结果。特别地,证明了用Barcan方案对$\mathsf{QBK}$的扩展对于具有常数域的适当可能世界语义是强完全的。此外,我们定义忠实的嵌入(à la Gödel-McKinsey-Tarski)的量化版本的纳尔逊的建设性逻辑到适当的$\mathsf{QBK}$ -扩展。
2022-01-12 math.LO
Quantified Reflection Calculus with one modality
本文提出了QRC逻辑$_1$,它是量化模态逻辑的严格正片段.对菱形模态的预期解读是形式理论的一致性。谓词符号被解释为参数化公理化。我们证明了算术可靠的逻辑QRC $_1$关于这个算术解释。量化的可证明性逻辑是不可判定的。然而,不可判定性证明不能在我们的签名和算术阅读中进行。我们猜想逻辑QRC $_1$是算术完备的.本文采取的第一步,通过提供关系语义QRC $_1$与相应的完整性证明算术的完整性。我们还展示了有限模型的属性,这意味着可判定性。
2020-03-30 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
Labelled calculi for quantified modal logics with definite descriptions
本文引入了具有确定描述的量化模态逻辑的标号演算。我们证明了这些演算具有G3型演算的良好结构性质。特别地,所有规则都是保高可逆的,弱化和收缩是保高容许的,割是容许的。最后,我们表明,每个演算给出了相应的模型类的有效性的证明理论表征。
2020-02-12 cs.LO math.LO
Incompleteness in Quantified Conditional Logic
该研究指出,Stalnaker和Thomason的条件逻辑在以命题为输入的选择函数语义下是不完整的,且这一结论在多种语义设定下保持不变。
2026-02-03 math.LO
Representation theorems in modal logic using algebraic logic
证明了无穷谓词模态逻辑的几个表示定理
2013-04-03 math.LO
Modal logic with the difference modality of topological $T_0$-spaces
本文的目的是研究$T_0$空间的拓扑模态逻辑,具有差模态(对于$T_n$,其中$n\geq1 $相应的逻辑是已知的)。我们考虑带有两个模态算子$\square$和$[\ne]$的命题模态逻辑。$\square$被解释为内部算子,并且$[\ne]$对应于不等式关系。引入逻辑$S4DT_0$,证明了$S4DT_0$是所有$T_0$空间的逻辑,并具有有限模型性质.
2019-11-30 math.LO
Standard Gödel modal logics are not realized by Gödel justification logics
我们表明,标准哥德尔模态逻辑,最初介绍了由Caicedo和Rodriguez在\cite{CR2009,CR2010},没有实现的基本哥德尔理由逻辑,虽然是由遗忘投影。
2019-07-10 math.LO
Rosser provability and normal modal logics
本文研究了可证逻辑为正规模态逻辑的Rosser可证谓词。首先,我们证明了存在一个Rosser可证明性谓词,其可证明性逻辑恰为正规模态逻辑${\sf KD}$。其次,我们引入了一个新的正规模态逻辑${\sf KDR}$,它是${\sf KD}$的一个适当扩展,并证明了存在一个Rosser可证明性谓词,其可证明性逻辑包含${\sf KDR}$。
2019-05-17 math.LO
The Modal Logic of Provability and Forcing
本文研究可证性与力迫在模态逻辑中的交互,提出双模态逻辑 PF 及 PF^ω,并分别刻画一般情形与集合论 ω-模型中的对应逻辑。
2023-11-01 math.LO
Modal Dependence Logics: Axiomatizations and Model-theoretic Properties
模态依赖逻辑是基于团队语义定义的模态逻辑,具有向下封闭性。在本文中,我们介绍了健全的和完整的演绎系统的主要模态依赖逻辑,特别是那些在其语言中的直觉连接词。我们还建立了一个具体的团队语义和单世界语义之间的联系,并表明,模态依赖逻辑可以解释为直觉模态逻辑的变种。
2017-06-03 math.LO
We belong together? A plea for modesty in modal plural logic
对强模态复数逻辑的动机的怀疑论考察。
2016-12-26 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
Nested Sequents for Quantified Modal Logics
本文针对带不同论域的量化模态逻辑构建嵌套序列演算,证明其具备良好结构性质、与公理系统等价且可靠完备,并说明存在谓词可表达时演算具有内部性。
2023-11-08 cs.LO math.LO
First-Order Modal Logic: Frame Definability and Lindström Theorems
本文将Goldblatt-Lindstrom特征定理推广到一阶模态逻辑。
2016-05-29 math.LO
Frame definability in finitely-valued modal logics
本文研究了有限值模态逻辑中的框架可定义性,并通过适当的变换建立了两个主要结果:(1)在有限值模态逻辑中,人们不能定义比经典模态逻辑中已经可定义的框架类更多的框架类(参见~ \citep [厚度~ 8]{tho}),以及(2)一个大的有限值模态逻辑族定义了与经典模态逻辑完全相同的框架类(包括基于有限Heyting和\MV -代数,甚至\BL -代数的模态逻辑)。这样,人们可以观察到,例如,著名的戈德布拉特--罗森定理立即适用于这些逻辑。特别地,我们用一个简单得多的证明得到了~ \citep{te}的中心结果,并回答了该论文中的一个未解决的问题。此外,建议的翻译,使我们能够确定一个大类的有限值模态逻辑的计算复杂性。
2022-06-26 math.LO
Deciding some displayable modal logics
本文利用显示演算证明了正规模态逻辑K及其若干扩张的可判定性。
2023-12-25 math.LO
Completeness of logics with the transitive closure modality and related logics
给出了具有传递闭包模态的模态逻辑的Kripke完备性的一个充分条件。更确切地说,我们表明,如果一个逻辑承认我们所谓的可定义过滤(ADF),那么这样的扩展的逻辑是完整的,此外,有有限的模型属性,并再次ADF。这个论点可以迭代,作为应用,我们得到的有限模型性质的PDL样扩展的逻辑,ADF。
2020-11-04 math.LO
Modal logic of some products of neighborhood frames
本文考虑邻域框架积的模态逻辑,证明了对于集合$\{S4, D4, D, T\}$中的任意逻辑对$L$和$L'$,$L$ -邻域框架和$L'$ -邻域框架积的模态逻辑是$L$和$L'$的融合.
2014-05-26 math.LO
A Characterization of Non-Iterative Normal Modal Logics
非迭代正规模态逻辑由模态度为1的公理定义。本文利用规范型计算确定了K的所有可能的非迭代正规模态逻辑、单峰命题扩张的集合。为了刻画它们,我们构建了这样的逻辑的完整集合(格),并提供了它们的公理和语义的通用规范。
2021-03-25 math.LO
Compatibility between modal operators in distributive modal logic
本文识别了分配模态逻辑中保证 box 和 diamond 算子源自同一可达关系且不施加额外限制的基本相容性条件,并通过添加局部性公理模块化地获得直觉主义和正模态逻辑。
2023-11-16 math.LO
Some General Completeness Results for Propositionally Quantified Modal Logics
本文研究命题量化模态逻辑的完全性问题,证明含Barcan模式的正规逻辑在可量化一般框架下强完全,给出公式真值在框架过渡中保持的充分条件,并基于有限多样性得到一类Kripke完全的逻辑及欧几里得框架逻辑的有限公理化。
2024-06-23 cs.LO math.LO
Derivational modal logics with the difference modality
在这一章中,我们用导模态和差模态研究了组合语言中拓扑空间的模态逻辑。我们给出公理化和证明以下类的完备性:所有的空间,$T_1$ -空间,稠密的本身空间,一个零维稠密的本身可分度量空间,$R^n$ $(n\ge 2)$。我们还讨论了语言之间的相关性与不同的组合的拓扑,派生,普遍和差异形式的可定义性。
2014-05-26 math.LO
Axiomatizing modal inclusion logic and its variants
本文为模态包含逻辑及其两个表达能力等价的变体(分别含可能算子及其单世界变体)建立了完全公理化,并通过范式定理和自然演绎系统完成完全性证明。
2025-03-11 math.LO
Reflexive insensitive modal logics
我们分析了一类模态逻辑呈现不敏感的自反性的方式修改的模态算子的语义定义。我们探讨在何种程度上可以这些逻辑的特点,并证明了一个一般的完整性定理的基础上,正常的模态逻辑和他们的自反不敏感的同行之间的翻译。最后,我们提供了一个充分的语义条件,描述了当一个类似的一般合理性结果也可用。
2015-07-22 math.LO
Affine modal propositional logic
Tarbiat Modares University(塔比尔·莫达雷斯大学)
研究仿射模态命题逻辑,通过用下半连续包络算子取代内部算子,证明了该逻辑的完备性和仿射紧致性定理。
2026-09-17 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
A note on public announcements in standard Gödel modal logic
我们研究公告运营商的背景下,标准哥德尔模态逻辑介绍了Caicedo和罗德里格斯。在这个基础逻辑上,承认一个自然的语义超过[0,1]-值的模态Kripke模型的推广,我们展示了三种可能的语义解释的公告运营商,所有等价的经典设置,并表明这些逻辑都是不同的表达强度。我们通过希尔伯特式演算为这些逻辑提供部分完备性结果。
2021-12-13 math.LO
Closure Semantics for Weak Modal Logics: Completeness and Representations
本文为弱模态逻辑引入闭包语义,证明其可靠性与强完备性,并给出与邻域、FMT及克里普克语义间的保真翻译。
2026-10-14 math.LO
A model category for modal logic
本文在Kripke模型树展开的预层拓扑斯上定义Quillen模型结构,为模态逻辑建立同伦理论,并重新审视模态保持定理与Hennessy-Milner性质。
2023-10-18 math.LO
Rooted Hypersequent Calculus for Modal Logic S5
本文提出了模态命题逻辑S5的一个有根超代数演算。我们表明,这个演算的所有规则是可逆的,削弱,收缩和削减的规则是容许的。也建立了健全性和完整性。
2019-05-22 math.LO
The Modal Logics of Kripke-Feferman Truth
我们通过Solovay式完备性结果确定了Solomon Feferman的不动点真值模型的模态逻辑及其公理化。给定一个不动点模型$\mathcal{M}$或其公理化$S$,我们找到一个模态逻辑$M$,使得模态语句$φ$是$M$的一个定理当且仅当通过用真值谓词翻译模态算子得到的语句$φ^*$在$\mathcal{M}$中为真,或在所有这样的翻译下都是$S$的一个定理。为此,我们引入了一个新版本的可能世界的语义,具有经典和非经典的世界,并建立了一个家庭的非全等模态逻辑,其内部逻辑是亚经典的这种语义的完整性。
2020-05-06 math.LO
A Logic for Aristotle's Modal Syllogistic
我们提出一种新的模态逻辑,赋予它一个简单的演绎系统来解释亚里士多德的模态三段论理论。虽然受到标准命题模态逻辑的启发,但它也是一种术语逻辑,它允许一种(声音)扩展语义,涉及给定世界中可能的事态。应用于分析亚里士多德的模态三段论发现在\emph{Prior Analytics} A8-22它揭示了各种精细-这种逻辑允许我们与现代命题模态逻辑的公理建立联系,并在多大程度上感知这些公理。都隐含在亚里士多德的推理中进一步的工作将涉及解决这个逻辑(或其变体)的完整性问题,以及逻辑的扩展,包括关系演算(例如,在盖伦的\emph{Introduction to Logic}中处理的关系三段论),Slomkowsky认为这已经在\emph{Topics}中找到了。
2022-06-14 math.LO
Effectively constructible fixed points in Sacchetti's modal logics of provability
本文给出了Sacchetti的模态逻辑${\bf K} + \Box(\Box^n p \to p) \to \Box p$($n \geq 2$)可证性不动点定理的一个纯语法证明.从我们的证明中,得到了构造这些逻辑中不动点的有效方法。我们还证明了特定模态公式的简单不动点的存在性。
2021-09-13 math.LO
Modal Matters in Interpretability Logics
这篇论文是2008年发表的关于可解释性逻辑中模态方法及其应用的三篇相关论文中的第一篇。在这第一个文件奠定了基础,为以后的结果。这些基础包括一个彻底的处理的施工方法,以获得模态模型。这种构造方法被用来重新证明一些已知的结果在该地区的可解释性,如模态完备性的逻辑${\textbf{IL}}$。其次,应用该方法得到了新的结果:逻辑${\textbf{IL}}{\sf M_0}$的模态完备性和${\textbf{IL}}({\sf W^*})$的模态完备性。
2020-04-15 math.LO
Product closure of some second-order modal logics
产品更新是一个操作模型引入到认知逻辑,以代表一个广泛的类的信息事件。如果向一种语言中添加表示产品更新的模态并不改变它的表达能力,那么我们就说这种语言是“因产品更新而关闭的”。“基本模态语言已知将因产品更新而关闭。证明了一元二阶逻辑对于乘积更新是闭的(定理5)。我们的技巧是通过一种中间语言来传递我们称之为“动作名词”的东西。“我们得到的推论是,命题量化的模态逻辑对于产品更新是封闭的,模态μ演算也是如此。
2010-11-23 math.LO
A Study of Subminimal Logics of Negation and their Modal Companions
我们研究由Johansson最小逻辑语言产生的命题逻辑系统,并通过弱化对否定算子的要求而得到。我们提出他们的语义作为一个变体的邻域语义。我们使用对偶性和完备性的结果表明,有不可数多次极小逻辑。我们还给出了最小逻辑的过滤的模型论和代数定义,并证明了它们是对偶的。这些构造保证了命题最小逻辑具有有限模型性质。最后,我们定义并研究了一些相关的次极小系统的具有非正规模态算子的双峰伴随,并给出了这些双峰伴随的无穷公理化。
2020-02-26 math.LO
Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
我们提出了一种允许非良基证明的模态Grzegorczyk逻辑Grz的演算,并通过构造作用于这些证明的连续割消映射,得到了它的割消定理。
2017-04-11 math.LO
Profiniteness, Monadicity and Universal Models in Modal Logic
本文证明投射有限模态代数在集合范畴上具有单子性,并通过分析单子函子重新得到模态逻辑中用于刻画自由模态代数与典范模型子框架的普遍模型构造。
2023-05-08 math.LO
On algorithmic expressivity of finite-variable fragments of intuitionistic modal logics
本文证明了直觉主义模态逻辑FS和MIPC可多项式时间嵌入其正单变量片段,揭示了其算法表达力。
2023-06-27 math.LO
More on modal logics and deduction
Eötvös Loránd University(厄特沃什·罗兰大学);Yozgat Bozok University(约加特博佐克大学)
本文研究了在共轭模态逻辑的代数语义中,可加性与推理定理之间的关系,提出强非可加变种,并证明其在保持局部推理-脱落定理的情况下,可将正常模态逻辑转换为强非可加逻辑,同时显示相关类不是初等的。
2026-03-18 math.LO
Provability Interpretation of Propositional and Modal Logics
1933年,哥德尔引入了命题直觉主义逻辑的可证明性解释,为BHK解释建立了形式化。他使用模态系统$\mathbf{S4}$作为可证明性的直观概念的形式化,然后将$\mathbf{IPC}$翻译为$\mathbf{S4}$。他的工作建议的问题,找到一个具体的可证明性解释的模态逻辑$\mathbf{S4}$。在本文中,我们将试图回答这个问题。事实上,我们将推广Solovay对模态逻辑$\mathbf{GL}$的可证明性解释,以捕获其他模态逻辑,如$\mathbf{K4}$,$\mathbf{KD4}$和$\mathbf{S4}$。然后,我们将使用这些结果来找到一个形式化的BHK解释,我们将表明,与不同的解释的BHK解释,我们可以捕获一些命题逻辑,如直觉主义逻辑,最小逻辑和Visser-Ruitenburg的基本逻辑。此外,我们将表明,没有证明性解释的任何扩展$\mathbf{KD45}$,也没有BHK解释的经典命题逻辑。
2017-08-31 math.LO
Non-Well-Founded Proofs for the Grzegorczyk Modal Logic
我们提出了一个Grzegorczyk模态逻辑Grz允许循环和其他非良基证明,并通过构造一个连续的切割消除映射作用于这些证明,得到它的切割消除定理。作为应用,我们从理论上证明了逻辑Grz的Lyndon插值性质。
2018-04-03 math.LO
Cut--free sequent calculus and natural deduction for the tetravalent modal logic
{ \em四价模态逻辑}($\cal TML$)是Font和Rius(\cite{FR2})定义的两种逻辑之一(另一种是{ \em正常四价模态逻辑} ${\cal TML}^N$),与蒙泰罗的四价模态代数有关。这些逻辑是众所周知的{ \em-邓恩的四值逻辑}的扩展,它结合了多值字符(四价)与模态字符。事实上,$\cal TML$是关于四价模态代数保持真度的逻辑。正如丰特和里乌斯所观察到的,逻辑$\cal TML$和代数之间的联系不如${\cal TML}^N$那么好,但是作为补偿,它具有更好的证明理论行为,因为它具有强充分的根岑演算(参见\cite{FR2})。本文证明了Font和Rius给出的非线性微积分不具有割消性质。然后,利用Avron,Ben-Naim和Konikowska提出的一般方法(\cite{Avron02}),我们给出了具有割消性质的$\cal TML$的一个代数演算.最后,受后者的启发,我们提出了一个{ \em自然演绎}系统,相对于四价模态逻辑是可靠的和完备的。
2021-01-24 math.LO
Automorphisms of the Lattice of Classical Modal Logics
本文分析了最小经典模态逻辑系统E的命题扩张,它们构成一个格CExtE。我们的分析方法使用代数计算与规范形式,这是一个推广的规范形式适用于正常的模态逻辑。作为应用,我们确定了CExtE的一个自同构群,它同构于对称群S4。
2021-03-23 math.LO
Toward the van Benthem Characterization Theorem for Non-Distributive Modal Logic
本文将模拟、互模拟及图像有限模型、模态饱和模型、超滤扩张和超幂扩张等模型论概念推广到非分配模态逻辑的极性语义,并据此证明了Hennessy-Milner定理与van Benthem刻画定理。
2024-04-08 math.LO
Topological product of modal logics with the McKinsey axiom
本文研究带McKinsey公理的S4.1与S4模态逻辑的拓扑积,证明其等价于两逻辑融合加一条额外公理且可判定,给出了介于融合与扩张积之间的拓扑积实例。
2024-03-10 math.LO
Modal completeness of sublogics of the interpretability logic $\mathbf{IL}$
研究了可解释性逻辑$\mathbf{IL}$的几个子逻辑的模态完备性和模态不完备性。引入了子逻辑$\mathbf{IL}^-$,证明了$\mathbf{IL}^-$相对于Visser引入的Veltman预结构是可靠和完备的.此外,我们证明了$\mathbf{IL}^-$和$\mathbf{IL}$之间的12个逻辑关于Veltman预结构的模态完备性。另一方面,我们证明了$\mathbf{IL}$的八个自然子逻辑是模态不完备的。最后,我们证明了这些不完备逻辑是关于广义Veltman预结构完备的。作为这些研究的结果,我们得到本文所研究的20个逻辑都是可判定的。
2020-11-23 math.LO
A dichotomy for some elementarily generated modal logics
本文考虑由$\forall x_0 \exists x_1 \dots \exists x_n \bigwedge x_i R_λx_j$形式的一阶公式定义的初等类的正规模态逻辑。我们证明了这些逻辑的许多性质,如有限axiomatisability,elementarity,axiomatisability由一组典型的公式或由一个单一的广义Sahlqvist公式,连同初始公式的模态可定义性,要么同时举行或同时不举行。
2015-02-27 math.LO
Subordination algebras in modal logic
本文的目的是表明,即使模态(正常)逻辑的自然代数语义是模态代数,更一般的从属代数类(粗略地说,非对称接触代数)是足够的,所以导致完全性结果。这激发了代数(在泛代数的意义上)研究那些从属代数的关系结构。
2020-06-16 math.LO
First-order swap structures semantics for some Logics of Formal Inconsistency
形式不一致逻辑(LFI)是次协调逻辑(即包含矛盾但非平凡理论的逻辑),具有一致性连接符,允许以受控的方式恢复ex falso quodlibet原则。本文的目的是考虑一种新的语义方法,一阶线性模糊集的基础上塔斯基结构定义在交换结构,一类特殊的多代数。拟议的语义框架概括了以前的aproaches量化的LFI在文献中提出的。QmbC的情况下,更简单的量化LFI扩展经典逻辑,将进行详细分析。本文还研究了QmbC的一个公理化扩展QLFI10,它等价于da Costa和D'Ottaviano三值逻辑J3的量化形式.这种逻辑的语义结构是基于扭曲结构的塔肯结构。还考虑了QmbC和QLFI1o使用标准相等谓词的扩展。
2019-12-21 cs.LO math.LO
Modal definability in Euclidean modal logics
本文研究欧几里得模态逻辑框架类中模态可定义性问题的可计算性,刻画了哪些欧几里得模态逻辑会导致该问题不可判定。
2025-08-14 cs.LO math.LO
Undecidability and non-axiomatizability of modal many-valued logics
在这项工作中,我们研究了一类全球模态逻辑所产生的Kripke框架评估某些剩余格,在文献中称为模态多值逻辑的可判定性。我们展示了一个大的家庭,这些模态逻辑是不可判定的,与经典的模态逻辑和命题逻辑定义在同一类代数。这个家族包括了在标准Lukasiewicz代数和乘积代数上计算的Kripke框架所产生的全局模态逻辑。我们改进了前面的结果,证明了全局模态Lukasiewicz和乘积逻辑甚至不能递归可公理化。我们的结论是否定地解决了开放的问题,即每个全局模态逻辑是否与它的局部模态逻辑在无限制必然规则下是封闭的。
2022-04-15 cs.LO math.LO
Intuitionistic modal logics: a minimal setting
本文提出一种严格包含于IK的直觉主义模态逻辑,作为最小正规直觉主义模态逻辑的候选,并探讨其设定。
2025-02-26 cs.LO math.LO