S4, S5の公理系
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/02/24 05:07 UTC 版)
公理系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 という公理系が適切であると考えられている。
※この「S4, S5の公理系」の解説は、「様相論理」の解説の一部です。
「S4, S5の公理系」を含む「様相論理」の記事については、「様相論理」の概要を参照ください。
- S4, S5の公理系のページへのリンク