様相論理のセマンティクス 命題様相論理の言語は、可算無限の 命題変数 の集合、真理関数結合子 の集合（この記事では）から構成される。→ {\displaystyle \to } ¬ {\displaystyle \neg } ◻ {\displaystyle \Box } ◊ {\displaystyle \Diamond } ） ◻ {\displaystyle \Box } 定義できる。 ◊ A := ¬ ◻ ¬ A {\displaystyle \Diamond A:=\neg \Box \neg A}
対応と完全性 意味論は、意味的帰結 関係がその構文的対応物である構文的帰結 導出可能性 ）を反映している場合にのみ、論理（すなわち導出システム）を調査する上で有用である。 どの様相論理がクリプキフレームのクラスに関して健全かつ完全であるかを知ること、そしてそれがどのクラスであるかを決定することは極めて重要である。
任意のクリプキフレームのクラスC に対して、Thm( C ) は正規様相論理 です(特に、最小正規様相論理K の定理は、すべてのクリプキモデルで有効です)。しかし、一般に逆は成り立ちません。研究されている様相システムのほとんどは、単純な条件で記述されるフレームのクラスで完全ですが、クリプキ不完全正規様相論理も存在します。そのようなシステムの自然な例は、ジャパリゼの多様相論理 です。
通常の様相論理L は、 C = Mod( L )の場合、フレームのクラスCに 対応する 。言い換えれば、Cは Lが C に関して健全であるような最大のフレームのクラスである。したがって、 L がクリプキ完全であるのは、L が対応するクラスに関して完全である場合に限る。
スキーマT を考えてみましょう。◻ A → A {\displaystyle \Box A\to A} Tは任意の 反射 フレームにおいて有効である。 ⟨ W 、 R ⟩ {\displaystyle \langle W,R\rangle } w ⊩ ◻ A {\displaystyle w\Vdash \Box A} w ⊩ A {\displaystyle w\Vdash A} w R w なので。一方、T を検証するフレームは反射的でなければなりません。w ∈ W を 固定し、命題変数p の充足性を次のように定義します。 u ⊩ p {\displaystyle u\Vdash p} w R u の場合に限る。 w ⊩ ◻ p {\displaystyle w\Vdash \Box p} w ⊩ p {\displaystyle w\Vdash p} T によって、つまり定義を使用して w R wとなります ⊩ {\displaystyle \Vdash } Tは 反射的クリプキフレームのクラスに対応する。
L の対応するクラスを特徴付ける方が、その完全性を証明するよりもはるかに容易な場合が多いため、対応関係は完全性証明の指針となる。対応関係は様相論理の不完全性を示すためにも用いられる。L 1 ⊆ L 2 が 同じフレームのクラスに対応する正規様相論理であると仮定するが、 L 1 は L 2 のすべての定理を証明しない。この場合、 L 1 はクリプキ不完全である。例えば、スキーマは次のようになる。 ◻ （ A ↔ ◻ A ） → ◻ A {\displaystyle \Box (A\leftrightarrow \Box A)\to \Box A} これは不完全な論理を生成する。なぜなら、 GL と同じクラスのフレーム（すなわち、推移的かつ逆の整礎フレーム）に対応するが、GLの トートロジーを証明しないからである。◻ A → ◻ ◻ A {\displaystyle \Box A\to \Box \Box A}
一般的な様相公理図式 以下の表は、一般的な様相論理の公理とそれに対応するクラスを一覧にしたものです。公理の命名はしばしば異なります。ここでは、公理Kは ソール・クリプキ にちなんで名付けられ、公理Tは 認識論理 の真理公理 にちなんで名付けられ、公理Dは 義務論理 にちなんで名付けられ、公理Bは LEJ ブロウワー にちなんで名付けられ、公理4 と5は CI ルイス の記号論理体系 の番号付けに基づいて名付けられています。
公理Kは 次のように書き換える こともできます。◻ [ （ A → B ） ∧ A ] → ◻ B {\displaystyle \Box [(A\to B)\land A]\to \Box B} モーダス・ポネンスが 推論規則 として論理的に確立されることを示している。
公理D については、◊ A {\displaystyle \Diamond A} ◊ ⊤ {\displaystyle \Diamond \top } ◊ A → ◊ ⊤ {\displaystyle \Diamond A\rightarrow \Diamond \top } これは、存在量化子による量化の範囲に関する 暗黙の含意に似ています。
一般的なモーダルシステム 以下の表は、いくつかの一般的な標準様相システムを一覧にしたものです。一部のシステムのフレーム条件は簡略化されています。論理は表に示されているフレームクラスに関して健全かつ完全 ですが、より広いフレームクラスに対応する場合もあります。
標準モデル 任意の通常の様相論理Lに対して、 最大整合集合を モデルとして用いる標準的な手法を応用することで、L の非定理を正確に反駁する クリプキモデル（正準モデルと呼ばれる）を構築することができる。正準クリプキモデルは、代数意味論における リンデンバウム・タルスキー代数の 構成と同様の役割を果たす。
一連の論理式は、L の定理とモーダス・ポネンスを用いて矛盾を導き出せない場合に、L 整合的であると言います。 最大 L 整合集合 （ 略してL - MCS ）とは、真の L 整合上位集合を持たないL 整合集合のことです。
L の標準モデル はクリプキモデルである ⟨ W 、 R 、 ⊩ ⟩ {\displaystyle \langle W,R,\Vdash \rangle } Wはすべての L - MCS の集合であり、関係R と⊩ {\displaystyle \Vdash }
X R Y {\displaystyle X\;R\;Y} A {\displaystyle A} ◻ A ∈ X {\displaystyle \Box A\in X} A ∈ Y {\displaystyle A\in Y} X ⊩ A {\displaystyle X\Vdash A} A ∈ X {\displaystyle A\in X} 標準モデルはL のモデルであり、すべてのL - MCS は L のすべての定理を含んでいます。ツォルンの補題 により、各L - MCS は L - MCS に含まれ、特にL で証明不可能なすべての論理式は標準モデルに反例を持ちます。
正準モデルの主な応用は、完全性証明です。K の正準モデルの性質は、すべて のクリプキフレームのクラスに関してK が完全であることを直ちに意味します。この議論は任意のL に対しては機能しません。なぜなら、正準モデルの基礎となる フレームが L のフレーム条件を満たすという保証はないからです。
クリプキフレームの性質P に関して、式または式の集合Xが 正準であるとは、
X は P を 満たすすべてのフレームで有効です。X を含む任意の通常の様相論理Lに対して、 L の標準モデルの基礎フレームはP を 満たす。正準論理式の集合の和集合自体が正準論理式である。以上の議論から、正準論理式によって公理化された論理はクリプキ完全かつ コンパクトで あることが導かれる。
公理 T、4、D、B、5、H、G（およびそれらの任意の組み合わせ）は正準です。GL と Grz はコンパクトではないため、正準ではありません。公理 M 単体では正準ではありませんが (Goldblatt、1991)、結合論理S4.1 (実際にはK4.1 も) は正準です。
一般に、与えられた公理が正準公理であるかどうかは決定不可能である。我々は良い十分条件を知っている。 ヘンリック・サールクヴィストは 、次のような広範なクラスの式（現在 サールクヴィスト式 と呼ばれている）を特定した。
サールクヴィスト式は正準であり、 サールクヴィスト式に対応するフレームのクラスは、一次 定義可能であり、 与えられたサールクヴィスト式に対応するフレーム条件を計算するアルゴリズムが存在する。 これは強力な基準です。例えば、上記で正準公理として挙げられたすべての公理は、（サールクヴィストの公式と同等です）。
有限モデル特性 論理体系が有限モデル特性 決定可能性の問題がある。 ポストの定理 によれば、 FMPを持つ再帰的に公理化された様相論理Lは、与えられた有限フレームが L のモデルであるかどうかを決定できる場合に限り、決定可能である。特に、FMPを持つ有限公理化可能な論理体系はすべて決定可能である。
与えられた論理体系に対してFMPを確立する方法は様々である。標準モデル構築の改良や拡張は、フィルタリング や アンラベリングといったツールを用いることでしばしば有効となる。また、別の可能性として、 カットフリー シーケント計算 に基づく完全性証明は、通常、有限モデルを直接生成する。
実際に使用されているモーダルシステムのほとんど（上記に挙げたものすべてを含む）はFMPを備えています。
場合によっては、FMP を用いて論理のクリプキ完全性を証明できます。すなわち、すべての正規様相論理は 様相代数 のクラスに関して完全であり、有限 様相代数はクリプキフレームに変換できます。例として、ロバート・ブルはこの方法を用いて、S4.3 のすべての正規拡張が FMP を持ち、クリプキ完全であることを証明しました。
マルチモーダルロジック クリプキ意味論は、複数の様相を持つ論理体系への直接的な一般化が可能だ。 { ◻ 私 ∣ 私 ∈ 私 } {\displaystyle \{\Box _{i}\mid \,i\in I\}} i ∈ Iに対して二項関係 R i W から構成される。充足関係の定義は次のように変更される。
w ⊩ ◻ 私 A {\displaystyle w\Vdash \Box _{i}A} ∀ u （ w R 私 u ⇒ u ⊩ A ） 。 {\displaystyle \forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A).} ティム・カールソンによって発見された簡略化された意味論は、多様体証明可能性論理 によく用いられる。カールソンモデル は構造である。 ⟨ W 、 R 、 { D 私 } 私 ∈ 私 、 ⊩ ⟩ {\displaystyle \langle W,R,\{D_{i}\}_{i\in I},\Vdash \rangle } R と部分集合 D i ⊆ W が存在する。満足度は次のように定義される。
w ⊩ ◻ 私 A {\displaystyle w\Vdash \Box _{i}A} ∀ u ∈ D 私 （ w R u ⇒ u ⊩ A ） 。 {\displaystyle \forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A).} カールソンモデルは、通常の多峰性クリプキモデルよりも視覚化しやすく、扱いやすい。ただし、カールソン不完全なクリプキ完全な多峰性論理も存在する。
直観主義論理のセマンティクス 直観主義論理 のクリプキ意味論は様相論理の意味論と同じ原理に従うが、充足の定義は異なる。
直観主義的クリプキモデル は三重構造である ⟨ W 、 ≤ 、 ⊩ ⟩ {\displaystyle \langle W,\leq ,\Vdash \rangle } ⟨ W 、 ≤ ⟩ {\displaystyle \langle W,\leq \rangle } 予約注文済みの クリプケフレームで、⊩ {\displaystyle \Vdash }
p が命題変数である場合、w ≤ u {\displaystyle w\leq u} w ⊩ p {\displaystyle w\Vdash p} u ⊩ p {\displaystyle u\Vdash p} 持続 条件（単調性 参照））w ⊩ A ∧ B {\displaystyle w\Vdash A\land B} w ⊩ A {\displaystyle w\Vdash A} w ⊩ B {\displaystyle w\Vdash B} w ⊩ A ∨ B {\displaystyle w\Vdash A\lor B} w ⊩ A {\displaystyle w\Vdash A} w ⊩ B {\displaystyle w\Vdash B} w ⊩ A → B {\displaystyle w\Vdash A\to B} u ≥ w {\displaystyle u\geq w} u ⊩ A {\displaystyle u\Vdash A} u ⊩ B {\displaystyle u\Vdash B} ないw ⊩ ⊥ {\displaystyle w\Vdash \bot } 直感的に、w ⊩ A → B {\displaystyle w\Vdash A\to B} 複合命題、つまり任意の命題A に対しても単調性を保証すること、w ≤ u {\displaystyle w\leq u} w ⊩ A {\displaystyle w\Vdash A} u ⊩ A {\displaystyle u\Vdash A} A の否定¬ Aは、 A → ⊥の略語として定義できます。すべてのuに対して w ≤ u であり、u ⊩ A でない場合、w ⊩ A → ⊥ は自明に真で あるため、w ⊩ ¬ A となります。
直観主義論理はクリプキ意味論に関して健全かつ完全であり、有限モデル特性 を持つ。
直観主義一階述語論理 L を 一階述語 論理とする。Lのクリプキモデルは、3 個の要素からなる三重構造である 。 ⟨ W 、 ≤ 、 { M w } w ∈ W ⟩ {\displaystyle \langle W,\leq ,\{M_{w}\}_{w\in W}\rangle } ⟨ W 、 ≤ ⟩ {\displaystyle \langle W,\leq \rangle } M w は各ノードw ∈ W に対して（古典的な）L構造であり、 u ≤ v の場合、次の互換性条件が成り立つ。
M u の定義域はM v の定義域に含まれる。M u とM v における関数記号の実現は、M u の要素で一致します。各n 項述語P と要素a 1 ,..., a n ∈ M u P ( a 1 ,..., a n ) がM u M v M w e が与えられたとき、満足度関係を定義します。w ⊩ A [ e ] {\displaystyle w\Vdash A[e]}
w ⊩ P （ t 1 、 … 、 t n ） [ e ] {\displaystyle w\Vdash P(t_{1},\dots ,t_{n})[e]} P （ t 1 [ e ] 、 … 、 t n [ e ] ） {\displaystyle P(t_{1}[e],\dots ,t_{n}[e])} M w で保持、w ⊩ （ A ∧ B ） [ e ] {\displaystyle w\Vdash (A\land B)[e]} w ⊩ A [ e ] {\displaystyle w\Vdash A[e]} w ⊩ B [ e ] {\displaystyle w\Vdash B[e]} w ⊩ （ A ∨ B ） [ e ] {\displaystyle w\Vdash (A\lor B)[e]} w ⊩ A [ e ] {\displaystyle w\Vdash A[e]} w ⊩ B [ e ] {\displaystyle w\Vdash B[e]} w ⊩ （ A → B ） [ e ] {\displaystyle w\Vdash (A\to B)[e]} u ≥ w {\displaystyle u\geq w} u ⊩ A [ e ] {\displaystyle u\Vdash A[e]} u ⊩ B [ e ] {\displaystyle u\Vdash B[e]} ないw ⊩ ⊥ [ e ] {\displaystyle w\Vdash \bot [e]} w ⊩ （ ∃ x A ） [ e ] {\displaystyle w\Vdash (\exists x\,A)[e]} 1 ∈ M w {\displaystyle a\in M_{w}} w ⊩ A [ e （ x → 1 ） ] {\displaystyle w\Vdash A[e(x\to a)]} w ⊩ （ ∀ x A ） [ e ] {\displaystyle w\Vdash (\forall x\,A)[e]} u ≥ w {\displaystyle u\geq w} 1 ∈ M u {\displaystyle a\in M_{u}} u ⊩ A [ e （ x → 1 ） ] {\displaystyle u\Vdash A[e(x\to a)]} ここで、e ( x → a )は xに 値a を与える評価であり、それ以外の場合はe と一致する。[ 10 ]
層理論 の独立した発展の一環として、1965 年頃に、クリプキ意味論がトポス理論 における 存在量化 の扱いと密接に関係していることが認識されました。つまり、層のセクションの存在の「局所的」側面は、「可能」の論理の一種でした。この発展は多くの人々の業績でしたが、この関連でクリプキ＝ジョヤル または単純な層意味論という 名前がよく使われます。
層意味論は、クリプキ意味論と類似のベス意味論 を統一するとともに、証明に関係のない（命題）ケースから証明に関連するケースへと拡張する。これは、アクセス可能性関係の場合に当てはまる。R {\displaystyle R} 再帰的 かつ他動詞 です。
模型製作 古典的なモデル理論 と同様に、他のモデルから新しいクリプキモデルを構築する方法が存在する。
クリプキ意味論における自然な準同型写像は p-射（ 擬全射 の略だが、後者の用語はめったに使われない）と呼ばれる 。クリプキフレームのp-射 ⟨ W 、 R ⟩ {\displaystyle \langle W,R\rangle } ⟨ W ′ 、 R ′ ⟩ {\displaystyle \langle W',R'\rangle } f : W → W ′ {\displaystyle f\colon W\to W'}
f はアクセス可能性関係を保持します。つまり、u R v は f ( u ) R' f ( v )を意味します。 f ( u ) R' v 'であるときはいつでも、 u R v かつf ( v ) = v 'となるv ∈ W が存在する。 クリプキモデルのp-射⟨ W 、 R 、 ⊩ ⟩ {\displaystyle \langle W,R,\Vdash \rangle } ⟨ W ′ 、 R ′ 、 ⊩ ′ ⟩ {\displaystyle \langle W',R',\Vdash '\rangle } f : W → W ′ {\displaystyle f\colon W\to W'}
w ⊩ p {\displaystyle w\Vdash p} f （ w ） ⊩ ′ p {\displaystyle f(w)\Vdash 'p} p に対して。P-射は特殊な双模倣 の一種である。一般に、 フレーム間の双模倣は ⟨ W 、 R ⟩ {\displaystyle \langle W,R\rangle } ⟨ W ′ 、 R ′ ⟩ {\displaystyle \langle W',R'\rangle } B ⊆ W × W'である。
u B u' かつu R v の場合、 v B v' かつu' R' v' となるv' ∈ W' が存在する。 u B u' かつu' R' v' の場合、 v B v' かつu R v となるようなv ∈ W が存在する。 原子式 の強制性を維持するためには、モデルの双模倣がさらに必要となる。
w B w' の場合、w ⊩ p {\displaystyle w\Vdash p} w ′ ⊩ ′ p {\displaystyle w'\Vdash 'p} p に対して。この定義から導かれる重要な特性は、モデルの双模倣（したがってp-射も）は、命題変数だけでなく、すべての論理式の充足性を保持するということである。
アンラベリング を用いることで、 クリプキモデルをツリー に変換できます。⟨ W 、 R 、 ⊩ ⟩ {\displaystyle \langle W,R,\Vdash \rangle } w 0 ∈ W でモデルを定義します ⟨ W ′ 、 R ′ 、 ⊩ ′ ⟩ {\displaystyle \langle W',R',\Vdash '\rangle } W' はすべての有限数列の集合である。 s = ⟨ w 0 、 w 1 、 … 、 w n ⟩ {\displaystyle s=\langle w_{0},w_{1},\dots ,w_{n}\rangle } すべてのi < n に対して w i R w i+1 であり、 s ⊩ ′ p {\displaystyle s\Vdash 'p} w n ⊩ p {\displaystyle w_{n}\Vdash p} pの場合。アクセス可能性関係 R' の定義は 様々です。最も単純なケースでは、次のようにします。
⟨ w 0 、 w 1 、 … 、 w n ⟩ R ′ ⟨ w 0 、 w 1 、 … 、 w n 、 w n + 1 ⟩ {\displaystyle \langle w_{0},w_{1},\dots ,w_{n}\rangle \;R'\;\langle w_{0},w_{1},\dots ,w_{n},w_{n+1}\rangle } しかし、多くのアプリケーションでは、この関係の反射閉包や推移閉包、あるいは同様の修正が必要となる。
フィルタリングは 、多くの論理のFMPを 証明するために使用できる有用な構成です。Xを 部分式を取る操作で閉じている式の集合とします。モデルのXフィルタリング ⟨ W 、 R 、 ⊩ ⟩ {\displaystyle \langle W,R,\Vdash \rangle } W からモデルへの 写像f ⟨ W ′ 、 R ′ 、 ⊩ ′ ⟩ {\displaystyle \langle W',R',\Vdash '\rangle }
fは 全射で ある。f はアクセス可能性関係を保持し、（両方向で）変数p ∈ X の充足、 f ( u ) R'f ( v )の場合、 u ⊩ ◻ A {\displaystyle u\Vdash \Box A} ◻ A ∈ X {\displaystyle \Box A\in X} v ⊩ A {\displaystyle v\Vdash A} したがって、f は X からのすべての式の充足性を保持する 。典型的な応用では、 f を 関係式上のW の商 への射影として扱う。
u ≡ X vは、すべての A ∈ X に対して、 u ⊩ A {\displaystyle u\Vdash A} v ⊩ A {\displaystyle v\Vdash A} 展開の場合と同様に、商におけるアクセス可能性関係の定義は変化する。
一般フレーム意味論 クリプキ意味論の主な欠点は、クリプキ不完全論理と、完全ではあるがコンパクトではない論理が存在することである。これは、代数意味論の考え方を用いて、可能な値集合を制限する追加構造をクリプキフレームに与えることで解決できる。これにより、一般フレーム 意味論が生まれる。
コンピュータサイエンスの応用 ブラックバーンら（2001）は、関係構造は単に集合とその集合上の関係の集合を組み合わせたものであるため、関係構造が頻繁に見られるのは当然であると主張している。理論計算機科学 プログラム実行を モデル化するラベル付き遷移システム を挙げている。ブラックバーンらは、この関連性から、様相言語は「関係構造に関する内部的、局所的な視点」を提供するのに理想的であると主張している。（p. xii）
歴史と用語 クリプキの革命的な意味論的ブレークスルーに先立つ同様の研究:
ルドルフ・カルナップは、評価関数にライプニッツの可能世界を網羅するパラメータを与えることによって、必然性と可能性の様相に 可能世界意味論 を与えることができるという考えを最初に提唱した人物であると思われる。バヤールはこの考えをさらに発展させたが、タルスキが導入したような満足の再帰的な定義はどちらも与えなかった。JCC McKinseyとAlfred Tarskiは 、現代の研究においても影響力のある様相論理のモデリング手法、すなわち演算子付きブール代数をモデルとして用いる代数的手法を開発した。Bjarni Jónsson とTarskiは、演算子付きブール代数がフレームによって表現可能であることを実証した。もしこの二つのアイデアが結びついていれば、まさにフレームモデル、つまりKripkeモデルが、Kripkeよりも何年も前に実現していたはずである。しかし、当時、誰も（Tarski自身でさえも）その関連性に気づかなかった。 アーサー・プライアーは、 C・A・メレディス の未発表の研究に基づいて、文様相論理を古典述語論理に翻訳する手法を開発した。もし彼がそれを後者の通常のモデル理論と組み合わせていれば、前者のクリプキモデルと同等のモデル理論が得られたであろう。しかし、彼のアプローチは断固として構文論的であり、反モデル理論的なものであった。スティグ・カンガーは 様相論理の解釈に関して、クリプキのアプローチよりもやや複雑な手法を提示したが、そこにはクリプキの手法の重要なアイデアが数多く含まれていた。彼はまず、到達可能性関係に関する条件と、様相論理におけるルイス 型の公理との関係性を指摘した。しかし、カンガーは自身の体系の完全性証明を与えることはできなかった。ヤーッコ・ヒンティッカは、 認識論理を導入した論文の中で、クリプキの意味論の単純な変形である意味論を与えた。これは、最大整合集合による評価の特徴付けに相当する。彼は認識論理の推論規則を与えていないため、完全性の証明を与えることはできない。リチャード・モンタギューは クリプキの研究に含まれる多くの重要なアイデアを持っていたが、完全性の証明がなかったため、それらを重要視せず、クリプキの論文が論理学界でセンセーションを巻き起こすまで発表しなかった。エバート・ウィレム・ベスは、 ツリーに基づいた直観主義論理のセマンティクスを提示した。これは、充足の定義がより煩雑である点を除けば、クリプキのセマンティクスとよく似ている。
注記 ↑ 可能世界意味論は、クリプキ意味論を含むさまざまなアプローチを包含するより広い用語です。一般的には、異なる命題が真または偽となる代替可能世界を考慮することによって様相命題を分析するという考え方を指します。クリプキ意味論は可能世界意味論の特定のタイプですが、可能世界とその関係をモデル化する他の方法もあります。クリプキ意味論は、様相論理における可能世界と命題の関係を表すために関係構造を使用する、可能世界意味論の特定の形式です。 ↑ クリプキ意味論における様相論理の「モデル」の 概念 は、古典的な非様相論理における「モデル」の概念とは異なること に 注意してください。古典論理では、ある式F の変数の何らかの「解釈」が存在し、それによって式 F が真になる場合、その式 F は「モデル」 を持つと 言います。この特定の解釈は、式 F のモデル です 。対照的に、クリプキ意味論における様相論理では、「モデル」は特定の様相式を真にする特定の「何か」ではありません。クリプキ意味論では、「モデル」はむしろ、 あらゆる 様相式が意味を持って「理解」されることのできる、より大きな議論の世界 として理解されなければなりません。つまり、古典的な非様相論理における「モデルを持つ」という概念は、その論理内の個々の論理式を指すのに対し、様相論理における「モデルを持つ」という概念は、論理 全体 （すなわち、その公理と演繹規則の体系全体）を指す ↑ アンジェイ・グジェゴルチク の後。 ↑ ブーロス、ジョージ (1993). 『証明可能性の論理 』ケンブリッジ大学出版局、 148、149頁。ISBN 0-521-43342-8 。 ↑ モスコヴァキス（2022） の若干異なる形式化を参照
参考文献 ブラックバーン、P.デ・ライケ、M. ;ベネマ、イデ (2002)。モーダルロジック 。ケンブリッジ大学出版局。ISBN 978-1-316-10195-7 。 Bull, Robert A.; Segerberg, K. (2012) [1984]. "基本様相論理" . Gabbay, DM; Guenthner, F. (編) 『古典論理の拡張』 .『哲学論理ハンドブック』第 2巻. Springer. pp. 1–88 . ISBN 978-94-009-6259-0 。 チャグロフ、A.ザハリヤシェフ、M. (1997)。モーダルロジック 。クラレンドンプレス。ISBN 978-0-19-853779-3 。 Cresswell, MJ ; Hughes, GE (2012) [1996]. A New Introduction to Modal Logic . Routledge. ISBN 978-1-134-80028-5 。ヴァン・ダーレン、ダーク （2013）[1986] 「直観主義論理」。ガベイ、ドヴ・M、ギュントナー、フランツ編『古典論理の代替 』哲学論理学ハンドブック第 3巻、シュプリンガー、225-339頁 。ISBN 978-94-009-5203-4 。ダメット、マイケル・A・E （2000）。直観主義の要素 （第2 版）。クラレンドン・プレス。ISBN 978-0-19-850524-2 。フィッティング、メルビン （1969）。直観主義論理、モデル理論、強制法 。ISBN 978-0-444-53418-7 。ガスケ、オリヴィエ。ヘルツィヒ、アンドレアス。ビラルは言った。シュワルツェントルーバー、フランソワ (2013)。Kripke's Worlds: An Introduction to Modal Logics via Tableaux 。スプリンガー。ページXV 、198。ISBN 978-3764385033 2014年12月24日 に取得 。 ジャキント、マーカス（2002）。『確実性の探求 ：数学の基礎に関する哲学的考察 』オックスフォード大学出版局、 256ページ。ISBN 019875244X 2014年12月24日 に取得 。 Goldblatt, Robert (2006a). 「数学的様相論理：その進化の概観」（PDF） 。Gabbay, Dov M.、Woods , John (編)『20世紀の論理と様相』 （PDF） 。論理学史ハンドブック第 7巻。Elsevier。pp. 1–98。ISBN 978-0-08-046303-2 。Goldblatt, Robert (2006b). "量子論理における非可換論理のためのクリプキ＝ジョヤル意味論" (PDF) . Governatori, G.; Hodkinson, I.; Venema, Y. (編) 『様相論理の進歩 』第 6巻. ロンドン: College Publications. pp. 209–225 . ISBN 1904987206 。Mac Lane, Saunders ; Moerdijk, Ieke (2012) [1991]. Sheaves in Geometry and Logic: A First Introduction to Topos Theory . Springer. ISBN 978-1-4612-0927-0 。ショハム、ヨアブ；レイトン＝ブラウン、ケビン（2008）。マルチエージェントシステム：アルゴリズム的、ゲーム理論的、論理的基礎 。ケンブリッジ大学出版局。397 ページ。ISBN 978-0521899437 。 シンプソン、アレックス K. (1994).直観主義様相論理の証明論と意味論 (学位論文).エジンバラ研究アーカイブ (ERA) . hdl : 1842/407 . ストックホフ、マーティン（2008）。「意味のアーキテクチャ：ウィトゲンシュタインの論理哲学論考 と形式意味論」。エドアルド・ザムナー、デイヴィッド・K・レヴィ編『ウィトゲンシュタインの不朽の議論』 所収。ロンドン：ラウトレッジ。211-244 頁。ISBN 9781134107070 。 Troelstra, AS ; van Dalen, D. (1988).数学における構成 主義：入門、第 1 巻 。論理学と数学の基礎に関する研究。第 121 巻。アムステルダム：North-Holland。ISBN 9780444702661 。
![{\displaystyle \Box [(A\to B)\land A]\to \Box B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0bb5446fefa7edfe8c494e8beae2661c2c2b956f)
![{\displaystyle w\Vdash A[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5904096a35806f2c02953bb68ba19d017bcaf1e9)
![{\displaystyle w\Vdash P(t_{1},\dots ,t_{n})[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8bed6a4398de6219b9869cde647174b79751084c)
![{\displaystyle P(t_{1}[e],\dots ,t_{n}[e])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f044e919c1699f3912aa10e901576f7edf998dc0)
![{\displaystyle w\Vdash (A\land B)[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/59c38161da49f139a1f966606cb046c16d837180)
![{\displaystyle w\Vdash B[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2ec4262aadbaddbbbd29208e26a2887915fb5ef0)
![{\displaystyle w\Vdash (A\lor B)[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a84898302d45c20f4f6db6c50d572916d3942341)
![{\displaystyle w\Vdash (A\to B)[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/78199ffd20d1c1697171cc8732fba8055f6a218b)
![{\displaystyle u\Vdash A[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8f26512eec2a9afbb76fb5bf0c851aae40852d3b)
![{\displaystyle u\Vdash B[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f3f80feb5d37d28d4f3f8fa9f48e714912720dea)
![{\displaystyle w\Vdash \bot [e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/681489a81096035bc73737762cffddc0248b86e9)
![{\displaystyle w\Vdash (\exists x\,A)[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c9e280fc19d6459dd2f63e61ff5f3bfe780a0c8e)
![{\displaystyle w\Vdash A[e(x\to a)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/35cfa78009e8ef4f2e7fd55829fe5068f492b2ba)
![{\displaystyle w\Vdash (\forall x\,A)[e]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/58f4621d5c02e76efb59d112699bbe7ce8aaae5c)
![{\displaystyle u\Vdash A[e(x\to a)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/741627df2ff936ce2f77b245fc160a7bca31678d)
