Kripke Models for Classical Logic
Danko Ilik, Gyesik Lee, Hugo Herbelin
我们引入了经典逻辑的Kripke模型的概念，并构造性地证明了它的可靠性和无割完备性。我们讨论的概念和它的潜在应用的新颖性。
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Kripke Semantics for Fuzzy Logics
克里普克框架（和模型）为次经典逻辑提供了合适的语义，例如直觉主义逻辑（布劳威尔和海廷）将自反和传递克里普克框架（具有持久满意关系）公理化，而基本逻辑（维瑟）将传递克里普克框架（具有持久满意关系）公理化。在这里，我们调查Kripke框架/模型是否可以提供一个语义模糊逻辑。对于基本模糊逻辑的每一个公理，寻找满足它们的Kripke框架/模型的充要条件。事实证明，唯一的模糊逻辑（包含基本模糊逻辑的逻辑），这是健全的和完整的关于一类克里普克框架/模型是哥德尔逻辑（或超直觉主义逻辑的达米特）的扩展，事实上，这种逻辑是健全的和强完整的关于自反，传递和连接（线性）克里普克框架（与持久的满意关系）。这为（命题）模糊逻辑中的哥德尔逻辑提供了一个语义特征。
Translating Labels to Hypersequents for Intermediate Logics with Geometric Kripke Semantics
我们给出了一个将几何Kripke框架公理转化为Int^*/Geo中相应的中间逻辑的结构超代数规则的过程，这些中间逻辑允许弱化、收缩，在某些情况下还允许切割。我们给出了一个过程，翻译相应的逻辑标记序列的超序列，共享相同的线性模型（对应于哥德尔-达米特逻辑）。我们证明了标记证明Int^*/Geo可以被转换成hyperereremantic证明，可以使用线性规则，这对应于著名的哥德尔-达米特逻辑的通信规则。
Recursive enumerability and elementary frame definability in predicate modal logic
研究了一阶谓词模态逻辑中递归可枚举性与基本框架可定义性之间的关系。一方面，众所周知，每个一阶谓词模态逻辑关于Kripke框架的基本类完备，即，一类可由经典一阶公式定义的框架是递归可递归的。另一方面，基于本质上具有二阶Kripke语义的“自然”命题模态逻辑的谓词模态逻辑的许多例子是已知的，它们要么不是递归可排数的，要么是Kripke不完全的。这就提出了一个问题，即是否每一个Kripke完备的、递归可判定的谓词模态逻辑都可以用一个Kripke框架的基本类来刻画。我们回答这个问题的否定，通过构建一个正常的谓词模态逻辑，这是Kripke完全的，递归可重复的，但不完全的一个基本类的框架。我们还提出了一个正常的谓词模态逻辑的例子，是递归可重复的，Kripke完全的，不完全的一个基本类的根框架，但相对于一个基本类的框架，没有根是完整的。
From Intuitionism to Many-Valued Logics through Kripke Models
直觉命题逻辑是由Kurt Gödel（1932）证明的无限多值逻辑，它是由Stanismartaw Jaumkowski（1936）证明的可数多值逻辑。在本文中，我们使用Saul Kripke（1959）的模型为这些定理提供了另一种证明。哥德尔的证明产生了一个中间命题逻辑（介于直觉主义和经典之间），现在被称为哥德尔或哥德尔-达米特逻辑，也被模糊逻辑学家研究。我们还提供了一些结果，在此逻辑命题连接词的可定义性。
Logics of Intuitionistic Kripke-Platek Set Theory
研究了直觉Kripke-Platek集合论IKP的逻辑结构，证明了IKP的一阶逻辑是直觉一阶逻辑IQC。
Algorithmic complexity of monadic multimodal predicate logics with equality over finite Kripke frames
本文确定了带等词的一元多模态谓词逻辑在有限Kripke框架上的算法复杂性，并给出了精确的复杂性界。
Degree of Kripke-incompleteness of Tense Logics
本文将模态逻辑中Blok的Kripke不完备程度二分定理推广到时态逻辑格K、LT和NExt(ST)，并证明这些格中迭代分裂恰好对应严格Kripke完备逻辑。
Finite Kripke models and provability interpretations in quantified modal logic
本文研究了有限克里普克模型在量化模态逻辑中的算术完备性，通过Artemov和Japaridze的有限模型嵌入技术，构建了两种不同场景下的可证明性谓词和算术解释。
Binary Kripke Semantics for a Strong Logic for Naive Truth
我表明，逻辑$\textsf{TJK}^{d+}$，目前已知的最强的逻辑之一，以支持天真的真理理论，是从克里普克语义常数域直觉主义逻辑（一）下降的要求，可访问性关系是自反的和（二）只允许自反世界作为反例逻辑后果。此外，我还为$\textsf{TJK}^{d+}$提供了一个简化的自然演绎系统，其中使用条件证明的限制形式来建立条件。
Kripke-like models of Set Theory in Modal Residuated Logic
本文借助Ono–Komori剩余Kripke模型推广Fitting的直觉主义集合论语义，构建模态剩余逻辑中的von Neumann层级，建立与Heyting值模型的公式翻译，并提出可构造集全域概念。
Axiomatizing logics of finite Gödel-Kripke models
研究模态戈德尔逻辑对有限戈德尔-克里普克模型的完备性，发现原有逻辑不满足，并提出新的公理化方法以实现完备性。
Kripke trick and decidability of monadic fragments of modal and superintuitionistic logics
本文研究 Kripke 技巧在模拟二元谓词时的修改与失效条件，并据此给出若干模态和超直觉主义一阶逻辑一元片段的算法上界结果。
An algebraic generalization of Kripke structures
经典命题正规模态逻辑的Kripke语义是通过将Kripke结构嵌入到更大类的点稳定支撑量子中来代数化的。这种代数语义包含了传统的代数语义的基础上格与一元运算符，它提出了自然的解释模态逻辑，可能感兴趣的应用，在结构中出现的几何和分析，如叶状流形和算子代数，通过拓扑群胚和逆半群。我们研究了系统K，T，K4，S4和S5的基于Quantale的语义的完备性，特别是获得了S5的公理化，它不使用否定或模态必要性算子。作为额外的例子，我们描述直觉命题模态逻辑，程序PDL的逻辑，和分歧的时态逻辑CTL。
Some General Completeness Results for Propositionally Quantified Modal Logics
本文研究命题量化模态逻辑的完全性问题，证明含Barcan模式的正规逻辑在可量化一般框架下强完全，给出公式真值在框架过渡中保持的充分条件，并基于有限多样性得到一类Kripke完全的逻辑及欧几里得框架逻辑的有限公理化。
Neighbourhood semantics for graded modal logic
引入了一类将Kripke框架嵌入邻域框架的分次模态逻辑的邻域框架。这类邻域框架是一阶可定义的，但不是模态可定义的。通过修正单调互模拟的定义，得到了Kripke框架上的分次互模拟的一个新定义。
The expressive power of modal logic with inclusion atoms
模态包含逻辑是基本模态逻辑的包含原子扩展，其语义定义在Kripke模型上。Kripke模型的团队只是其域的一个子集。本文给出了模态包含逻辑表达能力的一个完整刻画：一类带队的Kripke模型在模态包含逻辑中是可定义的当且仅当它在k-互模拟下是闭的，对于某个整数k，它在并下是闭的，并且它具有空队性质.我们还证明了同样的表达能力，可以通过添加一个单一的一元非空算子模态逻辑。此外，我们建立了一个指数下界的大小从模态包含逻辑到模态逻辑与非空算子的翻译。
Swap Kripke models for deontic LFIs
本文首次将交换结构与克里普克模型结合，为基于LFIs的道义逻辑构造非确定性语义，并首次给出$C^{D}_n$层级的完整公理化与语义。
Implicit Kripke Semantics and Ultraproducts in Stratified Institutions
我们提出分层机构（Goguen和Burstall机构理论的十年老的广义版本）作为一个完全抽象的模型理论方法模态逻辑。这允许在当代模态逻辑系统的巨大多样性中统一处理模型理论方面。此外，Kripke语义（在其所有的多种变化）被捕获在一个隐式的方式，从显式Kripke结构有时笨重的方面，也容纳其他形式的具体语义的模态逻辑系统。分层机构的概念权力的发展是独立于实际模态逻辑系统的具体细节的模态超积方法说明。因此，可以容易地导出具体模态逻辑中的大量紧性结果。
Graded modal logic and counting bisimulation
本文将互模拟不变片段的刻画定理推广到分级多模态逻辑，证明其在所有及有限点态 Kripke 结构上恰好对应计数互模拟等价下保持的一阶性质。
Simplified Kripke semantics for K45-like Godel modal logics and its axiomatic extensions
本文给出了经典模态逻辑K45的多值Godel对应逻辑K45（G）的简化语义。更确切地说，我们把K_（45）（G）刻画为可能性Godel Kripke框架类<W，π>的有效公式集，其中W是世界的非空集，π：W \to [0，1]是W上的可能性分布.
The Modal Logics of Kripke-Feferman Truth
我们通过Solovay式完备性结果确定了Solomon Feferman的不动点真值模型的模态逻辑及其公理化。给定一个不动点模型$\mathcal{M}$或其公理化$S$，我们找到一个模态逻辑$M$，使得模态语句$φ$是$M$的一个定理当且仅当通过用真值谓词翻译模态算子得到的语句$φ^*$在$\mathcal{M}$中为真，或在所有这样的翻译下都是$S$的一个定理。为此，我们引入了一个新版本的可能世界的语义，具有经典和非经典的世界，并建立了一个家庭的非全等模态逻辑，其内部逻辑是亚经典的这种语义的完整性。
Bi-modal Gödel logic over [0,1]-valued Kripke frames
考虑由模糊Kripke模型确定的Gödel双模态逻辑，其中命题和可达关系都是标准Gödel代数[0，1]上的无穷值，并证明了Fischer Servi直觉模态逻辑IK加上关于此语义的预线性公理的强完备性.我们也公理化的双峰类似物的$T,$ $S4,$和$S5$通过限制到模型的框架满足[0，1]-值版本的结构特性，这些逻辑的特点。作为完备性定理的应用，我们得到了双峰Gödel代数的一个表示定理。
Effect of the Choice of Connectives on the Relation between the Logic of Constant Domains and Classical Predicate Logic
不仅经典语义学可以推广，直觉Kripke语义学也可以推广，从而可以处理任意由真假值表或真假值函数表征的命题连接词。在我们以前的工作中，已经证明了Kripke有效命题序列集和经典有效命题序列集重合当且仅当所有可用的命题连接词都是单调的。本文将这一结果推广到一阶逻辑，证明了在谓词逻辑中，所有可用的命题连接词都是单调的条件是在所有常数域Kripke模型中有效的序列集，而不是Kripke有效序列集和经典有效序列集重合的充要条件.
Undecidability and non-axiomatizability of modal many-valued logics
在这项工作中，我们研究了一类全球模态逻辑所产生的Kripke框架评估某些剩余格，在文献中称为模态多值逻辑的可判定性。我们展示了一个大的家庭，这些模态逻辑是不可判定的，与经典的模态逻辑和命题逻辑定义在同一类代数。这个家族包括了在标准Lukasiewicz代数和乘积代数上计算的Kripke框架所产生的全局模态逻辑。我们改进了前面的结果，证明了全局模态Lukasiewicz和乘积逻辑甚至不能递归可公理化。我们的结论是否定地解决了开放的问题，即每个全局模态逻辑是否与它的局部模态逻辑在无限制必然规则下是封闭的。
Satisfiability problems on sums of Kripke frames
我们考虑Kripke框架上的和运算，其中一个框架-被加数族由另一个框架的元素索引。在许多情况下，和的模态逻辑继承了和的模态逻辑的有限模型性质和可判定性。本文证明了在一般条件下，和的可满足性问题是多项式空间图灵可约化为和的可满足性问题。特别地，对于许多模态逻辑，PSPACE中的可判定性是逻辑的语义表征的直接推论。
A non-distributive logic for semiconcepts of a context and its modal extension with semantics based on Kripke contexts
分别对纯双布尔代数和带算子的纯双布尔代数类提出了一个非分配的两类超代数演算\textbf{PDBL}及其模态扩张\textbf{MPDBL}.接下来提出了\textbf{PDBL}的关系语义，其中任何公式都被解释为上下文的概念。对于\textbf{MPDBL}，关系语义基于Kripke上下文，并且公式被解释为底层上下文的概念。该系统被证明是健全和完整的关系语义。将适当的序列添加到\textbf{MPDBL}导致具有基于自反、对称或传递Kripke上下文的语义的逻辑。这些系统之一是拓扑纯双布尔代数的逻辑。证明了利用\textbf{PDBL}可以表达概念知识的基本概念和关系，并可以得到涉及否定的推理。此外，绘制与粗糙集合论，上下近似的概念的上下文定义的连接。然后，它表明，使用公式和序列涉及模态算子在\textbf{MPDBL}，这些近似算子和它们的属性可以被捕获。
Gödel-Dummett and $\mathsf{BD_2}$: Linearity and Depth-Two Branching in Kripke Semantics
本文研究了GL和BD₂之间的语义关系，证明二者不可比，并展示了其结合后接近经典逻辑的特性。
Two-dimensional Kripke Semantics I: Presheaves
本文面向模态逻辑的 Kripke 语义与范畴语义，提出以预层为核心的二维语义框架，阐明两种研究路径之间的对应关系。
Kripke Contexts, Double Boolean Algebras with Operators and Corresponding Modal Systems
本文将形式概念分析中的上下文概念与粗糙集合论中的近似空间概念统一起来，定义了Kripke上下文。对于任何上下文（G，M，I），包含对象集合G上的关系和性质集合M上的关系，给出形式为（（G，R），（M，S），I）的结构。一个克里普克上下文产生了基于底层上下文的原概念和概念集合的复代数。在抽象上，定义了带算子的双布尔代数和拓扑双布尔代数.这些代数的表示结果建立在一个适当的Kripke上下文的复代数。作为自然的下一步，对应于这些代数类的逻辑被公式化。提出了一种基于上下文的dBAs，模态扩展的逻辑与运营商和拓扑上下文的dBAs。代数的表示定理导致这些逻辑的基于原型概念的语义。
Completeness results for many-valued \Lukasiewicz modal systems and relational semantics
本文研究了在\Lukasiewicz多值逻辑中增加模态的问题，以获得Kripke语义的完备性结果.定义了一类模态多值逻辑及其相应的Kripke模型和模态多值代数。完整性的结果被认为是通过一个典型的模型的建设。完备性得到模态有限值逻辑，但也为模态多值系统与无穷演绎规则。我们引入了两类框架的有限值逻辑，并表明他们定义了两个不同的类Kripke完全逻辑。
Awareness Logic: A Kripke-based Rendition of the Heifetz-Meier-Schipper Model
Heifetz，Meier和Schipper（HMS）提出了意识的晶格模型。HMS模型是无语法的，这排除了依赖于形式语言来诱导格的简单选择，并且用一个纠缠的构造来表示不确定性和无意识，使得难以评估任何一个的属性。在这里，我们提出了一个模型的基础上格的Kripke模型，诱导原子子集列入，其中的不确定性和无意识是分开的。我们证明了模型是等价的，通过定义它们之间的转换，保持公式的满足，并通过我们和HMS的结果获得完整性。
On partitioning Kripke frames of finite height
本文证明了一类模态逻辑的有限模型性质和可判定性。二元关系$R$称为预传递的，如果$R^*=\cup_{i\leq m} R^i$对于某些$m\geq 0$，其中$R^*$是$R$的传递自反闭包。$(W,R)$的高度是指前序$(W,R^*)$的高度。对有限高预传递框架刻画了特殊的分划（滤子），这意味着这些框架的有限模型性质和逻辑的可判定性。
Awareness Logic: Kripke Lattices as a Middle Ground between Syntactic and Semantic Models
关于认知建模的文献包括无语法和基于语法的框架。Heifetz，Meier \& Schipper（HMS）提出了一个无语法的意识格模型。虽然他们的格方法是优雅和直观的，但它排除了依赖形式语言来归纳格的简单选择，并且没有明确区分不确定性和无意识。与此相反，最突出的基于语法的解决方案，Fagin-Halpern（FH）模型，解释了这种区别，并提供了一个简单的意识表示，但缺乏格结构的直观性。在这里，我们结合这两种方法，通过提供一个格的Kripke模型，诱导原子子集包含，其中不确定性和无意识是分开的。我们证明了我们的模型等价于HMS和FH模型，通过定义它们之间的转换，保留了显式知识的语言公式的满意度，并通过我们和HMS的结果获得完整性。最后，我们证明了Kripke格模型可以被证明等价于FH模型（当意识是命题确定的），也相对于语言的一般意识的逻辑，FH模型最初提出。
Models of transfinite provability logic
对于任何序数Λ，我们可以定义一个多模态逻辑GLP（Λ），对于每个Λ <Λ，都有一个模态[Λ]。这些表示强度增加的可证明性谓词。虽然GLP（Λ）没有Kripke模型，但Ignatiev证明，确实可以用自然数模态构建无变量片段的Kripke模型。后来，Icard为同一片段定义了一个拓扑模型，这与Ignatiev的非常密切相关。在本文中，我们展示了如何推广这些结构任意Λ。更一般地，对于每个Θ，Λ，我们建立了Kripke模型I（Θ，Λ）和拓扑模型T（Θ，Λ），并表明GLP（Λ）的闭合片段对于这两种结构都是合理的，并且是完整的，只要Θ足够大。
What Kinds of Connectives Cause the Difference between Intuitionistic Predicate Logic and the Logic of Constant Domains?
直觉Kripke语义可以推广到任意命题连接词的真假值函数。我们将这种广义Kripke语义推广到一阶逻辑，并研究了连接词的选择如何改变直觉谓词逻辑和常域逻辑之间在序列有效性方面的关系。我们的主要结果给出了直觉谓词逻辑中的有效序列集与常域逻辑中的有效序列集重合的一个简单的充要条件。
Explicit Evidence Systems with Common Knowledge
本文开发了一种包含个体与公共知识证据项的多智能体证明逻辑，定义了 Kripke 风格语义并证明其可靠性与完备性，同时分析了其与 S4 的关系及协调攻击问题。
Epistemic Logic with Partial Dependency Operator
本文将$\textit{partial}$依赖模态$\mathcal{D}$引入认知逻辑，以推理Kripke模型中的$\textit{partial}$依赖关系。由此产生的依赖认知逻辑具有良好的表现力和美丽的性质。提供了几个有趣的例子，突出了这种逻辑的实际用途。然后讨论了该逻辑的互模拟性，并给出了该逻辑的一个子语言的可靠的强完备公理化。
Base-extension Semantics for Intuitionistic Modal Logics
本文为Simpson直觉主义模态逻辑建立基扩展语义，并证明其相对自然演绎系统的可靠性与完备性。
A $j$-translation with Kripke forcing relation
本文提出一种结合j-翻译与Kripkeforcing的内部逻辑拓扑学翻译，证明其对直觉逻辑和Heyting算术的正确性，并扩展了de Jongh和Goodman的sheaf模型。
Localizing Finite-Depth Kripke Models
我们可以将一阶（或命题）直觉Kripke模型看作是经典模型的有序集合。在本文中，我们表明，有限深度的Kripke模型在任意一阶语言或命题语言，本地（经典）真理的公式是等价的非经典真理（真理的Kripke语义）的弗里德曼翻译的公式，即$ α\Vdash A^ρ\Leftrightarrow \mathfrak{M}_α\models A$。我们介绍这个事实的一些应用。推广了[Ardeshir and Hessam 2002]的结果，证明了Heyting算术$ {\sf HA} $的半窄Kripke模型是局部的$ {\sf PA} $ .
Modal definability in Kripke's theory of truth
本文为克里普克真理论中的非正式模态定义引入模态语言，证明根基性和悖论性可表达而内在性不可表达，并刻画模态可定义关系及完全公理化其语义。
Some Problems in Logic: Applications of Kripke's Notion of Fulfilment
这是对S.克里普克的成就感。受Paris-Harrington声明的启发，克里普克一直在寻找哥德尔不完备性定理的证明，它是模型论的，自然的（没有自我引用），并且容易。实现为证明和模型理论提供了一个多功能的工具。我们首先简短的证明一些经典的结果。有两个新的结果：存在本原递归函数的容易定义的子环$R$，使得对于$ω$上的任何非主超滤子$D$，$R/D$是Peano算术的递归饱和模型;理论$\textsf{T}$和对于任何给定的r.e.集合，我们可以可行地找到一个$Σ_1^0$公式，半表示它在$\textsf{T}$。然后，我们给出了一个版本的Herbrand定理，和Hilbert-Ackermann方法证明的一致性，回答了一个问题的D。Guangzhou：\[\{\ulcornerϕ\urcorner\inΠ^0_k:ϕ\text{ is }Σ^0_k\text{-conservative over $\textsf{PA}$}\}\]是一套完整的$Π^0_2$。我们推广了H.弗里德曼的方法的结果，如$Σ^1_2\textsf{-AC}$是$Π^1_3$ -保守的$(Π^1_1\textsf{-CA})_{<\varepsilon_0}\upharpoonright$，随着统一版本\[\forallα<\varepsilon_0\;(Π^1_1\textsf{-CA})_α\uphar…
Toward the van Benthem Characterization Theorem for Non-Distributive Modal Logic
本文将模拟、互模拟及图像有限模型、模态饱和模型、超滤扩张和超幂扩张等模型论概念推广到非分配模态逻辑的极性语义，并据此证明了Hennessy-Milner定理与van Benthem刻画定理。
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic
在他们的开创性论文中，阿特莫夫和Protopescu提供了希尔伯特形式系统，Brower-Heyting-Kolmogorov和Kripke语义的直觉信念和知识的逻辑。随后Krupski证明了直觉知识的逻辑是PSPACE完全的，Su和Sano提供了享有子公式属性的演算。本文通过提供具有子公式性质且终止于线性深度的隐式演算，继续了对直觉主义认知逻辑隐式演算的研究。我们的演算允许我们设计一个过程，对于无效的公式，返回一个最小深度的Kripke模型。最后我们还讨论了反驳的反演算，即证明无效性的反演算。
Decidability of quantified propositional intuitionistic logic and S4 on trees
量化命题直觉主义逻辑是由命题直觉主义逻辑通过在命题上添加量词\forall p，\exists p而得到的.在Kripke语义学的上下文中，一个命题是一个向上封闭的模型结构中世界的子集。Kremer（1997）证明了基于所有偏序类的量化命题直觉主义逻辑Hπ+与完全二阶逻辑递归同构。他提出了一个问题，即从限制到树的逻辑是否是可公理化的。事实证明，它是可判定的。所使用的方法也可以用来建立模态S4的可判定性与类似类型的Kripke结构的命题量化。
Hennessy-Milner Type Theorems for Fuzzy Multimodal Logics Over Heyting Algebras
本文针对基于完备线性序Heyting代数的模糊多模态逻辑，引入Kripke模型间弱互模拟概念，证明三个Hennessy-Milner型定理，揭示不同公式集下弱互模拟与特定模糊互模拟的一致性。
Metrics for Formal Structures, with an Application to Kripke Models and their Dynamics
本报告介绍并研究了一系列关于指向Kripke模型的度量。度量是汉明距离的推广，适用于可数无限二进制字符串，并通过扩展，逻辑理论或语义结构。我们首先研究所得到的度量空间的拓扑性质。一个关键结果为具有Stone性质的空间提供了充分条件，即，紧的、全不连通的和豪斯多夫。其次，我们转向映射，它是一种广泛使用的类型的模型转换，产品更新，引起连续映射的诱导拓扑。
Knowing the Model
认知模态逻辑通常将认知情境视为克里普克模型。我们考虑一个更基本的方法：把一个认知情境看作是一组W的可能状态/世界--最大一致的命题集--具有由W确定的常规可及性关系。我们发现，在许多认识的情况下，W不是一个Kripke模型：W是一个Kripke模型的充要条件是所谓的“完全解释属性”-一个命题形式的共同知识的模型-这一直是一个隐藏的（和忽视的）假设在认识模态逻辑。我们勾勒出一个理论，描述了他们的一般性认识模型。我们认为新模型的概念和实用价值，特别是代表部分知识，不对称知识和意识。
A cut-free proof system for a predicate extension of the logic of provability
本文介绍了一个证明系统$\mathsf{NQGL}$，它是由$\mathbf{K}$和Löb公式$\Box(\Box p\supset p)\supset\Box p$定义的逻辑$\mathbf{GL}$的Kripke完全谓词扩展，即可证性逻辑. $\mathsf{NQGL}$是Gentzen微积分$\mathsf{LK}$的模态扩展。虽然$\mathsf{NQGL}$的命题片段公理化了$\mathbf{GL}$，但它没有Löb公式作为它的公理。相反，它有一个非紧规则，即一个具有可数个前提的推导规则。我们证明了$\mathsf{NQGL}$具有割容许性，并且对于Kripke框架类是完备的，使得对于每个世界，从世界出发的路径长度的上确界是有限的。
Kripke-Joyal forcing for type theory and uniform fibrations
本文提出将 Kripke-Joyal 力迫推广到类型论的新方法，用以连接预层范畴中的代数结构与内部类型论判断，并应用于刻画同伦类型论中的代数弱分解系统。
Sahlqvist theory for impossible worlds
我们将统一对应论推广到不可能世界的Kripke框架及其相关的正则模态逻辑。这些逻辑的模态联结不需要是正规的：只需要较弱的可加性和乘法性。在概念上，有人认为，它们缺乏必要性，使得规则模态逻辑比正常的模态逻辑更适合在形式化的认识和道义设置。从技术的角度来看，正则性被证明是非常自然的，足以处理代数正规性约翰逊式。事实上，加法性和乘法性是将琼森最初的规范性证明扩展到某些正则分配模态逻辑的完整萨尔奎斯特类的关键，自然地概括了分配模态逻辑。最有趣的是，加性和乘性也是原始（即正常）DML中约翰逊式正规性的关键。我们的贡献包括：在分配格命题基上定义了正则模态逻辑的Sahlqvist不等式，证明了它们遵循Jónsson策略的规范性，并将ALBA算法应用于两个非经典的正则模态逻辑的构造（分配格和直觉）的基础，证明适应ALBA是保证成功的语法定义的类，其中适当地包括Sahlqvist一个;最后，应用前面的结果，代替Kripke的证明，证明了Lemmon的认知逻辑E2-E5关于具有不可能世界的Kripke框架的初等类的强完备性。
Realisability for Infinitary Intuitionistic Set Theory
我们介绍了一个基于有序图灵机（OTM）的无穷直觉集合论的可实现性语义。我们表明，我们的OTM-可实现性的概念是健全的某些系统的无穷直觉主义逻辑，并实现了所有公理的无穷Kripke-Platek集合论。最后，我们使用我们的可实现性概念的一个变体来证明（有限）直觉Kripke-Platek集合论的命题容许规则正是直觉命题逻辑的容许规则。
Elementary modal logics and circuit complexity
本文证明有限公理化初等模态逻辑的有效性问题属于P，并利用图论复杂性结果，在假设P≠NP下构造无限多个非初等的K4-稳定逻辑，条件性否定回答开放问题。
Provability Models
本文提出名为可证性模型的经典模态逻辑新型克里普克式语义，证明了多类模态逻辑、解释性逻辑ILM对该类模型的可靠性与完全性，并将其改进为谓词可判定版本。
Wijesekera-style constructive modal logics
我们定义了一个命题构造性模态逻辑族，每个模态逻辑对应于一个不同的经典模态系统。逻辑定义在风格的Wijesekera的建设性模态逻辑，并证明理论和语义动机。一方面，它们对应于经典模态逻辑的标准演算的单一后继限制。另一方面，它们是通过将直觉Kripke模型的遗传性纳入模态公式的经典满足子句而获得的。我们表明，对于所考虑的经典逻辑，证明理论和语义方法返回相同的建设性系统。
The Distributive Full Lambek Calculus with Modal Operators
本文研究了在非交换条件下，考虑$\Box$和$\Diamond$的带有模态算子的有界分配剩余格的逻辑。我们为这样的子结构模态逻辑引入关系语义。通过离散对偶和正则扩张证明了任何正则逻辑都是Kripke完备的。也就是说，我们表明，一个模态扩展的分配充分Lambek演算是其框架的逻辑，如果它的品种是封闭的规范下的扩展。在此基础上，我们建立了剩余分配模态代数与基于Priestley空间的拓扑Kripke结构之间的Priestley式对偶。
Questions and dependency in intuitionistic logic
近年来，疑问句逻辑和依赖逻辑在探究逻辑和依赖逻辑两个密切相关的框架中得到了研究。这些研究假设经典逻辑作为陈述的背景逻辑，并在这个经典核心中加入了表达问题和依赖关系的公式。在本文中，我们通过在直觉主义逻辑的背景下研究问题和依赖关系来拓宽这些研究的范围。我们提出了一个直观的团队语义，团队嵌入在直观的Kripke模型。伴随逻辑是直觉主义逻辑的一个保守的扩展，带有问题和依赖公式。我们建立了一些关于这个逻辑的结果，包括一个范式的结果，一个完整性的结果，并翻译到经典的查询逻辑和模态依赖逻辑。
Infinitary provability logic
本文研究Gödel-Löb可证性逻辑的无穷性对应物，提出非良基深层推理系统$\dgla$，证明其相对于良基传递Kripke框架的可靠性与完备性，并借助Kripke-Platek集合论建立无穷可证性解释，表明Hilbert式变体可靠，且在某些条件下无穷可证性逻辑介于两者之间。
Propositional Mixed Logic: Its Syntax and Semantics
在本文中，我们提出了一个命题逻辑（称为混合逻辑）包含不相交的副本的最小，直觉和经典逻辑。我们证明了这个逻辑的Kripke语义的完备性定理。建立了混合逻辑与极小逻辑、直觉逻辑和经典逻辑之间的关系。最后，我们提出了这个逻辑的微积分版本。
A Simplicial Model for $KB4_n$: Epistemic Logic with Agents that May Die
多智能体认知逻辑S5的标准语义是基于Kripke模型，其可达性关系是自反的，对称的和传递的。这个一维结构包含了超越成对相互作用的隐式高维信息，我们在以前的工作中将其形式化为纯单纯模型（信息与计算，2021）。在这里，我们将理论扩展到包含不一定是纯的单纯模型。Kripke模型的对应类是那些可达性关系是对称和传递的，但可能不是自反的。这些模型对应于认知逻辑KB4。不纯单纯模型出现在两个可能的世界可能没有相同的代理集的情况下。我们用同步系统中进程可能崩溃的分布式计算例子来说明它。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。