クリプキ意味論

クリプキ意味論（関係意味論またはフレーム意味論とも呼ばれ、可能世界意味論と混同されることが多い）^[1]は、 1950年代後半から1960年代前半にかけてソール・クリプキとアンドレ・ジョイヤールによって考案された非古典的論理システムの形式意味論である。最初は様相論理のために考案され、後に直観主義論理やその他の非古典的システムに適応された。クリプキ意味論の発展は非古典的論理の理論における画期的な進歩であった。なぜなら、そのような論理のモデル理論はクリプキ以前にはほとんど存在しなかったからである（代数的意味論は存在したが、「偽装された統語論」と考えられていた）。

命題様相論理の言語は、命題変数の可算無限集合、真理関数接続子の集合（本稿および）、および様相演算子（「必然的に」）から構成される。様相演算子（「おそらく」）は（古典的には）の双対であり、次のように必然性の観点から定義することができる。 （「おそらくA」は「必ずしもAではない」と同等であると定義される。）^[2]${\displaystyle \to}$${\displaystyle \neg}$${\displaystyle \Box}$${\displaystyle \Diamond }$${\displaystyle \Box}$${\displaystyle \Diamond A:=\neg \Box \neg A}$

クリプキフレームまたは様相フレームは、Wが（空の可能性のある）集合であり、RがW上の二項関係であるペアです。Wの要素はノードまたは世界と呼ばれ、R はアクセス可能性関係として知られています。^[3]${\displaystyle \langle W,R\rangle }$

クリプキモデルは3つ組^[4]であり、は クリプキフレーム、はWのノードと様相式の関係であり、すべてのw∈W と 様相式AおよびBに対して次の関係が成り立つ。 ${\displaystyle \langle W,R,\Vdash \rangle }$${\displaystyle \langle W,R\rangle }$${\displaystyle \Vdash}$

• ${\displaystyle w\Vdash \neg A}$の場合に限り、${\displaystyle w\nVdash A}$
• ${\displaystyle w\Vdash A\to B}$またはの場合に限り、${\displaystyle w\nVdash A}$${\displaystyle w\Vdash B}$
• ${\displaystyle w\Vdash \Box A}$となるすべての に対してである場合に限ります。${\displaystyle u\Vdash A}$${\displaystyle u}$${\displaystyle w\;R\;u}$

「w はA を満たす 」、「Aはwで満たされる」、「w はA を強制する」と読みます。この関係は、満足関係、評価、または強制関係と呼ばれます 。満足関係は、命題変数の値によって一意に決定されます。 ${\displaystyle w\Vdash A}$${\displaystyle \Vdash}$

式A は次の場合に有効です。

• モデルでは、すべてのw  ∈  Wに対して、${\displaystyle \langle W,R,\Vdash \rangle }$${\displaystyle w\Vdash A}$
• フレーム がのすべての可能な選択肢に対してで有効である場合、${\displaystyle \langle W,R\rangle }$${\displaystyle \langle W,R,\Vdash \rangle }$${\displaystyle \Vdash}$
• フレームまたはモデルのクラスC （ Cのすべてのメンバーで有効である場合） 。

Thm( C ) をCで有効なすべての式の集合として 定義します。逆に、X が式の集合である場合、 Mod( X ) をXのすべての式を検証するすべてのフレームのクラスとします。

様相論理（つまり、式の集合）L は、 L  ⊆ Thm( C )であれば、フレームのクラスCに関して健全です。L  ⊇ Thm( C )であれば、L はCに関して完全です 。

意味論は、意味的帰結関係がその統語的対応物である統語的帰結関係（導出可能性）を反映している場合にのみ、論理（すなわち導出システム）を調査するのに役立ちます。 ^[5]クリプキフレームのクラスに関してどの様相論理が健全で完全であるかを知ること、またそれがどのクラスであるかを決定することは非常に重要です。

クリプキフレームの任意のクラスCに対して、Thm( C ) は正規様相論理です(特に、最小正規様相論理Kの定理は、すべてのクリプキモデルで有効です)。ただし、逆は一般には成り立ちません。研究されている様相システムのほとんどは、単純な条件で記述されるフレームのクラスが完全であるのに対し、クリプキ不完全正規様相論理は存在します。そのようなシステムの自然な例としては、ジャパリゼの多様相論理があります。

