日記 (2025 年 3 月 8 日)
我々は 2 月 26 日に、 様相論理の議論を行うためのベースとなる性質として正規性を定義し、 そのようなもののうち最小の体系として K を定式化した。
それから前回まで見てきたように、 正規性だけからでも様々な性質が導かれる。
しかし、 証明することのできる式の量という面では、 K は公理が少なすぎて、 様相として何を念頭に置いているかによっては不十分なことが多い。
そこで、 K に公理をいくつか追加することを考えたい。
追加する公理として最も有名なのが、 2 月 25 日に紹介した D,T,B,4,5 である。
素朴に考えれば、 これらを追加して得られる体系は、 この 5 種類それぞれに入れるか入れないかの選択ができるので、 全部で 25=32 通りのはずである。
しかし、 これら 5 種類のスキーマは互いに完全に独立というわけではなく、 いくつかのスキーマを入れるとそこから別のスキーマが導かれてしまうことがある。
今回は、 このようなスキーマの間の証明可能性の関係について触れていく。
ここで参照用に、 D,T,B,4,5 とその双対 D†,T†,B†,4†,5† の定義を確認しておこう。
各式 A に対して、
DA :≡ ◻A⇀⬦A DA† :≡ ◻A⇀⬦A TA :≡ ◻A⇀A TA† :≡ A⇀⬦A BA :≡ A⇀◻⬦A BA† :≡ ⬦◻A⇀A 4A :≡ ◻A⇀◻◻A 4A† :≡ ⬦⬦A⇀⬦A 5A :≡ ⬦A⇀◻⬦A 5A† :≡ ⬦◻A⇀◻A
であった。
命題 7.6 により、 このうちのあるスキーマを追加するのとその双対を追加するのは同値であることも思い出しておきたい。
最初に示すのは、 公理として T の方が D より強いことである。
命題 8.1.
正規な理論 に対し、
⊢T⟹⊢D
が成り立つ。
証明.
⊢T が成り立っていると仮定する。
この仮定により、 任意の式 A に対し、
⊢◻A⇀A
が成り立つ。
また、 命題 7.6 によって ⊢T† でもあるから、
⊢A⇀⬦A
も成り立つ。
これらに命題 5.1 を使うことで、
⊢◻A⇀⬦A
が得られる。
全ての A に対してこれが得られたので、 すなわち ⊢D が成り立つ。
次に、 B が含まれているという状況のもとでは、 4 と 5 は互いに一方を仮定すればもう一方を導くことができる。
命題 8.2.
正規な理論 に対し、
⊢B,4 ⟹ ⊢5 ⊢B,5 ⟹ ⊢4
がともに成り立つ。
証明.
まず、 ⊢B,4 が成り立っていると仮定する。
任意に式 A をとる。
特に ⊢4 であり、 さらに命題 7.6 によって ⊢4† でもあるから、
⊢⬦⬦A⇀⬦A
が成り立つ。
これと命題 5.2 により、
⊢◻⬦⬦A⇀◻⬦A
も成り立つ。
ここで ⊢B であることから、
⊢⬦A⇀◻⬦⬦A
が成り立つから、 今得られた 2 つの主張に命題 5.1 を適用すれば、
⊢⬦A⇀◻⬦A
が得られる。
A は任意だったから、 これで ⊢5 が示された。
次に、 ⊢B,5 が成り立っていると仮定する。
任意に式 A をとる。
命題 7.6 によって ⊢5† でもあるから、
⊢⬦◻A⇀◻A
が成り立つ。
これと命題 5.2 により、
⊢◻⬦◻A⇀◻◻A
も成り立つ。
ここで ⊢B であることから、
⊢◻A⇀◻⬦◻A
が成り立つから、 今得られた 2 つの主張に命題 5.1 を使えば、
⊢◻A⇀◻◻A
が得られる。
A は任意だったから、 これで ⊢4 が示された。
命題 8.1 で証明したように、 単独では T の方が D より強い。
しかし、 B と 4 がすでに含まれているという状況では、 D の方から T が導けるので、 結果的にこのときは T と D は同値になる。
命題 8.3.
正規な理論 に対し、
⊢D,B,4⟹⊢T
が成り立つ。
証明.
⊢D,B,4 が成り立つと仮定する。
任意に式 A をとる。
まず、 ⊢4 であるから、
⊢◻A⇀◻◻A
が成り立つ。
次に、 ⊢D によって、
⊢◻◻A⇀⬦◻A
が分かる。
さらに、 ⊢B と命題 7.6 によって ⊢B† でもあるから、
⊢⬦◻A⇀A
が成り立つ。
ここまでで得られた 3 つの主張に命題 5.1 を使えば、
⊢◻A⇀A
が得られる。
A は任意だったから、 これで ⊢T が示された。
T と 5 の組み合わせは最も強い。
命題 8.1 によってまず D が導かれることが分かるが、 さらに B と 4 も導くことができる。
命題 8.4.
正規な理論 に対し、
⊢T,5⟹⊢B,4
が成り立つ。
証明.
⊢T,5 が成り立つと仮定する。
まず、 ⊢B を示すため、 任意に式 A をとる。
⊢T と命題 7.6 によって ⊢T† であるから、
⊢A⇀⬦A
が成り立つ。
さらに、 ⊢5 でもあるから、
⊢⬦A⇀◻⬦A
も成り立つ。
ここまでで得られた 3 つの主張に命題 5.1 を使えば、
⊢A⇀◻⬦A
が得られる。
A は任意だったから、 これで ⊢B が示された。
次に、 ⊢4 を示すため、 改めて任意に式 A をとる。
上記により ⊢B が成り立つことが分かっているので、
⊢◻A⇀◻⬦◻A
が成り立つ。
⊢5 と命題 7.6 によって ⊢5† であるから、
⊢⬦◻A⇀◻A
が成り立つが、 これと命題 5.2 により、
⊢◻⬦◻A⇀◻◻A
も得られる。
これと最初の主張に命題 5.1 を使えば、
⊢◻A⇀◻◻A
が得られる。
A は任意だったから、 これで ⊢4 も示された。
以上を、 証明可能性の同値性という形でもまとめておこう。
命題 8.5.
正規な理論 に対し、
⊢T ⟺ ⊢T,D ⊢B,5 ⟺ ⊢B,4 ⊢T,5⟺⊢D,B,4⟺⊢T,B,4
が全て成り立つ。
これにより、 例えば T と D を両方とも追加した体系は、 単に T だけを追加した体系と同型である。
同様に、 B と 4 を追加した体系は、 4 の代わりに 5 を追加した体系と同型である。
さらに、 D もしくは T に加えて B と 4 も追加した体系は、 それら 3 つの代わりに T と 5 を追加した体系と同型である。
これらの関係から同型になる追加パターンを整理していくと、 D,T,B,4,5 の合計 32 通りの追加パターンのうち 17 通りは他のパターンと同型になることが分かる。
残る 15 通りは次の図のように整理できる。
K[T,4]K[T,5]K[T,4]K[T]K[T,B]K[D,4]K[D,4,5]K[D,5]K[D]K[D,B]K[4]K[4,5]K[B,5]K[5]KK[B]
線で繋がっているところには包含関係があり、 上や右に行くほど強い体系である。
例えば、 K[D,4,5] と K[T,5] は線で繋がっていて K[T,5] の方が右上にあるので、 K[D,4,5] で証明可能な式は K[T,5] でも証明可能ということである。
なお、 この段階で分かっているのは、 上記以外のパターンが上記の 15 パターンに帰着することと、 上記の 15 パターンの間に図の通りの包含関係があることだけである。
図が示す包含関係が真の包含であること、 すなわち包含関係のある 2 つの体系のうち一方で証明できて一方では証明できない式が存在することは、 まだ分かっていない。
実際にはこれら 15 パターンは全て相異なるのだが、 その証明は次回行う。
参考文献
- B. F. Chellas (1980) 『Modal Logic』 Cambridge University Press
- P. Blackburn, M. de Rijke, Y. Venema (2001) 『Modal Logic』 Cambridge University Press