モーダルコンパニオン

論理学において、超直観主義（中間）論理Lの様相コンパニオンは、以下に説明する特定の標準的な翻訳によってL を解釈する通常の様相論理です。様相コンパニオンは、元の中間論理のさまざまなプロパティを共有しており、様相論理用に開発されたツールを使用して中間論理を研究することができます。

A を命題的 直観主義式とする。様相式T ( A ) はAの複雑性に関する帰納法により定義される。

${\displaystyle T(p)=\Box p,}$任意の命題変数 に対して、${\displaystyle p}$

${\displaystyle T(\bot )=\bot ,}$

${\displaystyle T(A\land B)=T(A)\land T(B),}$

${\displaystyle T(A\or B)=T(A)\or T(B),}$

${\displaystyle T(A\to B)=\Box (T(A)\to T(B)).}$

否定は直観主義論理では で定義されるので、 ${\displaystyle A\to \bot }$

${\displaystyle T(\neg A)=\Box \neg T(A).}$

T はゲーデル変換またはゲーデル-マッキンゼー-タルスキー変換と呼ばれます。変換は、わずかに異なる方法で表されることがあります。たとえば、すべての部分式の前に を挿入する場合があります。このようなすべての変形は、S4で同等であることが証明されています。 ${\displaystyle \Box}$

S4を拡張する任意の通常の様相論理Mに対して、そのsiフラグメントρMを次のように 定義する。

${\displaystyle \rho M=\{A\mid M\vdash T(A)\}.}$

S4の任意の正規拡張の si フラグメントは、超直観主義論理です。 様相論理M は、次の場合、超直観主義論理Lの様相コンパニオンです。 ${\displaystyle L=\rho M}$

すべての超直観論理には様相伴が存在する。Lの最小の様相伴は

${\displaystyle \tau L=\mathbf {S4} \oplus \{T(A)\mid L\vdash A\},}$

ここで、 は正規閉包を表します。すべての超直観主義論理には、 σLで表される最大の様相コンパニオンも存在することがわかります。様相論理MがLのコンパニオンとなるのは、 の場合のみです。 ${\displaystyle \oplus}$${\displaystyle \tau L\subseteq M\subseteq \sigma L}$

例えば、S4自体は直観主義論理（IPC）の最小の様相的伴侶である。IPCの最大の様相的伴侶はグジェゴルチク論理Grzであり、公理として次のようになる。

${\displaystyle \Box (\Box (A\to \Box A)\to A)\to A}$

K上の。古典論理 ( CPC )の最小の様相の仲間はルイスのS5であるのに対し、その最大の様相の仲間は論理

${\displaystyle \mathbf {Triv} =\mathbf {K} \oplus (A\leftrightarrow \Box A).}$

その他の例:

包含によって順序付けられた超直観論理Lの拡張の集合は完全な格子を形成し、 Ext Lと表記されます。同様に、様相論理Mの正規拡張の集合は完全な格子 NExt Mです。コンパニオン演算子ρM、τL、およびσL は、格子 Ext IPCと NExt S4の間のマッピングとして考えることができます。

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

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

これら3つはすべて単調であり、はExt IPC上の恒等関数であることが簡単に分かります。L. MaksimovaとV. Rybakovは、ρ、τ、σがそれぞれ完全、join-complete、meet-complete格子準同型であることを示しました。様相同関数の理論の基礎は、 Wim BlokとLeo Esakiaによって独立に証明されたBlok-Esakia定理です。それは次のように述べています。 ${\displaystyle \rho \circ \tau =\rho \circ \sigma }$

マッピングρとσ は、Ext IPCとNExt Grzの相互逆格子同型です。

したがって、σとρのNExt Grzへの制限は、ブロック・エサキア同型性と呼ばれます。ブロック・エサキア定理の重要な系は、最大様相コンパニオンの簡単な構文記述です。すべての超直観主義論理Lに対して、

${\displaystyle \sigma L=\tau L\oplus \mathbf {Grz} .}$

