日記 (2025 年 2 月 23 日)

唐突だが、様相論理を少し勉強したくなり Chellas†1 を読み始めたので、ここに勉強ノートとして簡単にまとめておこうと思う。

様相論理とは、名前の通り様相を扱えるようにした論理体系である。では、様相とは一体何なのか? 私も勉強途中なので完璧な回答はできないが、とりあえず今の私の理解では次のように説明できる。

通常の命題論理において、命題として念頭に置かれているのは、「地球は太陽の周りを回っている」や「1+1 は 2 に等しい」のように、状況によらず真偽が一定である不変の真理である。したがって、「～というのは必然である」や「～ということは常識である」や「将来～だろう」のような、状況によって真偽が変わるような言明は扱いづらい。様相論理は、真偽が定まる状況や方式のようなものを「様相」と呼び、この様相を扱えるように命題論理を拡張することで、先述のような言明を扱おうとしたものである。

まず、様相論理で用いる式を定義しよう。

定義 1.1.

n は自然数を表すとし、言語を以下で定める。 A::=pn∣⊤∣⊥∣¬A∣A∧A∣A∨A∣A⇀A∣◻A∣⬦A これによって定まる記号列 A を「式 (formula)」と呼ぶ。さらに特に、 pn の形のものを「原子式 (atomic formula)」と呼び、 ◻A か ⬦A の形のものを「様相式 (modal formula)」と呼ぶ。

なお、式を書く際に括弧は曖昧にならない程度で適宜省略する。基本的に、 ¬, ◻, ⬦ が最も強く結合し、次に ⇀ が強く結合し、 ∧, ∨ は最も弱く結合する。また、 (A⇀B)∧(B⇀A) のことを A⥎B と略記する。

さて、定義から分かるように、様相論理における式には、通常の命題論理に対して ◻A と ⬦A という 2 つの形の式が追加されている。これが、先程述べた「～というのは必然である」や「将来～だろう」のような、様相を含む言明を表す式である。

と言っても、これだけでは様相のイメージは全然掴めないので、さっそくだが様相論理の意味論に触れていこう。様相論理の意味論として最も有名なのは、 Kripke によるフレーム意味論である。

定義 1.2.

次のような 3 つのデータ W,∼,P を考える。

W は空でない集合である。
∼ は W 上の二項関係である。
P:󱀍→󱁍(W) は写像である。すなわち、各自然数 n に対して部分集合 Pn⊆W が定まっている。

このとき、対 (W,∼) を「フレーム (frame)」と呼び、組 (W,∼,P) を「モデル (model)」と呼ぶ。また、 W の元をしばしば「世界 (world)」と呼ぶ。

モデル (W,∼,P) のイメージは概ね次のように説明できる。

まず W は、様々な言明の真偽が定まる並行世界の集合である。例えば、「A は常識である」という形の言明を扱いたければ、人それぞれが信じている内容を 1 つの並行世界と思うことで、「A は常識である」を「全ての世界で A が真である」と見なせる。また、「将来 A になるだろう」という形の言明を扱いたければ、各時刻を 1 つの並行世界と見なすことで、「将来 A になるだろう」は「今後のある世界で A が真である」と解釈できる。このように、最初に例に挙げたような様々な種類の様相を、「～のような世界においては真」のような形で表現しようとしているのである。

次に ∼ は、世界同士の関連性を定めているものだと解釈できる。例を挙げると、「将来 A になるだろう」という種類の様相を扱いたい場合は、先程述べたように、並行世界として特定の時刻における状況を考えれば良いのであった。このとき、 2 つの世界 α,β に対して α∼β を「β の時刻の方が α の時刻より後である」と定めれば、「α において将来 A になるだろう」は「α∼β であるような β において A が真である」と言い直せる。このように、考えている様相によっては、特定の世界における様相命題の真偽が、その世界と関連している (今の例ではその世界より時刻が後である) 世界のみに依存していることがある。 ∼ は、このような世界同士の関連性を定式化している。

最後に P は、各原子式が真であるような世界の集合を定めるものである。例えば、 P0⊆W は p0 が真であるような世界全体の集合を意図している。

以上のイメージを踏まえて、モデルに属するある世界における式の妥当性を以下のように定義する。特に、原子式と様相式の妥当性の定義に注目されたい。

定義 1.3.

モデル 󰒤=(W,∼,P) の世界 α∈W を考える。式 A に対し、命題 α⊨󰒤A を以下で再帰的に定義する。

