様相論理

様相論理（ようそうろんり、英: modal logic）は、命題が成立する様相 (modality) を扱う論理体系の総称である。形式的には、古典命題論理をはじめとする標準的な論理体系に、「必然性」や「可能性」などを表す様相演算子 $□, ◇$ を追加することで構成される。

形式論理としての様相論理は、「～は必然的に真である」や「～が真であることが可能である」といった命題の様相概念を形式化したC・I・ルイスらによる研究に端を発する。その後、クリプキによって関係構造に基づく意味論が与えられたことにより、様相論理はグラフ構造や状態遷移図などの関係構造を局所的に記述する論理として再定義されている。この柔軟な枠組みにより、現代の様相論理は哲学のみならず、計算機科学や数学など、幅広い分野で応用されている。

さまざまな様相

古典的な命題論理では、「雨が降っている」というような命題の真偽のみを問題にするが、様相論理では「雨が降る可能性がある」のような真理の様相を分析の対象とする。

伝統的に、様相論理は真理論的様相を分析する道具であった。これは、真理の論理的あるいは形而上学的な必然性を扱うもので、「～は必然的である」ということを必然性演算子 $□$ で、「～であることが可能である」ということを可能性演算子 $◇$ で表す。これらの演算子は互いに、 $◇ φ \equiv ￢□￢ φ$ （真である可能性があるとは、偽であることが必然的でないことと同値）という双対関係にある。

現代の様相論理では、これらの演算子を真理論的様相以外の多様な概念に読み替えることで、広範な応用が行われている。たとえば、「〜を知っている」のような認識論的様相、「～すべきである」のような義務表現、あるいは「常に〜である」「いままでずっと〜であった」のような時間概念は、すべて様相論理を用いて分析される対象となっている。

様相論理の公理系

以下では様相論理のうちで最もシンプルなものである、古典命題論理をベースにした古典命題様相論理を考える。

様相論理は、命題論理の論理記号 $￢, \land, \lor, \to$ に加え、ふたつの演算子 $□, ◇$ を用いる。具体的には、様相論理の論理式は、原子命題の可算集合 $Prop$ を用いて、以下のように帰納的に定義される。

全ての原子命題 $p \in Prop$ は論理式である。
$φ, ψ$ が論理式ならば、 $￢ φ, φ \land ψ, φ \lor ψ, φ \to ψ$ は論理式である。
$φ$ が論理式ならば、 $□ φ, ◇ φ$ は論理式である。
論理式は以上の手続きで定義されたものに限る。

この定義は、バッカス・ナウア記法を用いて、次のように簡潔に表現することもできる（ただし $p \in Prop$ ）。