通常の様相論理L は、 C  = Mod( L )の場合、フレームのクラスCに対応します。言い換えると、C は、 L がCに関して健全であるフレームの最大のクラスです。したがって、 Lが対応するクラスに対して完全である場合に限り、 L はクリプキ完全になります。

スキーマT  :について考えます。 T は任意の反射フレームで有効です。 の場合、w R w であるためです。一方、T を検証するフレームは反射的でなければなりません。w  ∈  Wを固定し、命題変数pの充足度を次のように定義します。 w R uの場合に限ります。すると となり、T によって、の定義を使用して w R wを意味します。T は反射クリプキ フレームのクラスに対応します。 ${\displaystyle \Box A\to A}$${\displaystyle \langle W,R\rangle }$${\displaystyle w\Vdash \Box A}$${\displaystyle w\Vdash A}$  ${\displaystyle u\Vdash p}$  ${\displaystyle w\Vdash \Box p}$${\displaystyle w\Vdash p}$  ${\displaystyle \Vdash}$

Lの対応するクラスを特徴付ける方が、その完全性を証明するよりもはるかに簡単な場合が多いため_、対応は完全性証明のガイドとして役立ちます。対応は様相論理の不完全性を示すためにも使用されます。L 1  ⊆  L ₂が同じクラスのフレームに対応する通常の様相論理であるが、L _{1 が}L ₂のすべての定理を証明していないとします。その場合、 L ₁はクリプキ不完全です。たとえば、スキーマはGLと同じクラスのフレーム (つまり、推移的および逆の well-founded フレーム) に対応するため不完全な論理を生成しますが、 GLトートロジーは証明しません。 ${\displaystyle \Box (A\leftrightarrow \Box A)\to \Box A}$${\displaystyle \Box A\to \Box \Box A}$

次の表は、一般的な様相公理とそれに対応するクラスを示しています。公理の名前は多くの場合異なります。ここで、公理KはSaul Kripkeにちなんで名付けられています。公理T は認識論的論理の真理公理にちなんで名付けられています。公理D は義務論的論理にちなんで名付けられています。公理BはLEJ Brouwerにちなんで名付けられています。公理4と5 は、 CI Lewisの記号論理システムの番号付けに基づいて名付けられています。

公理Kは と書き直すこともでき、これはあらゆる可能世界における 推論規則としてmodus ponens を論理的に確立します。${\displaystyle \Box [(A\to B)\land A]\to \Box B}$

公理Dの場合、 は暗黙的に を意味し、これはモデル内のすべての可能世界に対して、そこからアクセス可能な可能世界が少なくとも 1 つ存在することを意味します (それ自体である可能性もあります)。この暗黙的な含意は、存在量指定子による量化 の範囲への暗黙的な含意に似ています。 ${\displaystyle \Diamond A}$${\displaystyle \Diamond \top }$${\displaystyle \Diamond A\rightarrow \Diamond \top }$

次の表には、一般的な通常モード システムのいくつかがリストされています。一部のシステムのフレーム条件は簡略化されています。表に示されているフレーム クラスに関しては、ロジックは健全かつ完全ですが、より大きなクラスのフレームに対応している可能性があります。

任意の通常の様相論理Lに対して、最大無矛盾集合をモデルとして使用する標準的な手法を適応させることにより、Lの非定理を正確に反証する クリプキモデル（標準モデルと呼ばれる）を構築できます。標準クリプキモデルは、代数的意味論におけるリンデンバウム-タルスキ代数構成と同様の役割を果たします。

式の集合は、 L の定理と Modus Ponens を使って矛盾を導き出せない場合は L 整合です。最大L整合集合(略して L - MCS) は、適切なL整合スーパーセットを持たないL整合集合です。

Lの標準モデルはクリプキモデルであり 、W はすべてのL - MCSの集合であり、関係Rとは次のようになります。 ${\displaystyle \langle W,R,\Vdash \rangle }$${\displaystyle \Vdash }$

${\displaystyle X\;R\;Y}$任意の式 に対して の場合に限り、の場合、${\displaystyle A}$${\displaystyle \Box A\in X}$${\displaystyle A\in Y}$

${\displaystyle X\Vdash A}$の場合に限ります。${\displaystyle A\in X}$

標準モデルはLのモデルであり、すべてのL - MCSにはLのすべての定理が含まれます。ゾルンの補題により、各L整合集合はL - MCSに含まれ、特にLで証明できないすべての式には標準モデルに反例があります。