α⊨󰒤pn であるのは、 α∈Pn が成り立つときである。
α⊨󰒤⊤ は常に真である。
α⊨󰒤⊥ は常に偽である。
α⊨󰒤¬A であるのは、 α⊨󰒤A が成り立たないときである。
α⊨󰒤A∧B であるのは、 α⊨󰒤A かつ α⊨󰒤B が成り立つときである。
α⊨󰒤A∨B であるのは、 α⊨󰒤A または α⊨󰒤B が成り立つときである。
α⊨󰒤A⇀B であるのは、 α⊨󰒤A ならば α⊨󰒤B が成り立つときである。
α⊨󰒤◻A であるのは、 β∈W であって α∼β を満たすもの全てに対して β⊨󰒤A が成り立つときである。
α⊨󰒤⬦A であるのは、 β∈W であって α∼β を満たすものが存在して β⊨󰒤A が成り立つときである。

α⊨󰒤A が成り立つとき、 A は α において「妥当 (valid)」であるという。

これはモデルに属する特定の世界における式の妥当性の定義である。これを用いて、モデル全体における (世界によらない) 式の妥当性を以下のように定義する。

定義 1.4.

モデル 󰒤=(W,∼,P) をとる。式 A に対して、 ⊨󰒤A が成り立つことを、任意の α∈W に対して α⊨󰒤A が成り立つことと定める。このとき、 A は 󰒤 において「妥当 (valid)」であるという。

さて、ある式があらゆるモデルで妥当であれば、その式自体は様相論理において絶対的に成り立つものだと考えることができる。しかし、考えている様相によっては、念頭に置いているモデルの形 (特に世界の間の二項関係) に制約をかけるべきであることがある。例えば、「将来～になるだろう」という様相を考える場合、世界 α,β に対して、 α∼β を「β の時刻の方が α の時刻より後である」と捉えるのであった。ところで、 3 つの世界 α,β,γ があり、 β の方が α より時刻が後で、 γ の方が β よりさらに時刻が後であるなら、当然 γ は α よりも時刻が後である。すなわち、 ∼ を今述べたように解釈するならば、 α∼β かつ β∼γ ならば α∼γ が成り立つべきである。逆にこれが成り立たないモデルは、「将来～になるだろう」という様相を考える上では不適切である。

このことから、様相論理における恒真式は、ある定められたクラスに属するモデルにおいて妥当であるものとして定義しておくのが都合が良い。

定義 1.5.

モデルから成るクラス 󱁀 をとる。式 A に対して、 ⊨󱁀A が成り立つことを、任意の 󰒤∈󱁀 に対して ⊨󰒤A が成り立つことと定める。このとき、 A は 󱁀 において「妥当 (valid)」もしくは「恒真 (tautological)」であるという。

モデルのクラスとしては、モデルを定める二項関係 ∼ が特定の性質を満たすものの全体を考えることが多い。例えば、「将来～になるだろう」という様相を念頭に置くのであれば、上で述べたように ∼ が推移的であるようなモデル全体のクラスを考えることになる。

さて、ここまでは 1 つの式に注目してそれが妥当かどうかの定義をしたが、ただ 1 つの式に注目することは少なく、特定の形をした式が全て妥当になるかどうかを考えることが多い。そこで、そのための用語も定義しておこう。

定義 1.6.

式の集合を「スキーマ (schema)」という。

定義はこの通りだが、基本的に「スキーマ」といった場合は、特定の形をした式の全体を指すことが多い。例えば、スキーマ Σ をある式 A について ΣA:=◻A⇀⬦A の形で書けるもの全体をとするといった具合である。

スキーマの妥当性は、そのスキーマに属する全ての式が妥当であるとして定義する。

定義 1.7.

モデルから成るクラス 󱁀 をとる。スキーマ Σ に対して、 ⊨󱁀Σ が成り立つことを、任意の式 A∈Σ について ⊨󱁀A が成り立つことと定める。このとき、 Σ は 󱁀 において「妥当 (valid)」もしくは「恒真 (tautological)」であるという。

次回は、一旦あらゆるモデルのクラスで成立する恒真式 (のスキーマ) について触れることにする。その後で、特定のクラスにおける恒真式のうち重要なものに触れる予定である。

参考文献

B. F. Chellas (1980) 『Modal Logic』 Cambridge University Press
P. Blackburn, M. de Rijke, Y. Venema (2001) 『Modal Logic』 Cambridge University Press