{\displaystyle \varphi

正規様相論理 K

現在扱われる様相論理の中で関係構造を記述する論理として標準的なものは正規様相論理とよばれるものである。その中でももっとも基本的なものは、論理学者ソール・クリプキの頭文字をとり $K$ とよばれる。

公理系 $K$ は古典命題論理の公理系に次の公理と推論規則を付け加えたものである。

K公理： $\Box (p\rightarrow q)\rightarrow (\Box p\rightarrow \Box q)$
Dual公理： $\Diamond p\leftrightarrow \neg \Box \neg p$
必然化規則： $φ$ が証明可能ならば、 $□ φ$ が証明可能。

必然化規則は「任意の論理式 $φ$ について $φ \to□ φ$ 」と同義でないことに注意。必然化規則が認められるのは、あくまで $φ$ が公理系で証明できるときに限る。

主要な拡張体系

公理系 $K$ にさらに特定の公理図式を追加することで、より強い論理体系（ $K$ の拡張体系）が作られる。代表的な公理は次の5つで、歴史的な経緯からアルファベットや数字の名前が付けられている。

D公理： $\Box p\rightarrow \Diamond p$
T公理： $\Box p\rightarrow p$
B公理： $p\rightarrow \Box \Diamond p$
4公理： $\Box p\rightarrow \Box \Box p$
5公理： $\Diamond p\rightarrow \Box \Diamond p$

これらの公理を $K$ に組み合わせていくことで、様々な正規様相論理の体系が定義される。代表的な体系として、 $K$ にT公理と4公理を追加した $S4$ 、 $K$ にT公理と5公理を追加した $S5$ がある。これらの体系の間には、証明能力の強弱による包含関係が存在する（たとえば、 $S4$ の定理はすべて $S5$ で証明可能： $S4 \subseteq S5$ ）。上にあげた5つの公理からは、どれを採用するかによって合計で15個の相異なる公理系を構成できる。これらの包含関係は図としてまとめられており、これを modal cube と呼ぶこともある^[1]。

公理系 $K$ においては、様相演算子を多重に重ねた論理式（例えば $□□ p$ や $◇□◇ p$ など）は、それぞれが互いに論理的に独立した異なる意味を持つ。したがって、理論上は無限に多くの様相のパターンが区別されることになる。しかし、より強い公理系である $S4$ や $S5$ においては、多重の様相演算子をより単純な形に「還元」することができる。

たとえば $S5$ ではきわめて強力な還元法則が成り立つ。具体的には、次の4つの論理式が証明可能^[2]。

$\Diamond \Diamond \varphi \leftrightarrow \Diamond \varphi$
$\Box \Box \varphi \leftrightarrow \Box \varphi$
$\Box \Diamond \varphi \leftrightarrow \Diamond \varphi$
$\Diamond \Box \varphi \leftrightarrow \Box \varphi$

この結果、 $S5$ において本質的に区別される様相は、空（様相なし）・ $□$ ・ $◇$ のわずか3種類（その否定を含めれば6種類）にまで単純化される^[3]。同様に、公理系 $S4$ では 1. と 2. および 3. の左辺から右辺、4. の右辺から左辺の方向が証明可能である。そのため、様相のパターンは7種類（否定を含めれば14種類）に絞られる^[4]。

非正規様相論理

公理系 $K$ のような正規様相論理は、特定の応用においては「強すぎる」ことがある。例えば $□ p$ を「 $p$ を知っている」と解釈した場合、必然化規則は「論理的なトートロジーをすべて知っている」ことを要求する。これは、人間などの有限なエージェントのモデルとしては非現実的である。

そこで、 $K$ の条件すら満たさない、より弱い体系である非正規様相論理も考えられている。非正規様相論理の代表的な公理系である公理系 $E$ は、古典命題論理の公理系にDual公理と次の推論規則を加えたものである。

同値性規則： $\varphi \leftrightarrow \psi$ が証明可能ならば、 $\Box \varphi \leftrightarrow \Box \psi$ が証明可能。

この規則は、「互いに論理的に同値な命題は、様相演算子を適用しても同値である」という、様相オペレーターの最低限の性質を保証するものである。Dual公理を持ち同値性規則を満たす様相論理のクラスは一般に古典的様相論理（英語版）と総称されており、公理系 $E$ はその中で最小の体系として位置づけられる^[5]。

様相論理の意味論

様相論理の標準的な意味論は、ソール・クリプキによって与えられたクリプキ意味論と呼ばれる枠組みである。この意味論は、前節で導入した正規様相論理に対して、グラフ構造を用いた解釈を与える。このグラフにおける点が可能世界論における可能世界とみなせることから、クリプキ意味論は可能世界意味論とも呼ばれる。

クリプキ意味論

命題様相論理のクリプキ意味論の概要を述べる。

$W$ を空でない集合とする。これは個々の可能世界全体の集合を表していると考えられる。次に $W$ 上に二項関係 $R$ を定める（すなわち $R \subseteq W\timesW$ ）。 $R$ は $W$ 上の到達関係と呼ばれ、様相演算子の付いた論理式の真偽に影響する。これらの組 $F = (W, R)$ をクリプキフレーム（あるいは単にフレーム）と呼ぶ。また原子命題全体の集合 $Prop$ と先に定義した $W$ に対し、関数 $V$ を

V:\mathbf {Prop} \rightarrow {\mathcal {P}}(W)

として定義する（ $P (W)$ は $W$ の冪集合、すなわち部分集合全体の集合である）。これは付値関数とよばれ、ある原子命題についてそれが真である可能世界の集合を与える関数である。このように定義された組 $M = (W, R, V)$ をクリプキモデル（あるいは単にモデル）と呼ぶ。

論理式の真偽は、扱うモデルとその可能世界に対して相対的に定まる。モデル $M$ とその可能世界 $w$ において、論理式 $φ$ が真であることを $M, w ⊨ φ$ と書き、この関係を以下のように再帰的に定義する。

${\mathcal {M}},w\models p\iff w\in V(p)$ （ただし、 $p\in \mathbf {Prop}$ ）
${\mathcal {M}},w\models \neg \varphi \iff {\mathcal {M}},w\not \models \varphi$
${\mathcal {M}},w\models \varphi \land \psi \iff {\mathcal {M}},w\models \varphi$ かつ ${\mathcal {M}},w\models \psi$
${\mathcal {M}},w\models \varphi \lor \psi \iff {\mathcal {M}},w\models \varphi$ または ${\mathcal {M}},w\models \psi$
${\mathcal {M}},w\models \varphi \rightarrow \psi \iff {\mathcal {M}},w\not \models \varphi$ または ${\mathcal {M}},w\models \psi$
${\mathcal {M}},w\models \Box \varphi \iff$ すべての $v\in W$ について、 $wRv$ ならば ${\mathcal {M}},v\models \varphi$
${\mathcal {M}},w\models \Diamond \varphi \iff$ ある $v\in W$ が存在して、 $wRv$ かつ ${\mathcal {M}},v\models \varphi$

すなわち、 $□ φ$ は「現在の世界からアクセス可能な全ての世界で $φ$ が真」であることを意味し、局所的な全称量化として機能する。対して $◇ φ$ は「アクセス可能ないずれかの世界で $φ$ が真」であるという局所的な存在量化として機能する。

ある論理式 $φ$ が任意のモデルの任意の可能世界で真であるとき（すなわち、すべての $M, w$ について $M, w ⊨ φ$ が成り立つとき）、 $φ$ は恒真である (valid) という。また、あるフレームのクラス $C$ に属する任意のフレーム $(W, R)$ について、どんな付値関数 $V$ とどんな可能世界 $w$ をとっても論理式 $φ$ が真であるとき（ $(W, R, V), w ⊨ φ$ となるとき）、論理式 $φ$ はそのフレームクラスにおいて恒真であるという。

さらに、特定の様相論理の論理式およびその集合は、フレームにおける二項関係の性質を定義する。より具体的には、あるフレームのクラスで特定の論理式が恒真であることと、そのクラスに属するフレームの二項関係が特定の性質を満たすことが同値になる。この性質はフレームの定義可能性^[6]、あるいは対応理論^[7]と呼ばれる。例えば、前節で導入した5つの公理は、次の性質を定義する。

D公理は継起性（任意の $w$ に対し、 $wRv$ となる $v$ が存在する）に対応する。
T公理は反射性（任意の $w$ に対し $wRw$ が成り立つ）に対応する。
B公理は対称性（任意の $w, v$ に対し、 $wRv$ ならば $vRw$ が成り立つ）に対応する。
4公理は推移性（任意の $w, v, u$ に対し、 $wRv$ かつ $vRu$ ならば $wRu$ が成り立つ）に対応する。
5公理はユークリッド性（任意の $w, v, u$ に対し、 $wRv$ かつ $wRu$ ならば $vRu$ が成り立つ）に対応する。

この対応関係により、例えば「到達関係が反射的かつ推移的であるようなフレームのクラスは、T公理と4公理が恒真であるようなフレームのクラスと一致する」というような事実が導かれる。

近傍意味論

前節で述べたクリプキ意味論は、K公理や必然化規則を自動的に満たしてしまう。したがって、これらを持たない公理系 $E$ などの非正規様相論理を解釈するためには、クリプキ意味論をさらに一般化した枠組みが必要となる。その代表的なものが近傍意味論（考案者の名前からスコット＝モンタギュー意味論とも呼ばれる）である。

近傍意味論におけるモデルは、可能世界と「命題の集合」との対応関係が含まれる。具体的には、近傍関数 $N$ を次のように定義する。

N:W\rightarrow {\mathcal {P}}({\mathcal {P}}(W))

このとき、組 $(W, N)$ を近傍フレームといい、また近傍フレームと付値関数を使って構成されるモデル $M = (W, N, V)$ を近傍モデルという。

近傍モデルとその可能世界に対する命題の真偽は、命題変数およびそのブール演算子による結合についてはクリプキモデルと同様にして定まる。いま、ある論理式 $φ$ に対して集合 $‖ φ ‖ M$ を $\|\varphi \|^{\mathcal {M}}=\{w\in W\mid {\mathcal {M}},w\models \varphi \}$ と定めると（すなわち $φ$ が真となる可能世界の集合）、近傍モデルにおける必然化演算子を含む論理式の真理条件は

{\mathcal {M}},w\models \Box \varphi \iff \|\varphi \|^{\mathcal {M}}\in N(w)

と定義される。付値関数の定め方から、様相論理における命題はそれが真になる可能世界の集合と同一視できる。このことから、ある可能世界 $w$ の近傍 $N (w)$ とは「 $w$ で必然的に真である命題の集合」であると考えることもできる。

近傍モデルにおいては、同値性規則が成立する。もし $φ$ と $ψ$ が論理的に同値であれば $‖ φ ‖ M = ‖ ψ ‖ M$ が成り立つ。このとき一方が $N (w)$ に属する時かつその時に限りもう一方も $N (w)$ に属するから、 $□ φ$ と $□ ψ$ も論理的に同値である。しかし、K公理は一般には成り立たず、また必然化規則も成り立たない。

任意のクリプキモデルに対して、それと同等の近傍モデルが存在する。実際に、あるクリプキモデル $M = (W, R, V)$ が与えられたとき、以下の条件で近傍関数 $N$ を定めれば、近傍モデル $M' = (W, N, V)$ は与えられたクリプキモデルと等価になる。

N(w)=\{\|\varphi \|^{\mathcal {M}}\mid {\mathcal {M}},w\models \Box \varphi \}

しかしその逆は成り立たず、任意の近傍モデルに対してそれと等価なクリプキモデルを構成できるとは限らない。このことから、近傍意味論はクリプキ意味論の数学的な一般化として位置づけられている。

様相論理の主要な性質

様相論理はいくつかのすぐれた性質をもつ。この節ではそのうちいくつかを紹介する。

健全性と完全性

様相論理の公理系と意味論のあいだには、健全性・完全性が成り立つことが知られている。

健全性: 論理式がある公理系で証明可能ならば、それは対応するフレームのクラスにおいて恒真である、という性質。
完全性: 論理式があるフレームのクラスにおいて恒真であるならば、それは対応する公理系で証明可能、という性質。

公理系 $K$ はすべてのクリプキフレームのクラスに対して健全かつ完全である。また、公理系 $S4$ は反射的かつ推移的な関係をもつフレームのクラスに対し健全かつ完全、公理系 $S5$ は二項関係が同値関係になるようなフレームのクラスに対し健全かつ完全であり、同様の性質が modal cube に属する15の公理系についていえる。さらに、公理系 $E$ はすべての近傍フレームのクラスと健全かつ完全である。

決定可能性と有限モデル性

一階述語論理とは異なり、代表的な様相論理の多く（たとえば modal cube 内の公理系）は決定可能である。これは、任意の論理式 $φ$ が与えられたとき、それが公理系の定理であるか否かを有限時間で判定するアルゴリズムが存在することを意味する。

さらに、多くの様相論理は有限モデル性をもつこともわかっている。これは、ある論理式 $φ$ を真にするモデルと可能世界が存在するならば、その論理式を真にする「有限個の世界からなるモデル」とその可能世界が存在する、という性質である。

フレーム定義可能性

様相論理の論理式によって定義可能なフレームの性質を特徴づける定理として、ゴールドブラッド・トマソンの定理が知られている。この定理は、一階述語論理で記述可能なフレームの性質が、様相論理の論理式集合によって定義可能であるための必要十分条件を与える^[8]。

また、フレームを定義可能な論理式のクラスとして、サールクヴィスト式（英語: Sahlqvist formula）というものが知られている。このクラスに属する様相論理の論理式には対応するフレームの性質が存在し、さらにその式を公理として追加した正規様相論理は、対応するフレームのクラスに対して健全性と完全性が成り立つ（サールクヴィストの対応定理）^[9]。

ファン・ベンタムの定理

様相論理を一階述語論理の断片としてみなすとき、その表現力は双模倣性によって特徴づけられる。ふたつのクリプキモデルの間に双模倣関係が存在するとき、それらのモデルは様相論理の言語では区別することができない。ファン・ベンタムの定理は、「一階述語論理の論理式のうち、双模倣性に関して不変なものは、様相論理の論理式と等価である」ことを主張する^[10]。双模倣的なふたつのシステムは互いにもう一方をシミュレートできるということから、様相論理の言語はまさしくそうした局所的な構造を記述するための言語であるといえる。

様相論理の応用

対象とする様相を適切に設定することで、様相論理の枠組みは、哲学、計算機科学、数学の多種多様な領域に応用されている。

認識論理

認識論理とは、「〜を知っている」という知識の様態や、「～を信じている」という信念の様相を扱う論理である。認識論理においては、エージェント $i$ が命題 $φ$ を知っているということを $K i φ$ と表記する（信念の場合は $B i φ$ が用いられる）。対応するクリプキモデルはエージェントの数だけ二項関係 $R i, R j, ...$ を持ち、演算子 $K i$ はモデルの上では必然化演算子として解釈される。

通常、知識の性質を反映する体系としては $S5$ が採用される。また、誤った事実であってもそれを信じることはできる（すなわち、 $B i p \to p$ が一般には成り立たない）という事実から、「信念」の場合は $KD45$ が採用される。ところが、正規様相論理を認識論理に適用すると、必然化規則やK公理により、「エージェントは全てのトートロジーを知っており、かつ自分の知識の論理的帰結をすべて知っている」ことになってしまう。このことは論理的全知 (Logical Omniscience) とよばれ、現実のエージェントの知的能力の有限性を考えるうえで、この乖離を解消することがひとつの重要な研究テーマとなる^[11]。

義務論理

義務論理 (deontic logic) とは、義務や権利といった規範の様相を扱う論理である。ゲオルク・ヘンリク・フォン・ウリクトによる標準義務論理では、「 $φ$ すべきである」という義務の様相を $Oφ$ 、「 $φ$ してもよい」という権利の様相を $Pφ$ と表記し、これらをそれぞれ様相論理の必然化演算子と可能性演算子として読む。標準義務論理では、公理系 $K$ にD公理を足した体系 $D$ をベースとする。義務論理におけるD公理は $Op \to Pp$ であり、これは「義務であることは許可される」として直観的に解釈できる。ただし、標準義務論理の枠組みとわれわれの義務概念にはいくつかの隔たりがあり（義務論理のパラドックスを参照）、これを解決する取り組みが行われている。

時相論理

時相論理 (temporal logic) は時間の様相を扱う論理であり、「未来でいつか〜になる」「過去ずっと〜であった」といった時間の経過に伴う真偽の変化を形式化する。

様相論理を用いて時間概念をとらえる論理のはしりとなったのは、アーサー・プライヤーによって提唱された時制論理 (tense logic) である。この論理では、4 つの様相記号 $F$ （未来のいつかで～が真）、 $G$ （今後つねに～が真）、 $P$ （かつてあるときに～が真）、 $H$ （これまでずっと～が真）を用いる。これらはクリプキモデルにおいては以下のように解釈される。

${\mathcal {M}},w\models F\varphi \iff$ ある $v\in W$ が存在して、 $wRv$ かつ ${\mathcal {M}},v\models \varphi$
${\mathcal {M}},w\models G\varphi \iff$ すべての $v\in W$ について、 $wRv$ ならば ${\mathcal {M}},v\models \varphi$
${\mathcal {M}},w\models P\varphi \iff$ ある $v\in W$ が存在して、 $vRw$ かつ ${\mathcal {M}},v\models \varphi$
${\mathcal {M}},w\models H\varphi \iff$ すべての $v\in W$ について、 $vRw$ ならば ${\mathcal {M}},v\models \varphi$

時制論理の公理系は、 $F$ , $G$ のペアと $P$ , $H$ のペアそれぞれに関するDual公理、ふたつの必然化演算子 $G$ , $H$ に関するK公理と必然化規則を認め、さらに次の2つの公理を加える^[12]。

$p\rightarrow GPp$
$p\rightarrow HFp$

ほかの時相論理として、時間の流れを直線的なものととらえて記述する線形時相論理 (LTL) や、未来を分岐する木構造ととらえて記述する計算木論理 (CTL) などがあり、これらは計算機科学の分野で不可欠な道具となっている。

命題動的論理

命題動的論理 (propositional dynamic logic, PDL) とは、コンピュータプログラムの実行とその結果生じる状態変化を形式的に記述・検証する論理である。命題動的論理の様相演算子 $[α]$ はプログラム $α$ ごとに定められ、これを用いた論理式 $[α] φ$ は「プログラム $α$ が終了したのちのいかなる状態においても $φ$ が成り立つ」と解釈される。

命題動的論理は、プログラムの逐次実行 $α; β$ 、非決定的選択 $α \cup β$ 、繰り返し $α *$ 、テスト $φ ?$ といった操作を演算子として持つ。これらを用いることで、複雑なアルゴリズムにおいても、その正当性を形式的に証明できる。また命題動的論理は、プログラムの正当性を検証するための古典的な枠組みであるホーア論理 (Hoare logic) を、プログラムの構造に着目して抽象化したものとみなせる^[13]^{[注釈 1]}。

証明可能性論理

証明可能性論理 (provability logic) とは、ある形式的体系（形式的算術など）において「〜が証明可能である」という概念を様相とみなし、そのふるまいを記述する論理である。

証明可能性論理の最も代表的な公理系は $GL$ とよばれる。これは公理系 $K$ にマルティン・レーブから名付けられた以下のレーブの公理（あるいはL公理）を追加することで得られる。

\Box (\Box p\rightarrow p)\rightarrow \Box p

L公理は、算術において「ある体系で『 $φ$ が証明可能ならば $φ$ 』が証明可能ならば、その体系で $φ$ 自身が証明可能である」というレーブの定理を様相論理の論理式で表現したものである。この定理は、ゲーデルの第二不完全性定理の一般化としてとらえることができ^{[注釈 2]}、それゆえ証明可能性論理もまた不完全性定理と密接な関係にある。

証明可能性論理と形式的算術をつなぐ重要な性質として、ロバート・ソロヴェイ（英語: Robert M. Solovay）により証明された算術的完全性定理がある。この定理によれば、ある様相論理の論理式が $GL$ で証明可能であることと、その論理式の算術的解釈がある種の算術、たとえばペアノ算術 $PA$ 、で証明可能であることは同値となる^[14]。算術的完全性はいわば、形式的算術と証明可能性論理のあいだに健全性・完全性が成り立っていることを主張している。

様相論理の歴史

現代的な様相論理の歴史^{[注釈 3]}は、1918年に発表されたC・I・ルイスの著書 A Survey of Symbolic Logicに始まる。その著書の中で彼は、自然言語における含意により忠実なふるまいをする厳密含意を扱う論理体系を提案した。オスカー・ベッカー（英語: Oscar Becker）は1930年の論文^[19]で、ルイスの体系において様相演算子の反復により多様な様相が表現できることを指摘し、またそれらの還元公理を提案した。その後、ルイスとクーパー・ラングフォード（英語: Cooper Harold Langford）との共著 Symbolic Logic において $S1$ から $S5$ までの5つの論理体系が提案された。

1933年、クルト・ゲーデルは「形式論理における証明可能性」という概念を様相ととらえて公理化した^[20]。この公理系は、現代の様相論理における $S4$ と同一である。またロバート・フェイス（英語: Robert Feys）は1937年の論文^[21]で、様相記号を用いてルイスの煩雑な体系を整理し、のちの公理系 $T$ を提案している。

様相論理の意味論は、ルドルフ・カルナップによる状態記述を用いた可能世界概念に基づく意味論や、J・C・C・マッキンゼー（英語: J. C. C. McKinsey）とアルフレト・タルスキによる代数的意味論など、様々な形で考えられてきた。そのなかでもソール・クリプキによって提案された可能世界意味論は様相論理を飛躍的に前進させた。彼はまず1959年に $S5$ に対する健全性と完全性を証明した^[22]。その後1963年には論文 Semantical Analysis of Modal Logic I において、可能世界間の到達関係を備えた遷移モデルを導入し、さまざまな正規様相論理の健全性と完全性を示した^[23]。これにより、公理系の性質を遷移モデルの幾何学的な性質と対応させて扱うことが可能になった。正規様相論理の公理系とクリプキの提案した意味論との関係はジョン・レモンとデイナ・スコットによる共同研究によって整理され、俗に「レモン・ノート」として知られる草稿（1977年に出版^[24]）にまとめられた。

脚注

注釈

↑ たとえば、if文 $if φ then α else β$ は $(φ ?; α)\cup(￢ φ ?; β)$ のように、while文 $while φ do α$ は $(φ ?; α) *;￢ φ ?$ のように書ける。
↑ L公理の $p$ に $⊥$ を代入して対偶をとると $￢□⊥\to￢□￢□⊥$ となり、まさに「ある体系で矛盾が証明できない（無矛盾）ならば、矛盾が証明できないことそのものは証明できない」という第二不完全性定理の主張となる。
↑ 様相論理の歴史については、Blackburn らの書籍^[15]や Cresswell の論文^[16]を参照。また、日本語文献として、菊池らの書籍^[17]や吉満^[18]の論文がある。

出典

↑ Leme, R., et al. (2026). The Modal Cube Revisited: Semantics Without Worlds. In TABLEAUX 2025, LNAI 15980, pp. 181-200. doi:10.1007/978-3-032-06085-3_10.
↑ Chellas 1980, p. 148.
↑ Chellas 1980, p. 154.
↑ Chellas 1980, p. 149.
↑ Chellas 1980, pp. 231–232.
↑ 菊池（編） 2016, p. 30.
↑ 大西 2021, p. 63.
↑ Blackburn, de Rijke & Venema 2002, p. 143.
↑ Blackburn, de Rijke & Venema 2002, p. 165.
↑ Blackburn, de Rijke & Venema 2002, p. 103.
↑ Fagin, R., et al. (1995). Reasoning About Knowledge. The MIT Press. doi:10.7551/mitpress/5803.001.0001
↑ Blackburn, de Rijke & Venema 2002, p. 205.
↑ 鹿島 2025, p. 148.
↑ 菊池（編）, p. 115.
↑ Blackburn, de Rijke & Venema 2002, pp. 38–48.
↑ Cresswell, M. (2019). Modal Logic before Kripke. Organon F, 26(3), pp. 323-339. doi:10.31577/orgf.2019.2630.
↑ 菊池（編） 2016, pp. 84–92.
↑ 吉満昭宏「C.I.ルイスと様相論理の起源」『科学哲学』37-1号、2004年、1-14頁。doi:10.4216/jpssj.37.1
↑ Becker, O. (1930). Zur Logik der Modalitäten. Jahrbuch für Philosophie und Phänomenologische Forschung, 11, pp. 497-548.
↑ Gödel, K. (1933). Eine Interpretation des intuitionistischen AussagenKalüls. Ergebnisse eines Mathematischen Kolloquiums, 4, pp. 39–40.
↑ Feys, R. (1937). Les Logiques Nouvelles des Modalités. Revue Néoscholastique de Philosophie, 40, pp. 517–553. doi:10.3406/phlou.1937.3056
↑ Kripke, S. A. (1959). A Completeness Theorem in Modal Logic. The Journal of Symbolic Logic, 24(1), pp. 1-14. doi:10.2307/2964568
↑ Kripke, S. A. (1963). Semantical Analysis of Modal Logic I. Normal Propositional Calculi. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 9, pp. 67-96. doi:10.1002/malq.19630090502
↑ Lemmon, E. J. and Scott, D. (1977). An Introduction to Modal Logic: the Lemmon Notes. Oxford: Blackwell.

参考文献

Blackburn, Patrick; de Rijke, Maarten; Venema, Yde (2002) [2001]. Modal Logic. Cambridge: Cambridge University Press. doi:10.1017/cbo9781107050884. ISBN 9780521527149
Chellas, Brian F. (1980). Modal logic: an introduction. Cambridge University Press. doi:10.1017/CBO9780511621192. ISBN 9780511621192
大西琢朗『論理学（3STEPシリーズ）』昭和堂、2021年。ISBN 9784627856417。
鹿島亮『コンピュータサイエンスにおける様相論理』名古屋大学出版会、2025年。ISBN 9784627856417。
佐野勝彦、倉橋太志、薄葉季路、黒川英徳、菊池誠著、菊池誠編『数学における証明と真理―様相論理と数学基礎論―』共立出版、2016年。ISBN 9784320111486。
戸田山和久『論理学をつくる』名古屋大学出版会、2000年。ISBN 4815803900。

外部リンク

Modal logic （英語版wikipedia）
Modal Logic （英語） - スタンフォード哲学百科事典「様相論理」の項目。
modal logic - nLab （英語）

[14] たとえば、if文 $if φ then α else β$ は $(φ ?; α)\cup(￢ φ ?; β)$ のように、while文 $while φ do α$ は $(φ ?; α) *;￢ φ ?$ のように書ける。

[15] L公理の $p$ に $⊥$ を代入して対偶をとると $￢□⊥\to￢□￢□⊥$ となり、まさに「ある体系で矛盾が証明できない（無矛盾）ならば、矛盾が証明できないことそのものは証明できない」という第二不完全性定理の主張となる。

[21] 様相論理の歴史については、Blackburn らの書籍^[15]や Cresswell の論文^[16]を参照。また、日本語文献として、菊池らの書籍^[17]や吉満^[18]の論文がある。

[1] Leme, R., et al. (2026). The Modal Cube Revisited: Semantics Without Worlds. In TABLEAUX 2025, LNAI 15980, pp. 181-200. doi:10.1007/978-3-032-06085-3_10.

[FOOTNOTEChellas1980148-2] Chellas 1980, p. 148.

[FOOTNOTEChellas1980154-3] Chellas 1980, p. 154.

[FOOTNOTEChellas1980149-4] Chellas 1980, p. 149.

[FOOTNOTEChellas1980231–232-5] Chellas 1980, pp. 231–232.

[FOOTNOTE菊池（編）201630-6] 菊池（編） 2016, p. 30.

[FOOTNOTE大西202163-7] 大西 2021, p. 63.

[FOOTNOTEBlackburnde_RijkeVenema2002143-8] Blackburn, de Rijke & Venema 2002, p. 143.

[FOOTNOTEBlackburnde_RijkeVenema2002165-9] Blackburn, de Rijke & Venema 2002, p. 165.

[FOOTNOTEBlackburnde_RijkeVenema2002103-10] Blackburn, de Rijke & Venema 2002, p. 103.

[11] Fagin, R., et al. (1995). Reasoning About Knowledge. The MIT Press. doi:10.7551/mitpress/5803.001.0001

[FOOTNOTEBlackburnde_RijkeVenema2002205-12] Blackburn, de Rijke & Venema 2002, p. 205.

[FOOTNOTE鹿島2025148-13] 鹿島 2025, p. 148.

[FOOTNOTE菊池（編）115-16] 菊池（編）, p. 115.

[FOOTNOTEBlackburnde_RijkeVenema200238–48-17] Blackburn, de Rijke & Venema 2002, pp. 38–48.

[18] Cresswell, M. (2019). Modal Logic before Kripke. Organon F, 26(3), pp. 323-339. doi:10.31577/orgf.2019.2630.

[FOOTNOTE菊池（編）201684–92-19] 菊池（編） 2016, pp. 84–92.

[20] 吉満昭宏「C.I.ルイスと様相論理の起源」『科学哲学』37-1号、2004年、1-14頁。doi:10.4216/jpssj.37.1

[22] Becker, O. (1930). Zur Logik der Modalitäten. Jahrbuch für Philosophie und Phänomenologische Forschung, 11, pp. 497-548.

[23] Gödel, K. (1933). Eine Interpretation des intuitionistischen AussagenKalüls. Ergebnisse eines Mathematischen Kolloquiums, 4, pp. 39–40.

[24] Feys, R. (1937). Les Logiques Nouvelles des Modalités. Revue Néoscholastique de Philosophie, 40, pp. 517–553. doi:10.3406/phlou.1937.3056

[25] Kripke, S. A. (1959). A Completeness Theorem in Modal Logic. The Journal of Symbolic Logic, 24(1), pp. 1-14. doi:10.2307/2964568

[26] Kripke, S. A. (1963). Semantical Analysis of Modal Logic I. Normal Propositional Calculi. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 9, pp. 67-96. doi:10.1002/malq.19630090502

[27] Lemmon, E. J. and Scott, D. (1977). An Introduction to Modal Logic: the Lemmon Notes. Oxford: Blackwell.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[注釈 1]

[注釈 2]

[14]

[注釈 3]

[19]

[20]

[21]

[22]

[23]

[24]

[15]

[16]

[17]

[18]