正準モデルの主な応用は完全性の証明です。 Kの正準モデルの特性は、すべてのクリプキフレームのクラスに関してKが完全であることを直ちに意味します。 この議論は任意のLには当てはまりません。なぜなら、正準モデルの基になるフレームがLのフレーム条件を満たすという保証がないからです。

式または式の集合Xがクリプキフレームの性質P に関して正準であるとは、

• XはPを満たすすべてのフレームで有効であり、
• X を含む任意の通常の様相論理Lに対して、 Lの標準モデルの基礎となるフレームはP を満たします。

正規の式集合の和集合は、それ自体が正規です。これまでの議論から、正規の式集合によって公理化された論理は、クリプキ完全かつ コンパクトであることがわかります。

公理 T、4、D、B、5、H、G (およびそれらの任意の組み合わせ) は標準です。GL と Grz はコンパクトではないため標準ではありません。公理 M 自体は標準ではありません (Goldblatt、1991) が、組み合わせた論理S4.1 (実際にはK4.1も) は標準です。

一般に、与えられた公理が正準であるかどうかは決定できない。我々は良い十分条件を知っている。ヘンリク・サールクヴィストは、次のような幅広いクラスの式（現在 サールクヴィスト式と呼ばれる） を特定した。

• サールクヴィストの公式は標準的である。
• サールクヴィストの公式に対応するフレームのクラスは一階で定義可能である。
• 与えられた Sahlqvist 式に対応するフレーム条件を計算するアルゴリズムがあります。

これは強力な基準です。たとえば、上記で標準としてリストされているすべての公理は、Sahlqvist の公式と同等です。

論理が有限モデル特性(FMP) を持つとは、有限フレームのクラスに関して完全であることを意味します。この概念の応用は決定可能性の問題です。ポストの定理から、与えられた有限フレームが L のモデルであるかどうかが決定可能である限り、 FMP を持つ再帰的に公理化され た様相論理L は決定可能であることがわかります。特に、 FMP を持つ有限に公理化可能な論理はすべて決定可能です。

特定のロジックに対して FMP を確立する方法はさまざまです。フィルタリングやアンラベリングなどのツールを使用した標準モデル構築の改良と拡張は、多くの場合機能します。別の可能性として、カットフリー シーケント計算に基づく完全性証明は通常、直接有限モデルを生成します。

実際に使用されているモーダル システムのほとんど (上記のすべてを含む) には FMP があります。

場合によっては、FMP を使用して論理のクリプキ完全性を証明できます。つまり、すべての通常の様相論理は 様相代数のクラスに関して完全であり、有限様相代数はクリプキ フレームに変換できます。例として、ロバート ブルはこの方法を使用して、S4.3のすべての通常の拡張にはFMP があり、クリプキ完全であることを証明しました。

クリプキ意味論は、複数の様相を持つ論理に簡単に一般化できます。 を その必然性演算子の集合として持つ言語のクリプキフレームは、各i  ∈  Iに対して二項関係 R _iを備えた空でない集合Wで構成されます。 満足関係の定義は次のように変更されます。 ${\displaystyle \{\Box _{i}\mid \,i\in I\}}$

${\displaystyle w\Vdash \Box _{i}A}$もし、もし、${\displaystyle \forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A).}$

ティム・カールソンによって発見された単純化された意味論は、多様相証明論理によく使われる。カールソンモデルは、 単一のアクセス関係Rと、各様相のサブセット D _i  ⊆  W を持つ構造である 。満足度は次のように定義される。 ${\displaystyle \langle W,R,\{D_{i}\}_{i\in I},\Vdash \rangle }$

${\displaystyle w\Vdash \Box _{i}A}$もし、もし、${\displaystyle \forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A).}$

カールソン モデルは、通常の多様相クリプキ モデルよりも視覚化や操作が簡単です。ただし、カールソン不完全であるクリプキ完全多様相論理も存在します。

直観主義論理のクリプキ意味論は様相論理の意味論と同じ原理に従いますが、満足度の定義が異なります。

直観主義クリプキモデルは三つ組であり 、 は順序付きクリプキフレームであり、以下の条件を満たす: ^[8]${\displaystyle \langle W,\leq ,\Vdash \rangle }$${\displaystyle \langle W,\leq \rangle }$${\displaystyle \Vdash }$

