一个结合Kripkeforcing关系的j-翻译

类型论与一致纤维化的 Kripke-Joyal 力迫

Kripke-Joyal forcing for type theory and uniform fibrations

本文提出将 Kripke-Joyal 力迫推广到类型论的新方法，用以连接预层范畴中的代数结构与内部类型论判断，并应用于刻画同伦类型论中的代数弱分解系统。

Localizing Finite-Depth Kripke Models

We can look at a first-order (or propositional) intuitionistic Kripke model as an ordered set of classical models. In this paper, we show that for a finite-depth Kripke model in an arbitrary first-order language or propositional language, local (classical) truth of a formula is equivalent to non-classical truth (truth in the Kripke semantics) of a Friedman's translation of that formula, i.e. $ α\Vdash A^ρ\Leftrightarrow \mathfrak{M}_α\models A$. We introduce some applications of this fact. We extend the result of [Ardeshir and Hessam 2002] and show that semi-narrow Kripke models of Heyting Ari…

模态剩余逻辑中的集合论类Kripke模型

Kripke-like models of Set Theory in Modal Residuated Logic

本文借助Ono–Komori剩余Kripke模型推广Fitting的直觉主义集合论语义，构建模态剩余逻辑中的von Neumann层级，建立与Heyting值模型的公式翻译，并提出可构造集全域概念。

模态逻辑的集合论翻译：通过力迫法

A Set-Theoretic Translation of Modal Logic via Forcing

本文通过力迫法为模态逻辑的扩张理论建立集合论翻译，证明其可靠性与完备性，并构建相应的Kripke模型。

The Modal Logics of Kripke-Feferman Truth

We determine the modal logic of fixed-point models of truth and their axiomatizations by Solomon Feferman via Solovay-style completeness results. Given a fixed-point model $\mathcal{M}$, or an axiomatization $S$ thereof, we find a modal logic $M$ such that a modal sentence $φ$ is a theorem of $M$ if and only if the sentence $φ^*$ obtained by translating the modal operator with the truth predicate is true in $\mathcal{M}$ or a theorem of $S$ under all such translations. To this end, we introduce a novel version of possible worlds semantics featuring both classical and nonclassical worlds and es…

The expressive power of modal logic with inclusion atoms

Modal inclusion logic is the extension of basic modal logic with inclusion atoms, and its semantics is defined on Kripke models with teams. A team of a Kripke model is just a subset of its domain. In this paper we give a complete characterisation for the expressive power of modal inclusion logic: a class of Kripke models with teams is definable in modal inclusion logic if and only if it is closed under k-bisimulation for some integer k, it is closed under unions, and it has the empty team property. We also prove that the same expressive power can be obtained by adding a single unary nonemptine…