様相論理

様相論理（ようそうろんり、）は、いわゆる古典論理の対象でない、様相（modal）と呼ばれる「〜は必然的に真」や「〜は可能である」といった必然性や可能性などを扱う論理である（様相論理は、部分の真理値からは全体の真理値が決定されない内包論理の一種と見ることができる）。
その歴史は古くアリストテレスまで遡ることができるが、形式的な扱いは数理論理学以降、非古典論理としてである。
様相論理では一般に、標準的な論理体系に「～は必然的である」ことを意味する必然性演算子□と、「～は可能である」ことを意味する可能性演算子◇のふたつの演算子が追加される。
真理論的様相と認識論的様相.
様相論理は真理論的（形而上学的、論理的）様相の文脈で語られることが最も多い。この様相においては「～は必然的である」、「～は可能である」といった言明が扱われるが、これは認識論的様相と混同されやすい。
例えば「雪男は存在しているはずがない」という主張と、「雪男が存在することは可能である」という主張は、矛盾無く行うことが可能である。この場合、前者は認識論的様相であり、「（これまでの情報からして）雪男が実際に存在するとは考えられない」という主張とみなしうる。一方、後者は真理論的様相であり「（実際には存在しないのだが）雪男が存在することは可能である」という主張であると解釈することができる。
あるいは、「ゴールドバッハ予想は正しいかもしれないし、正しくないかもしれない」という言明も認識論的である。これは現時点の知識では正しいかどうか分からないということであり、仮にゴールドバッハ予想の証明が存在し、その方法に気付いていないだけだとすれば、真理論的には「正しくないかもしれない」という主張は誤りであることになる。
これ以外の様相としては、時間的なものがある。例えば、「明日雨が降るかどうかは決まっていない」のに対し、「昨日雨が降ったかどうかは決まっている」と考えられる。このようなナイーヴな時間観には同意しない哲学者も多いが、その構造は様相論理によって把握することができる。
さらに「～べきではない」「～してもよい」といった義務に関わる命題も様相論理によって扱うことができる。直感的にも、「～べきではない」と「～してもよい」の関係は「～は必然的である」と「～は可能である」の関係と極めて類似している。義務表現を扱う様相論理は義務論理と呼ばれる。
様相論理の公理系.
様相論理には様々な公理系が考えられており、どのような公理系が妥当なのかはそれ自体が論争の的である。二つの様相演算子のあいだにド・モルガンの法則的な関係が成立することは、どの公理系でも共通している。□は必然性演算子、◇は可能性演算子である。
即ち、「必然的に真」は「偽である可能性がない」と同等であり、「真である可能性がある」は「必然的に偽であるわけではない」と同等である。
様相論理としての最低限の定義 ◇p=￢□￢p のみを満たす最小の公理系としては、E という公理系が知られている。これは古典命題論理に以下の推論規則を加えたものである。
この公理系 E より「強い」すべての公理系は、Classical な公理系と呼ばれる。
しかしながら、真と認めるべきかどうか直感的に明らかでない論理式も多く作ることができる。例えば「必然的に真ならば必然的に「必然的に真」である」と言えるのかどうか、即ち □p→□□p が成り立つのかどうかは、はっきりしない。こういった定理を認めるか否かによって、様々な公理系が生まれる。
必然化規則を満たす公理系（Normal な公理系）の中で、最も「小さな」公理系として知られているのは、クリプキによる K という公理系である。K の公理系に更に公理を付け加えることにより、様々な様相論理が得られる
K の公理系.
K の公理系は古典命題論理の公理系に公理図式K
（太字になっていることに注意）
と必然化規則（necessitation）を付け加えたものである。
ここで可能性演算子は定義 ◇p=￢□￢p によって導入される。
T の公理系.
K の公理系に以下の公理図式T「必然的に真ならば、真である」を加えた体系は T と呼ばれる。
T においては、K では証明可能でなかった P→◇P などが証明可能となる。
S4, S5の公理系.
公理系K,Tにおいては以下の1–4の同値性を証明できないために多重の様相（◇◇, □□, ◇□, □◇, □□□, …）
を減らすことができない。従って無限に多くの様相が区別されることになる。
これらは還元法則と呼ばれるが、右辺→左辺はTで証明可能なので、1–4の左辺→右辺の内、どれを公理系T に付け加えるかで S4, S5 の違いが生まれる。
実は、還元法則の1を仮定すれば、Tの下で2–4は証明可能となる。一方3を仮定すれば4がTで証明可能だが、2は証明可能でない。従ってS5はS4より真に強い（証明力の強い）公理系である。還元法則の導入により本質的に区別される様相はS4で7種類、S5で3種類と実際に減少する。
クリプキはこの S5 に非常に単純な意味論が当てはまることを示した（下の#様相論理の意味論参照）。しかし実際には、議論の目的によって適切な公理系は異なる。例えば、真理論的様相に関しては S5 が最も適当だが、認識論的様相では S4 という公理系が適切であると考えられている。
様相論理の意味論.
様相論理の意味論としてはソール・クリプキによって与えられたクリプキ意味論と呼ばれる体系があり、それと関係するよく知られたアイディアとして可能世界論がある。上で見た公理系のバリエーションは、可能世界のあいだの二項関係として定義される到達可能性の概念によって捉えることができる。なお、可能世界という概念をどう解釈すべきかを巡っては、哲学上の議論も盛んである。
命題様相論理の意味論の概要は以下の通りである。
"W"を空でない集合とする。これは個々の可能世界全体の集合を表していると考えられる。次に"W"上の二項関係"R"を考える。つまりformula_14である。またformula_15 を formula_16と表す。"R"は"W"上の到達関係と呼ばれ、様相演算子の付いた論理式の真偽に影響する。また"PV"を命題変数全体の集合とし、この"PV"と先に定義したWに対し、関数Vを
として定義する（formula_18は"W"の冪集合、すなわち部分集合全体の集合である）。これは、ある原子命題について、それが真である可能世界の集合を与える解釈である。すなわち、可能世界"w"において原子命題"p"が真であることをformula_19として表す。このように定義された順序三組〈"W", "R", "V"〉を解釈（もしくはクリプキモデル）と呼ぶ。
さて、解釈"V"を以下のように論理式全体に再帰的に拡張する。"A"、"B"を任意の論理式、"w"を"W"の任意の要素とする。
命題論理の結合子については古典命題論理と全く同じであるが、様相演算子については、可能世界と到達関係を持つ別の可能世界を考える必要がある。任意のクリプキモデル〈"W", "R", "V"〉の全てのformula_35でformula_36の時、AはK（クリプキに因む）で恒真であると言う。ルイスの公理系の一部の意味論は到達関係"R"に制限（二項関係の制限について詳しくは集合上の関係を参照）を加えることにより作ることが出来る。例えば"S5"で"A"が証明可能なのは、反射的かつ対称的かつ推移的であるという制限を"R"に加えた全てのクリプキモデルの全ての世界で"A"が真である時であり、その時のみである。同様に"S4"は反射的かつ推移的という制限を加える。
次に「非正規世界」（non-normal worlds）を導入する。"W"を空でない集合、"N"を"W"の部分集合、他"R"及び"v"は上と同様に定義する。この時、順序四組〈"W", "N", "R", "V"〉が非正規様相論理における解釈である。"v"は、命題論理の結合子については、全てのformula_35で上記と同様に拡張される。様相演算子については、正規世界"N"においては上記と全く同じだが、非正規世界"W" - "N（WのうちでNに含まれない世界全ての集合）"においては異なる。
いわば、非正規世界では定義的に（到達関係と関係なく）全ての可能命題が真であり、全ての必然命題が偽である。Aが恒真であるとは全ての解釈〈"W", "N", "R", "V"〉の下で全てのformula_41に対しformula_36であることを言う。非正規様相論理の解釈の到達関係"R"に反射的であるという制限を加えると"S2"、反射的かつ推移的という制限を加えると"S3"の意味論となる。
公理系S4の位相的意味論では、原子命題達を位相空間の中の図形と解釈する。ここでは様相演算子 □ と ◇ は、それぞれ開核作用素と閉包作用素に解釈される。代数的意味論では、原子命題達を位相ブール代数の元と解釈する。
様相論理の歴史.
アリストテレスの論理学は大部分がいわゆる三段論法に関わるものであり、古典論理の枠内で扱えるものであるが、有名な "De Interpretatione" （『命題論』）の海戦問題のように、時間と可能性に関わる発展的な議論も行っている。スコラ哲学では主に本質（essence）と付随的な性質（accident）の区別について、厳密な論理が展開された。中世の思想家の中で、様相論理に関わる重要な仕事をした人物としてはオッカムのウィリアム、ヨハネス・ドゥンス・スコトゥスが挙げられる。
今日の様相論理は、1918年の著書 "A Survey of Symbolic Logic" のなかで S1–S5 の公理系を導入した C・I・ルイスに始まる。1933年にはクルト・ゲーデルにより、必然性演算子□を基準とした方法で S4 が定義された。J・C・C・マッキンゼーは1941年に代数的方法を用いてルイスの S2 と S4 の体系の決定可能性を証明した。
様相論理に対しての意味論は様々な形で考えられてきたが、1963年にソール・クリプキにより提唱されたクリプキ意味論（可能世界意味論とも）は、様々な様相論理の体系に対して完全性定理が成り立つことが示され、様相論理を飛躍的に前進させた。
様相論理から派生した論理体系としては、従来の演算子に代わり、それぞれ過去・未来の到達可能性を示す様相演算子P・Fを導入する時相論理や、従来の様相演算子□、◇にラベル付けを施した動的論理などがある。これらは認知現象の解析や計算機科学への応用など、目的に応じて様々に考案され、適用されている。