ゲーデル変換にはフレーム理論上の対応物がある。を推移的かつ反射的な様相一般フレームとする。前置順序Rは同値関係を誘導する。${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$

${\displaystyle x\sim y\iff x\,R\,y\land y\,R\,x}$

F上の は、同じクラスターに属する点を識別する。を誘導商半順序（すなわち、ρFはの同値類の集合）とし、 ${\displaystyle \langle \rho F,\leq \rangle =\langle F,R\rangle /{\sim }}$ ${\displaystyle \sim}$

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

は直観主義的な一般フレームであり、Fのスケルトンと呼ばれる。スケルトン構築のポイントは、ゲーデル変換を法として妥当性を維持することである。任意の直観主義式Aに対して、 ${\displaystyle \rho \mathbf {F} =\langle \rho F,\leq ,\rho V\rangle }$

A がρ Fで有効であるのは、T ( A ) がFで有効である場合に限ります。

したがって、様相論理Mの si フラグメントは意味的に定義できます。Mが推移的反射的一般フレームのクラスCに関して完全である場合、ρM はクラスに関して完全です。 ${\displaystyle \{\rho \mathbf {F} ;\,\mathbf {F} \in C\}}$

最大の様相コンパニオンにも意味的記述があります。任意の直観主義一般フレーム に対して、σV をブール演算 (二項積と補集合) によるVの閉包とします。σVはの下で閉じていることが示され、したがって は一般様相フレームです。σ FのスケルトンはFと同型です。Lが一般フレームのクラスCに関して完全な超直観主義論理である場合、その最大の様相コンパニオンσL はに関して完全です。 ${\displaystyle \mathbf {F} =\langle F,\leq ,V\rangle }$${\displaystyle \Box}$${\displaystyle \sigma \mathbf {F} =\langle F,\leq ,\sigma V\rangle }$${\displaystyle \{\sigma \mathbf {F} ;\,\mathbf {F} \in C\}}$

クリプキフレームのスケルトンはそれ自体がクリプキフレームです。一方、F が無限の深さのクリプキフレームである 場合、 σ F は決してクリプキフレームにはなりません。

様相同性とブロック・エサキア定理が中間論理の調査ツールとして価値があるのは、論理の多くの興味深い性質がρ、σ、τの写像の一部またはすべてによって保存されるという事実から来ている。例えば、

• 決定可能性はρ、τ、σによって保存される。
• 有限モデルの性質はρ、τ、σによって保存される。
• 表形式性はρとσによって保存される。
• クリプキ完全性はρとτによって保存される。
• クリプキフレーム上の一階の定義可能性はρとτによって保存されます。

すべての中間論理L には無限の数の様相コンパニオンがあり、さらに、Lの様相コンパニオンの集合には無限の下降チェーン が含まれます。たとえば、はS5と、すべての正の整数nに対する論理で構成されます( はn要素のクラスター)。任意のLの様相コンパニオンの集合は、可算 であるか、連続体の濃度を持ちます。Rybakov は、格子 Ext Lが に埋め込むことができることを示しました。特に、論理は、拡張の連続体を持つ場合、様相コンパニオンの連続体を持ちます (これは、たとえば、KCより下のすべての中間論理に当てはまります)。逆もまた真であるかどうかは不明です。 ${\displaystyle \rho^{-1}(L)}$${\displaystyle \rho ^{-1}(\mathbf {CPC} )}$${\displaystyle L(C_{n})}$${\displaystyle C_{n}}$${\displaystyle \rho^{-1}(L)}$

ゲーデル変換は、規則だけでなく公式にも適用できる。規則の変換は、

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

ルールは

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

規則R は、 Lの定理の集合がR の下で閉じている場合に、論理Lで許容されます。 T ( R ) がLの様相コンパニオンで許容される場合は常に、Rが超直観主義論理Lで許容されることは容易にわかります。逆は一般には真ではありませんが、Lの最大の様相コンパニオンでは当てはまります。

• Alexander Chagrov と Michael Zakharyaschev、「Modal Logic」、Oxford Logic Guides の第 35 巻、Oxford University Press、1997 年。
• Vladimir V. Rybakov、「論理的推論規則の許容性」、Studies in Logic and the Foundations of Mathematics の第 136 巻、Elsevier、1997 年。