日記 (2025 年 3 月 3 日)
今回は、 全ての正規な理論で証明できる式について触れる。
まずは、 命題 2.4 の意味論版を証明する。
命題 5.1.
正規な理論 をとる。
式 A1,⋯,An(n≥0) と式 B に対し、 A1∧⋯∧An⇀B が命題論理的恒真であれば、
⊢A1AND⋯AND⊢An⟹⊢B
が成り立つ。
証明.
まず、 A1∧⋯∧An⇀B が命題論理的恒真であるということは、 A1⇀(A2⇀(⋯(An⇀B)⋯)) が命題論理的恒真であるということである。
したがって、
⊢A1⇀(A2⇀(⋯(An⇀B)⋯))
が成り立つ。
ここで、 ⊢A1 から ⊢An までを全て仮定すれば、 規則 MP を n 回適用することで、 ⊢B を導くことができる。
この命題は大変重要で、 以降息をするように使う。
今後 「命題 5.1 により」 と言って式変形を何度も行うが、 そのときは変形前の式と変形後の式を ⇀ で結んだ式が命題論理的恒真であることを確かめれば良い。
特に断りがなければ、 その恒真性は明らかである。
次に、 命題 2.8 の演繹体系版を証明する。
証明はほとんどパラレルにできる。
命題 5.2.
正規な理論 をとる。
式 A1,⋯,An(n≥0) と式 B に対し、
⊢A1∧⋯∧An⇀B⟹⊢◻A1∧⋯∧◻An⇀◻B
が成り立つ。
特に、 式 A,B に対し、
⊢A⇀B⟹⊢◻A⇀◻B
が成り立つ。
証明.
n に関する帰納法による。
n=0 のとき。
示すべきは、
⊢⊤⇀B⟹⊢⊤⇀◻B
である。
そこで、 ⊢⊤⇀B を仮定する。
ここで、 ⊤ は命題論理的恒真だから ⊢⊤ が成り立つので、 これと前の式に規則 MP を適用することで ⊢B が分かり、 さらにこれに規則 RN を適用すれば ⊢◻B が得られる。
ここで、 ◻B⇀(⊤⇀◻B) は命題論理的恒真だから、 命題 5.1 によって ⊢⊤⇀◻B が得られる。
n≥1 のとき。
帰納法の仮定と、
⊢A1∧⋯∧An⇀B
が成り立つことを仮定する。
すると、 命題 5.1 により、
⊢A1∧⋯∧An−1⇀(An⇀B)
が成り立つ。
これに帰納法の仮定を用いれば、
⊢◻A1∧⋯∧◻An−1⇀◻(An⇀B)
が得られる。
さて、 が K を含むことから、
⊢◻(An⇀B)⇀(◻An⇀◻B)
が成り立つので、 今得られた 2 つの式に命題 5.1 を使うことで、
⊢◻A1∧⋯∧◻An−1⇀(◻An⇀◻B)
が分かる。
再び命題 5.1 を使えば、
⊢◻A1∧⋯∧◻An⇀◻B
が示された。
次の命題も重要である。
命題 5.3.
正規な理論 をとる。
式 A,B に対し、
⊢A⥎B⟹⊢◻A⥎◻B
が成り立つ。
証明.
⊢A⥎B が成り立つと仮定する。
すると、 命題 5.1 により、 ⊢A⇀B と ⊢B⇀A がともに成り立つ。
このそれぞれに命題 5.2 を使うことで、 ⊢◻A⇀◻B と ⊢◻B⇀◻A が得られる。
この 2 つに命題 5.1 を使えば、 ⊢◻A⥎◻B が分かる。
命題 5.2 と命題 5.3 は ◻ に関する主張であるが、 同様の主張が ⬦ に関しても成り立つ。
命題 5.4.
正規な理論 をとる。
式 A と式 B1,⋯,Bn(n≥0) に対し、
⊢A⇀B1∨⋯∨Bn⟹⊢⬦A⇀⬦B1∨⋯∨⬦Bn
が成り立つ。
特に、 式 A,B に対し、
⊢A⇀B⟹⊢⬦A⇀⬦B
が成り立つ。
証明.
まず、
⊢A⇀B1∨⋯∨Bn
を仮定する。
すると、 命題 5.1 により、
⊢¬B1∧⋯∧¬Bn⇀¬A
が分かる。
これに命題 5.2 を適用すると、
⊢◻¬B1∧⋯∧◻¬Bn⇀◻¬A
が得られる。
再び命題 5.1 を使えば、
⊢¬◻¬A⇀¬◻¬B1∨⋯∨¬◻¬Bn
が分かる。
さて、 が Dual⬦ を含むことから ⊢⬦A⥎¬◻¬A 等が成り立つので、 これと上の式に命題 5.1 を適用することで、
⊢⬦A⇀⬦B1∨⋯∨⬦Bn
が示された。
命題 5.5.
正規な理論 をとる。
式 A,B に対し、
⊢A⥎B⟹⊢⬦A⥎⬦B
が成り立つ。
次に、 ◻ は ∧ に関して分配的であることを示そう。
命題 5.6.
正規な理論 をとる。
式 A1,⋯,An に対し、
⊢◻(A1∧⋯∧An)⥎◻A1∧⋯∧◻An
が成り立つ。
証明.
命題 5.1 により、
⊢◻(A1∧⋯∧An)⇀◻A1∧⋯∧◻An ⊢◻A1∧⋯∧◻An⇀◻(A1∧⋯∧An)
がともに成り立つことを示せば良い。
まず 1 つ目を示す。
命題論理的恒真性により、 ⊢A1∧⋯∧An⇀A1 から ⊢A1∧⋯∧An⇀An までが全て成り立つ。
これに命題 5.2 を適用すれば、 ⊢◻(A1∧⋯∧An)⇀◻A1 から ⊢◻(A1∧⋯∧An)⇀◻An までが得られる。
これらと命題 5.1 により、
⊢◻(A1∧⋯∧An)⇀◻A1∧⋯∧◻An
が分かる。
次に 2 つ目を示す。
命題論理的恒真性により、
⊢A1∧⋯∧An⇀A1∧⋯∧An
が成り立つ。
これに命題 5.2 を適用すれば、 そのまま
⊢◻A1∧⋯∧◻An⇀◻(A1∧⋯∧An)
が分かる。
双対的に、 ⬦ は ∨ に関して分配的である。
命題 5.7.
正規な理論 をとる。
式 A1,⋯,An に対し、
⊢⬦A1∨⋯∨⬦An⥎⬦(A1∨⋯∨An)
が成り立つ。
他にも重要な恒真式は様々あり、 Chellas†1 の 4.1 節の演習問題でたくさん取り上げられている。
しかしこの勉強ノートでは、 一旦この辺りにしておいて、 他のものは必要に応じて取り上げていくことにする。
次回は、 同値な式による書き換えについて触れる予定である。
参考文献
- B. F. Chellas (1980) 『Modal Logic』 Cambridge University Press
- P. Blackburn, M. de Rijke, Y. Venema (2001) 『Modal Logic』 Cambridge University Press