模態夥伴

在邏輯中，中間(超直覺)邏輯 L 的模態夥伴是通過下面的特定規範變換解釋 L 的正規模態邏輯。模態夥伴共享最初中間邏輯的各種性質，這確使使用為模態邏輯開發的工具研究中間邏輯。

Gödel–McKinsey–Tarski 變換

設 A 是命題直覺公式。模態公式 T(A)通過在 A 的複雜性上的歸納來定義:

$T(p)=\Box p$ 對於任何命題變量 $p$，

$T(\bot )=\bot$，

$T(A\land B)=T(A)\land T(B)$，

$T(A\lor B)=T(A)\lor T(B)$，

$T(A\to B)=\Box (T(A)\to T(B))$。

直覺邏輯中的否定定義為 $A\to \bot$，我們還有

$T(\neg A)=\Box \neg T(A)$。

$T$ 叫做哥德爾變換或哥德爾–McKinsey–塔斯基變換。這個變換有時以稍微不同的方式來定義: 例如，我們可以在所有子公式前插入 $\Box$。所有變體都被證明在 S4 中等價。

模態夥伴

已隱藏部分未翻譯內容，歡迎參與翻譯。

For any normal modal logic M which extends S4, we define its si-fragment ρM as

$\rho M=\{A;\,M\vdash T(A)\}.$

The si-fragment of any normal extension of S4 is an intermediate logic. A modal logic M is a modal companion of an intermediate logic L if $L=\rho M$.

Every intermediate logic has modal companions. The smallest modal companion of L is

$\tau L=\mathbf {S4} +\{T(A);\,L\vdash A\},$

where + denotes normal closure. It can be shown that every intermediate logic also has the largest modal companion, which is denoted by σL. A modal logic M is a companion of L if and only if $\tau L\subseteq M\subseteq \sigma L$.

For example, S4 itself is the smallest modal companion of the intuitionistic logic (IPC). The largest modal companion of IPC is the Grzegorczyk logic Grz, axiomatized by the axiom

$\Box (\Box (A\to \Box A)\to A)\to A$

over K. The smallest modal companion of the classical logic (CPC) is Lewis' S5, whereas its largest modal companion is the logic

$\mathbf {Triv} =\mathbf {K} +A\equiv \Box A.$

More examples:

L	τL	σL	other companions of L
IPC	S4	Grz	S4.1, Dum, ...
KC	S4.2	Grz.2	S4.1.2, ...
LC	S4.3	Grz.3	S4.1.3, S4.3Dum, ...
CPC	S5	Triv	see below

Blok–Esakia 同構

已隱藏部分未翻譯內容，歡迎參與翻譯。

The set of extensions of an intermediate logic L ordered by inclusion forms a complete lattice, denoted ExtL. Similarly, the set of normal extensions of a modal logic M is a complete lattice NExtM. The companion operators ρM, τL, and σL can be considered as mappings between the lattices ExtIPC and NExtS4:

$\rho \colon \mathrm {NExt} \,\mathbf {S4} \to \mathrm {Ext} \,\mathbf {IPC} ,$

$\tau ,\sigma \colon \mathrm {Ext} \,\mathbf {IPC} \to \mathrm {NExt} \,\mathbf {S4} .$

It is easy to see that all three are monotone, and $\rho \circ \tau =\rho \circ \sigma$ is the identity function on ExtIPC. L. Maximova and V. Rybakov have shown that ρ, τ, and σ are actually complete lattice homomorphisms. The corner-stone of the theory of modal companions is the Blok–Esakia theorem, proved independently by Wim Blok and Leo Esakia. It states

The mappings ρ and σ are mutually inverse lattice isomorphisms of ExtIPC and NExtGrz.

Accordingly, σ and the restriction of ρ to NExtGrz are called the Blok–Esakia isomorphism. An important corollary to the Blok–Esakia theorem is a simple syntactic description of largest modal companions: for every intermediate logic L,

