様相論理

様相論理（ようそうろんり、英: modal logic）は、いわゆる古典論理の対象でない、様相（modal）と呼ばれる「〜は必然的に真」や「〜は可能である」といった必然性や可能性などを扱う論理である（様相論理は、部分の真理値からは全体の真理値が決定されない内包論理の一種と見ることができる）。 その歴史は古くアリストテレスまで遡ることができるが、形式的な扱いは数理論理学以降、非古典論理としてである。 様相論理では一般に、標準的な論理体系に「～は必然的である」ことを意味する必然性演算子□と、「～は可能である」ことを意味する可能性演算子 ◇ のふたつの演算子が追加される。 様相論理は真理論的（形而上学的、論理的）様相の文脈で語られることが最も多い。この様相においては「～は必然的である」、「～は可能である」といった言明が扱われるが、これは認識論的様相と混同されやすい。 例えば「雪男は存在しているはずがない」という主張と、「雪男が存在することは可能である」という主張は、矛盾無く行うことが可能である。この場合、前者は認識論的様相であり、「（これまでの情報からして）雪男が実際に存在するとは考えられない」という主張とみなしうる。一方、後者は真理論的様相であり「（実際には存在しないのだが）雪男が存在することは可能である」という主張であると解釈することができる。 あるいは、「ゴールドバッハ予想は正しいかもしれないし、正しくないかもしれない」という言明も認識論的である。これは現時点の知識では正しいかどうか分からないということであり、仮にゴールドバッハ予想の証明が存在し、その方法に気付いていないだけだとすれば、真理論的には「正しくないかもしれない」という主張は誤りであることになる。 これ以外の様相としては、時間的なものがある。例えば、「明日雨が降るかどうかは決まっていない」のに対し、「昨日雨が降ったかどうかは決まっている」と考えられる。このようなナイーヴな時間観には同意しない哲学者も多いが、その構造は様相論理によって把握することができる。 さらに「～べきではない」「～してもよい」といった義務に関わる命題も様相論理によって扱うことができる。直感的にも、「～べきではない」と「～してもよい」の関係は「～は必然的である」と「～は可能である」の関係と極めて類似している。義務表現を扱う様相論理は義務論理と呼ばれる。 様相論理には様々な公理系が考えられており、どのような公理系が妥当なのかはそれ自体が論争の的である。二つの様相演算子のあいだにド・モルガンの法則的な関係が成立することは、どの公理系でも共通している。□ は必然性演算子、◇ は可能性演算子である。 ◻ p ↔ ¬ ◊ ¬ p {\displaystyle \Box p\leftrightarrow \neg \Diamond \neg p} ◊ p ↔ ¬ ◻ ¬ p {\displaystyle \Diamond p\leftrightarrow \neg \Box \neg p} 即ち、「必然的に真」は「偽である可能性がない」と同等であり、「真である可能性がある」は「必然的に偽であるわけではない」と同等である。 様相論理としての最低限の定義◇p=￢□￢pのみを満たす最小の公理系としては、E という公理系が知られている。これは古典命題論理に以下の推論規則を加えたものである。 推論規則 : φ ↔ ψ {\displaystyle \varphi \leftrightarrow \psi } が成り立つならば、 ◻ φ ↔ ◻ ψ {\displaystyle \Box \varphi \leftrightarrow \Box \psi } も成り立つ。 この公理系 E より「強い」すべての公理系は、Classical な公理系と呼ばれる。 しかしながら、真と認めるべきかどうか直感的に明らかでない論理式も多く作ることができる。例えば「必然的に真ならば必然的に「必然的に真」である」と言えるのかどうか、即ち□p→□□pが成り立つのかどうかははっきりしない。こういった定理を認めるか否かによって様々な公理系が生まれる。 必然化規則を満たす公理系（Normal な公理系）の中で、最も「小さな」公理系として知られているのはクリプキによる K という公理系であり、K の公理系に更に公理を付け加えることにより、様々な様相論理が得られる 。 K の公理系は古典命題論理の公理系に公理図式K （太字になっていることに注意） と必然化規則（necessitation）を付け加えたものである。 公理K : ◻ ( A → B ) → ( ◻ A → ◻ B ) {\displaystyle \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)} 必然化規則 : A が K で証明可能ならば、 ◻ A {\displaystyle \Box A} も成り立つ。 ここで可能性演算子は定義◇p=￢□￢pによって導入される。 K の公理系に以下の公理図式T「必然的に真ならば、真である」を加えた体系は T と呼ばれる。 公理T : ◻ A → B {\displaystyle \Box A\rightarrow B} T においては、K では証明可能でなかったP→◇Pや◇(P→□P)が証明可能となる。 公理系K,Tにおいては以下の1～4の同値性を証明できないために多重の様相（◇◇,□□,◇□,□◇,□□□…） を減らすことができない。従って無限に多くの様相が区別されることになる。 ◊ P ↔ ◻ ◊ P {\displaystyle \Diamond P\leftrightarrow \Box \Diamond P} ◻ P ↔ ◊ ◻ P {\displaystyle \Box P\leftrightarrow \Diamond \Box P} ◊ P ↔ ◊ ◊ P {\displaystyle \Diamond P\leftrightarrow \Diamond \Diamond P} ◻ P ↔ ◻ ◻ P {\displaystyle \Box P\leftrightarrow \Box \Box P} これらは還元法則と呼ばれるが右辺→左辺はTで証明可能なので、 1～4の左辺→右辺の内、どれを公理系T に付け加えるかでS4,S5の違いが生まれる。 公理4 : ◻ A → ◻ ◻ A {\displaystyle \Box A\rightarrow \Box \Box A} （還元法則の4に対応）をTに付け加えたのがS4である。 公理5 : ◊ A → ◻ ◊ A {\displaystyle \Diamond A\rightarrow \Box \Diamond A} （還元法則の1に対応）をTに付け加えたのがS5である。 実は、還元法則の1を仮定すれば、Tの下で2～4は証明可能となる。一方3を仮定すれば4がTで証明可能だが、 2は証明可能でない。従ってS5はS4より真に強い（証明力の強い）公理系である。 還元法則の導入により本質的に区別される様相はS4で7種類、S5で3種類と実際に減少する。 クリプキはこの S5 に非常に単純な意味論が当てはまることを示した（下の様相論理の意味論参照）。しかし実際には、議論の目的によって適切な公理系は異なる。例えば、真理論的様相に関しては S5 が最も適当だが、認識論的様相では S4 という公理系が適切であると考えられている。 様相論理の意味論としてはソール・クリプキによって与えられたクリプキ意味論と呼ばれる体系があり、それと関係するよく知られたアイディアとして可能世界論がある。上で見た公理系のバリエーションは可能世界のあいだの二項関係として定義される到達可能性の概念によって捉えることができる。なお可能世界という概念をどう解釈すべきかを巡っては哲学上の議論も盛んである。 命題様相論理の意味論を簡単に見てみよう。Wを空でない集合、PVを命題変数全体の集合、vを v : W × P V → { 0 , 1 } {\displaystyle v:W\times PV\rightarrow \{0,1\}} である関数とする。Wは可能世界全体の集合と考えると、vは特定の可能世界で命題変数の真偽を与える解釈である。次にW上の二項関係Rを考える。つまり R ⊆ W 2 {\displaystyle R\subseteq W^{2}} である。RはW上の到達関係と呼ばれ、様相演算子の付いた論理式の真偽に影響する。このように定義された順序三組<W,R,V>を解釈（もしくはクリプキモデル）と呼ぶ。以下 v ( ⟨ w , p ⟩ ) {\displaystyle v(\langle w,p\rangle )} （世界wにおける命題変数pの真偽を表す） を単に v w ( p ) {\displaystyle v_{w}(p)} と、 ⟨ w , w ′ ⟩ ∈ R {\displaystyle \langle w,w'\rangle \in R} を w R w ′ {\displaystyle _{w}R_{w'}} と表す。解釈vを以下のように論理式全体に再帰的に拡張する。A、Bを任意の論理式、wをWの任意の要素とする。 v w ( ¬ A ) = 1 ⇔ v w ( A ) = 1 {\displaystyle v_{w}(\neg A)=1\Leftrightarrow v_{w}(A)=1} v w ( A ∧ B ) = 1 ⇔ v w ( A ) = 1 {\displaystyle v_{w}(A\land B)=1\Leftrightarrow v_{w}(A)=1} かつ v w ( B ) = 1 {\displaystyle v_{w}(B)=1} v w ( A ∨ B ) = 1 ⇔ v w ( A ) = 1 {\displaystyle v_{w}(A\lor B)=1\Leftrightarrow v_{w}(A)=1} または v w ( B ) = 1 {\displaystyle v_{w}(B)=1} v w ( A ⊃ B ) = 1 ⇔ v w ( A ) = 0 {\displaystyle v_{w}(A\supset B)=1\Leftrightarrow v_{w}(A)=0} または v w ( B ) = 1 {\displaystyle v_{w}(B)=1} v w ( ◻ A ) = 1 ⇔ {\displaystyle v_{w}(\Box A)=1\Leftrightarrow } 全ての w R w ′ {\displaystyle _{w}R_{w'}} である w ′ ∈ W {\displaystyle w'\in W} について v w ( A ) = 1 {\displaystyle v_{w}(A)=1} v w ( ◊ A ) = 1 ⇔ {\displaystyle v_{w}(\Diamond A)=1\Leftrightarrow } ある w R w ′ {\displaystyle _{w}R_{w'}} である w ′ ∈ W {\displaystyle w'\in W} において v w ( A ) = 1 {\displaystyle v_{w}(A)=1} 命題論理の結合子については古典命題論理と全く同じである。任意のクリプキモデル<W,R,V>の全ての w ∈ W {\displaystyle w\in W} で v w ( A ) = 1 {\displaystyle v_{w}(A)=1} の時、AはK（クリプキに因む）で恒真であると言う。ルイスの公理系の一部の意味論は到達関係Rに制限（二項関係の制限について詳しくは集合上の関係を参照）を加えることにより作ることが出来る。例えばS5でAが証明可能なのは、反射的かつ対称的かつ推移的であるという制限をRに加えた全てのクリプキモデルの全ての世界でAが真である時であり、その時のみである。同様にS4は反射的かつ推移的という制限を加える。 次に「非正規世界」（non-normal worlds）を導入する。Wを空でない集合、NをWの部分集合、他R及びvは上と同様に定義する。この時、順序四組<W,N,R,V>が非正規様相論理における解釈である。vは命題論理の結合子については全ての w ∈ W {\displaystyle w\in W} で上記と同様に拡張される。様相演算子については正規世界Nにおいては上記と全く同じだが、非正規世界W-N（WのうちでNに含まれない世界全ての集合）においては異なる。 全ての w ∈ W − N {\displaystyle w\in W-N} で v w ( ◊ A ) = 1 {\displaystyle v_{w}(\Diamond A)=1} 且つ v w ( ◻ A ) = 0 {\displaystyle v_{w}(\Box A)=0} である。 いわば、非正規世界では定義的に（到達関係と関係なく）全ての可能命題が真であり、全ての必然命題が偽である。Aが恒真であるとは全ての解釈<W,N,R,V>の下で全ての w ∈ N {\displaystyle w\in N} に対し v w ( A ) = 1 {\displaystyle v_{w}(A)=1} であることを言う。非正規様相論理の解釈の到達関係Rに反射的であるという制限を加えるとS2、反射的かつ推移的という制限を加えるとS3の意味論となる。 公理系S4の位相的意味論では、原子命題達を位相空間の中の図形と解釈する。ここでは様相演算子 ◻ {\displaystyle \square } と ◇ はそれぞれ開核作用素と閉包作用素に解釈される。代数的意味論では、原子命題達を位相ブール代数の元と解釈する。 アリストテレスの論理学は大部分がいわゆる三段論法に関わるものであり、古典論理の枠内で扱えるものであるが、有名な De Interpretatione （『命題論』）の海戦問題のように、時間と可能性に関わる発展的な議論も行っている。スコラ哲学では主に本質（essence）と付随的な性質（accident）の区別について、厳密な論理が展開された。中世の思想家の中で、様相論理に関わる重要な仕事をした人物としてはオッカムのウィリアム、ヨハネス・ドゥンス・スコトゥスが挙げられる。 今日の様相論理は、1918年の著書 A Survey of Symbolic Logic のなかで S1 - S5 の公理系を導入した C・I・ルイスに始まる。J・C・C・マッキンゼーは1941年に代数的方法を用いてルイスの S2 と S4 の体系の決定可能性を証明した。ソール・クリプキは1959年、1963年にクリプキ意味論を導入し、様相論理を飛躍的に前進させた。 A・N・プライアーは様相論理に未来演算子 F と過去演算子 P を加えた時制論理を作り出した。このほかにもコンピュータサイエンスへの応用など、目的に応じて様々な論理が提案されている。 ^ 序説(2010) p.138 ^ 以下のK,T,S4,S5の公理系については戸田山(2000)p306-310に拠った。 ^ Priest(2008) p36-35 ^ Priest(2008) p64-65 古森 雄一, 小野 寛晰 (2010). 現代数理論理学序説. 日本評論社.  戸田山和久 (2000). 論理学をつくる. 名古屋大学出版会.  Moshe Y.Vardi (2002), Branching vs. Linear Time: Final Showdown, https://www.cs.rice.edu/~vardi/papers/etaps01-ver13.pdf  Graham Priest (2008), An Introduction to Non-Classical Logic (2 ed.), Cambridge University Press  認識論理 義務論理 時相論理 - 線形時相論理 直観主義理論 ソール・クリプキ 吉満昭宏 「C.I.ルイスと様相論理の起源」 科学哲学 Vol.37 , No.1(2004) pp.1-14 Modal Logic （英語） - スタンフォード哲学百科事典「様相論理」の項目。（英語）