• pが命題変数、、の場合、(持続条件(cf.単調性))、${\displaystyle w\leq u}$${\displaystyle w\Vdash p}$${\displaystyle u\Vdash p}$
• ${\displaystyle w\Vdash A\land B}$かつの場合に限り、${\displaystyle w\Vdash A}$${\displaystyle w\Vdash B}$
• ${\displaystyle w\Vdash A\lor B}$またはの場合に限り、${\displaystyle w\Vdash A}$${\displaystyle w\Vdash B}$
• ${\displaystyle w\Vdash A\to B}$全ての に対して が成り立つ場合、かつその場合に限り、が成り立つ。${\displaystyle u\geq w}$${\displaystyle u\Vdash A}$${\displaystyle u\Vdash B}$
• ない。${\displaystyle w\Vdash \bot }$

Aの否定¬ Aは、 A → ⊥の省略形として定義できます。w ≤ uとなるすべてのuに対してu ⊩ Aでない場合、w ⊩ A → ⊥ は空虚に真であるため、w ⊩ ¬ Aとなります。

直観主義論理はクリプキ意味論に関して健全かつ完全であり、有限モデル特性を持ちます。

L を一階言語とする。Lのクリプキモデルは三つ組 であり 、 は 直観主義クリプキフレーム、M _{w は}各ノードw  ∈  Wの（古典的な）L構造であり、u  ≤  vの場合は常に次の互換性条件が成り立つ。 ${\displaystyle \langle W,\leq ,\{M_{w}\}_{w\in W}\rangle }$${\displaystyle \langle W,\leq \rangle }$

• M _uの領域はM _vの領域に含まれる。
• M _uとM _vにおける関数記号の実現はM _uの要素と一致する。
• 各n項述語Pと要素a ₁ ,..., a _n  ∈  M _uについて、P ( a ₁ ,..., a _n ) がM _uで成り立つ場合、 M _vでも成り立ちます。

M _wの要素による変数の評価eが与えられた場合、満足度関係を定義します。 ${\displaystyle w\Vdash A[e]}$

• ${\displaystyle w\Vdash P(t_{1},\dots ,t_{n})[e]}$M _wにおいて成立する場合に限り、${\displaystyle P(t_{1}[e],\dots ,t_{n}[e])}$
• ${\displaystyle w\Vdash (A\land B)[e]}$かつの場合に限り、${\displaystyle w\Vdash A[e]}$${\displaystyle w\Vdash B[e]}$
• ${\displaystyle w\Vdash (A\lor B)[e]}$またはの場合に限り、${\displaystyle w\Vdash A[e]}$${\displaystyle w\Vdash B[e]}$
• ${\displaystyle w\Vdash (A\to B)[e]}$全ての に対して が成り立つ場合、かつその場合に限り、が成り立つ。${\displaystyle u\geq w}$${\displaystyle u\Vdash A[e]}$${\displaystyle u\Vdash B[e]}$
• ない、${\displaystyle w\Vdash \bot [e]}$
• ${\displaystyle w\Vdash (\exists x\,A)[e]}$が存在する場合に限り、${\displaystyle a\in M_{w}}$${\displaystyle w\Vdash A[e(x\to a)]}$
• ${\displaystyle w\Vdash (\forall x\,A)[e]}$あらゆるに対して である場合に限り、 となります。${\displaystyle u\geq w}$${\displaystyle a\in M_{u}}$${\displaystyle u\Vdash A[e(x\to a)]}$

ここでe ( x → a )はxに値aを与える評価であり、それ以外はeと一致する。^[9]

層理論の独立した発展の一環として、1965年頃にクリプキ意味論がトポス理論における 存在量化の扱いと密接に関係していることが認識されました。^[10]つまり、層のセクションの存在の「ローカル」側面は、一種の「可能」の論理でした。この発展は多くの人々の仕事でしたが、これに関連してクリプキ-ジョイアル意味論という名前がよく使用されます。

古典的なモデル理論と同様に、他のモデルから新しいクリプキモデルを構築する方法があります。