$\sigma L=\tau L+\mathbf {Grz} .$

語義描述

已隱藏部分未翻譯內容，歡迎參與翻譯。

The Gödel translation has a frame-theoretic counterpart. Let $\mathbf {F} =\langle F,R,V\rangle$ be a transitive and reflexive modal general frame. The preorder R induces the equivalence relation

$x\sim y\iff x\,R\,y\land y\,R\,x$

on F, which identifies points belonging to the same cluster. Let $\langle \rho F,\leq \rangle =\langle F,R\rangle /{\sim }$ be the induced quotient partial order (i.e., ρF is the set of equivalence classes of $\sim$), and put

$\rho V=\{A/{\sim };\,A\in V,A=\Box A\}.$

Then $\rho \mathbf {F} =\langle \rho F,\leq ,\rho V\rangle$ is an intuitionistic general frame, called the skeleton of F. The point of the skeleton construction is that it preserves validity modulo Gödel translation: for any intuitionistic formula A,

A is valid in ρF if and only if T(A) is valid in F.

Therefore the si-fragment of a modal logic M can be defined semantically: if M is complete with respect to a class C of transitive reflexive general frames, then ρM is complete with respect to the class $\{\rho \mathbf {F} ;\,\mathbf {F} \in C\}$.

The largest modal companions also have a semantic description. For any intuitionistic general frame $\mathbf {F} =\langle F,\leq ,V\rangle$, let σV be the closure of V under Boolean operations (binary intersection and complement). It can be shown that σV is closed under $\Box$, thus $\sigma \mathbf {F} =\langle F,\leq ,\sigma V\rangle$ is a general modal frame. The skeleton of σF is isomorphic to F. If L is an intermediate logic complete with respect to a class C of general frames, then its largest modal companion σL is complete with respect to $\{\sigma \mathbf {F} ;\,\mathbf {F} \in C\}$.

The skeleton of a Kripke frame is itself a Kripke frame. On the other hand, σF is never a Kripke frame if F is a Kripke frame of infinite depth.

保持定理

已隱藏部分未翻譯內容，歡迎參與翻譯。

The value of modal companions and the Blok–Esakia theorem as a tool for investigation of intermediate logics comes from the fact that many interesting properties of logics are preserved by some or all of the mappings ρ, σ, and τ. For example,

• decidability is preserved by ρ, τ, and σ,
• finite model property is preserved by ρ, τ, and σ,
• tabularity is preserved by ρ and σ,
• Kripke completeness is preserved by ρ and τ,
• first-order definability on Kripke frames is preserved by ρ and τ.

其他性質

已隱藏部分未翻譯內容，歡迎參與翻譯。

Every consistent intermediate logic L has an infinite number of modal companions, and moreover, the set $\rho ^{-1}(L)$ of modal companions of L contains an infinite descending chain. For example, $\rho ^{-1}(\mathbf {CPC} )$ consists of S5, and the logics $L(C_{n})$ for every positive integer n, where $C_{n}$ is the n-element cluster. The set of modal companions of any L is either countable, or it has the cardinality of the continuum. Rybakov has shown that the lattice ExtL can be embedded in $\rho ^{-1}(L)$; in particular, a logic has a continuum of modal companions if it has a continuum of extensions (this holds, for instance, for all intermediate logics below KC). It is unknown whether the converse is also true.

The Gödel translation can be applied to rules as well as formulas: the translation of a rule

$R={\frac {A_{1},\dots ,A_{n}}{B}}$

is the rule

$T(R)={\frac {T(A_{1}),\dots ,T(A_{n})}{T(B)}}.$

A rule R is admissible in a logic L if the set of theorems of L is closed under R. It is easy to see that R is admissible in an intermediate logic L whenever T(R) is admissible in a modal companion of L. The converse is not true in general, but it holds for the largest modal companion of L.

引用

• Alexander Chagrov and Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997.
• Vladimir V. Rybakov, Admissibility of Logical Inference Rules, vol. 136 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1997.