S5（様相論理）

論理学と哲学において、S5はクラレンス・アーヴィング・ルイスとクーパー・ハロルド・ラングフォードが1932年の著書『記号論理学』で提唱した 5つの様相論理体系の1つである。これは通常の様相論理であり、あらゆる種類の様相論理体系の中で最も古いものの1つである。命題論理式とトートロジー、そして代入とモーダス・ポネンスによる推論装置で構成されているが、構文には必然的に様相演算子が追加されている。${\displaystyle \Box }$そしてその双対は${\displaystyle \Diamond }$[ ^{1 ] [ 2 ]​}

以下では、モーダル演算子を使用します。${\displaystyle \Box }$（「必然的に」）${\displaystyle \Diamond }$（「可能性あり」）

S5は以下の公理によって特徴づけられる。

• K：${\displaystyle \Box (A\to B)\to (\Box A\to \Box B)}$;
• T：${\displaystyle \Box A\to A}$、

そして以下のいずれか：

• 5 :${\displaystyle \Diamond A\to \Box \Diamond A}$;
• または以下の両方: ^{[ 3 ]}

• 4 :${\displaystyle \Box A\to \Box \Box A}$、 そして
• B：${\displaystyle A\to \Box \Diamond A}$。

（５）公理はアクセス可能性関係を制限する${\displaystyle R}$クリプキフレームがユークリッド的である、つまり${\displaystyle (wRv\land wRu)\implies vRu}$それによって、冪等性の下で必然性と可能性を混同することになる。

クリプキ意味論の観点から言えば、S5は、アクセス可能性関係が同値関係であるフレームによって特徴付けられます。つまり、反射的、推移的、対称的です。

S5 式の充足可能性を判定することはNP 完全問題です。S5 には命題論理が含まれているため、困難性の証明は自明です。充足可能な式には、式のサイズに対して世界の数が最大で線形であるようなクリプキ モデルが存在することを示すことで、メンバーシップが証明されます。

S5は、異なる種類の修飾語の不必要な繰り返しを避けることができるため便利です。たとえば、S5では、Xが必然的に、おそらく、必然的に、おそらく真である場合、Xはおそらく真です。最後の「おそらく」より前の太字でない修飾語はS5で削除されます。これは命題を適度に短く保つのに役立ちますが、S5では何かがおそらく必要であれば、それは必要であるという点で、直感に反するように見えるかもしれません。

アルヴィン・プランティンガは、S5のこの特徴は実際には直感に反するものではないと主張している。それを正当化するために、彼は、Xが必然的であるならば、少なくとも一つの可能​​世界では必然的である。したがって、すべての可能世界で必然的であり、すべての可能世界で真である、と論じている。このような推論は、存在論的証明の「様相」的定式化の根底にある。

S5は、${\displaystyle \Diamond \dashv \Box }$[ ^{4 ]​}

ライプニッツはこの公理を用いて神の存在に関する存在論的証明を提唱した。彼の言葉を借りれば、「必然的存在が可能であれば、それは実際に存在することになる」 ^{[ 5 ] 。}

S5は聖トマス・アクィナスの形而上学、特に五つの道のための様相体系でもある。^{[ 6 ]}

しかし、これらのアプリケーションでは、各演算子が単一のモダリティの直列配置にあることが必要です。^{[ 7 ]}マルチモーダル論理、例えば「X は（認識的モダリティにおいて、個人のデータによれば）必然的である可能性がある（真理的モダリティにおいて）」という場合、少なくとも 1 つの認識的に可能な世界で X が必然的であるということは、すべての認識的に可能な世界で X が必然的であることを意味するとはもはや言えません。これは、ある必然的実体を提案することが、それが実在することを意味するわけではないという直観と一致します。

• モーダルロジック
• 通常のモーダルロジック
• クリプキ意味論

• http://home.utah.edu/~nahaj/logic/structures/systems/s5.html 2006年4月22日にWayback Machineにアーカイブされました
• スタンフォード哲学百科事典の様相論理学