クリプキ意味論における自然準同型はp-写像と呼ばれる （これは擬似エピモーフィズムの略だが、後者の用語はあまり使われない）。クリプキフレームのp-写像は 、次のような 写像である 。${\displaystyle \langle W,R\rangle }$${\displaystyle \langle W',R'\rangle }$${\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-射とは その基礎となるフレームのp-射であり、次式を満たす。 ${\displaystyle \langle W,R,\Vdash \rangle }$${\displaystyle \langle W',R',\Vdash '\rangle }$${\displaystyle f\colon W\to W'}$

${\displaystyle w\Vdash p}$任意の命題変数pに対して の場合に限ります。${\displaystyle f(w)\Vdash 'p}$

P-モルフィズムは特別な種類の双模倣です。一般に、 フレームと 間の双模倣は関係 B ⊆ W × W'であり、次の「ジグザグ」特性を満たします。 ${\displaystyle \langle W,R\rangle }$${\displaystyle \langle W',R'\rangle }$

• 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'ならば、任意の命題変数pに対してが成り立つこと、また が成り立つことに限ります。${\displaystyle w\Vdash p}$${\displaystyle w'\Vdash 'p}$

この定義から導かれる重要な特性は、モデルの双模倣（したがって p モルフィズム）が命題変数だけでなく すべての式の満足性を保持することです。

クリプキモデルは、アンラベリングを使って ツリーに変換できます。モデルと固定ノードw ₀  ∈  Wが与えられた場合、モデルを定義します 。ここで、W'は、すべての i  <  nに対してw _i  R w _i+1であり、命題変数 pに対してである 必要条件を満たすすべての有限シーケンスの集合です 。アクセス関係R'の定義は さまざまですが、最も単純なケースでは、次のように定義します 。${\displaystyle \langle W,R,\Vdash \rangle }$${\displaystyle \langle W',R',\Vdash '\rangle }$${\displaystyle s=\langle w_{0},w_{1},\dots ,w_{n}\rangle }$${\displaystyle s\Vdash p}$${\displaystyle w_{n}\Vdash p}$

${\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からモデルへの 写像fであり、 ${\displaystyle \langle W,R,\Vdash \rangle }$${\displaystyle \langle W',R',\Vdash '\rangle }$

• fは全射であり、
• f はアクセス可能性関係を保存し、（両方向で）変数p  ∈  Xの満足を維持する。
• f ( u )  R'  f ( v ) かつ （ただし ）であれば、となります。${\displaystyle u\Vdash \Box A}$${\displaystyle \Box A\in X}$${\displaystyle v\Vdash A}$

すると、f はXからのすべての式の充足度を保存する 。典型的な応用では、 f を関係式 Wの商への射影としてとらえる。

u ≡ _X  vであるべきとき、またその場合のみ、すべてのA  ∈  Xに対して であるべきとき、またその場合のみ。${\displaystyle u\Vdash A}$${\displaystyle v\Vdash A}$

解き明かしの場合と同様に、商のアクセス可能性関係の定義は変化します。

クリプキ意味論の主な欠陥は、クリプキ不完全論理、および完全だがコンパクトではない論理が存在することです。代数的意味論のアイデアを使用して、クリプキフレームに可能な値のセットを制限する追加の構造を装備することで、これを修正できます。これにより、一般的なフレーム意味論が生まれます。

Blackburn ら (2001) は、関係構造は単に集合とその集合上の関係の集合であるので、関係構造があらゆるところに見られるのは驚くことではないと指摘しています。理論計算機科学の例として、彼らはプログラム実行をモデル化するラベル付き遷移システムを挙げています。Blackburn らは、この関係性から、様相言語は「関係構造に対する内部的かつ局所的な視点」を提供するのに最適であると主張しています (p. xii)。

クリプキの革命的な意味論的ブレークスルーに先立つ同様の研究: ^[11]

• ルドルフ・カルナップは、評価関数にライプニッツの可能世界にわたるパラメータを与えることによって、必然性と可能性の様相に可能世界意味論を与えることができるという考えを最初に思いついた人物のようだ。バヤートはこの考えをさらに発展させたが、どちらもタルスキが導入したスタイルで満足度の再帰的な定義を与えなかった。
• JCC マッキンゼーとアルフレッド タルスキは、様相論理をモデル化するアプローチを開発しました。これは現代の研究でも依然として影響力を持っています。つまり、演算子を持つブール代数をモデルとして使用する代数的アプローチです。ビャルニ ヨンソンとタルスキは、演算子を持つブール代数のフレームによる表現可能性を確立しました。この 2 つのアイデアを組み合わせれば、クリプキより何年も前に、まさにフレーム モデル、つまりクリプキ モデルが誕生したでしょう。しかし、当時は誰も (タルスキでさえも) その関連性に気づきませんでした。
• アーサー・プライアは、 CAメレディスの未発表の研究を基に、文様論理から古典的な述語論理への翻訳を開発した。これを後者の通常のモデル理論と組み合わせれば、前者のクリプキモデルと同等のモデル理論が生み出されたであろう。しかし、彼のアプローチは断固として統語論的であり、反モデル理論的であった。
• スティグ・カンガーは様相論理の解釈に対して、より複雑なアプローチを示したが、それはクリプキのアプローチの重要なアイデアの多くを含んでいる。彼はまず、アクセス可能性関係の条件と様相論理のルイススタイルの公理との関係に注目した。しかし、カンガーは彼のシステムの完全性証明を与えることができなかった。
• ヤッコ・ヒンティッカは、クリプキの意味論の単純なバリエーションである認識論的論理を導入した論文で意味論を提示しました。これは、最大整合集合による値の特徴付けと同等です。彼は認識論的論理の推論規則を提示していないため、完全性の証明はできません。
• リチャード・モンタギューはクリプキの著作に含まれる重要なアイデアの多くを持っていたが、完全性の証明がなかったためそれらを重要だとは考えず、クリプキの論文が論理学界でセンセーションを巻き起こすまで出版しなかった。
• Evert Willem Beth は、満足度のより面倒な定義を使用することを除けば、Kripke 意味論に非常によく似た、ツリーに基づく直観主義論理の意味論を提示しました。

• アレクサンドロフ位相幾何学
• 通常様相論理
• 二次元主義
• 泥だらけの子供たちのパズル

• ブラックバーン、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。
• クレスウェル、MJ ;ヒューズ、GE (2012) [1996]。様相論理への新入門。ラウトレッジ。ISBN 978-1-134-80028-5。
• Van Dalen, Dirk (2013) [1986]. 「直観主義論理」。Gabbay, Dov M.、Guenthner, Franz (編)。古典論理の代替案。哲学論理ハンドブック。第3巻。Springer。pp. 225–339。ISBN 978-94-009-5203-4。
• ダメット、マイケル AE (2000)。『直観主義の要素』（第 2 版）。クラレンドン プレス。ISBN 978-0-19-850524-2。
• フィッティング、メルビン（1969年）。直観主義論理、モデル理論および強制。ノースホランド。ISBN 978-0-444-53418-7。
• ガスケ、オリヴィエ。ヘルツィヒ、アンドレアス。ビラルは言った。シュワルツェントルーバー、フランソワ (2013)。クリプキの世界: 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)。「Quantales における非可換論理の Kripke-Joyal 意味論」(PDF)。Governatori, G.、Hodkinson, I.、Venema, Y. (編)。Advances in Modal Logic。第 6 巻。ロンドン: College Publications。pp. 209–225。ISBN 1904987206。
• マック・レーン、サンダース、モーダイク、イエケ（2012）[1991]。幾何学と論理における層：トポス理論への最初の入門。シュプリンガー。ISBN 978-1-4612-0927-0。
• ショーハム、ヨアブ、レイトンブラウン、ケビン (2008)。マルチエージェントシステム：アルゴリズム、ゲーム理論、論理的基礎。ケンブリッジ大学出版局。p. 397。ISBN 978-0521899437。
• シンプソン、アレックス (1994)。直観主義様相論理の証明理論と意味論 (論文)。エディンバラ研究アーカイブ (ERA)。
• ストクホフ、マーティン (2008)。「意味のアーキテクチャ: ウィトゲンシュタインの論理哲学論考と形式意味論」。ザムナー、エドアルド、レヴィ、デイヴィッド K. (編)。ウィトゲンシュタインの不朽の議論。ロンドン: ラウトレッジ。211～244 ページ。ISBN 9781134107070。

ウィキメディア・コモンズには、クリプキモデルに関連するメディアがあります。

• Burgess, John P. 「Kripke モデル」。2004 年 10 月 20 日のオリジナルからアーカイブ。
• Detlovs, V.; Podnieks, K. 「4.4 構成的命題論理 - クリプキ意味論」。数理論理学入門。ラトビア大学。注意: 建設的 = 直観主義的。
• ガーソン、ジェームズ（2023年1月23日）。「様相論理」。ザルタ、エドワードN.（編）スタンフォード哲学百科事典。
• 「クリプキモデル」、数学百科事典、EMS Press、2001 [1994]
• モスコヴァキス、ジョアン（2022年12月16日）。「直観主義論理」。ザルタ、エドワードN.（編）スタンフォード哲学百科事典。