様相論理のメモ。S4に次の公理Mを加えたものをS4.1という。
- M: □◇P→◇□P
この名称は論理学者マッキンゼーに由来する。S4.1に対応するフレームの条件は、反射性・推移性、そして、終点の存在（endpoint existence）、すなわち
- ∀w∃u [wRu ＆ ∀t(uRt → u=t)]
である。
奇妙なことに、終点の存在というフレーム条件はマッキンゼー式そのものと対応しているわけではないらしい。それどころか、マッキンゼー式に対応するフレーム条件は一階の言語では書けないのだとか。
また、S4.1という名にも関わらず、S4.1はS5の部分システムですらない。MをS5に加えると、"P≡□P" が導出されて、単なる命題論理につぶれるからだ。しかし、Ｍの逆
- ◇□P→□◇P
はギーチの公理と呼ばれ、S4にこれを加えた体系はS4.2と呼ばれる。S4.2はS4.3やS5の部分システムになる。ギーチの公理に対応するフレームの条件は
- wRu ＆ wRt → ∃z[uRz ＆ tRz]
である。
ちなみに、マッキンゼーは様相量化論理の開発者の一人なのだが、同性愛者だったこともあって弾圧されて、自殺したらしい*1。同性愛者であったために酷い目にあったのはチューリングだけではなかったのだ…。
