日記 (2025 年 3 月 22 日)
今回は、 ついに完全性を証明する。
とはいえ、 その本質的な議論は前回までで終わっているので、 後はそれらをまとめるだけである。
まずは、 正準モデルを定義しよう。
定義 12.1.
正規な理論 をとる。
モデル =(W,∼,P) を以下で定める。
- W は、
W:={Γ∣Γ は -極大整合的集合}
とする。
- ∼ は、 各 Γ,Δ∈W に対して、
Γ∼Δ:⟺◻−1Γ⊆Δ
であるとして定める。
- P は、 各 n∈ に対して、
Pn:={Γ| Γ は -極大整合的集合 pn∈Γ{
であるとして定める。
このとき、 この を による 「正準モデル (canonical model)」 という。
正準モデルでの世界 (すなわち極大整合的集合) における式の妥当性は、 その極大整合的集合への所属関係と同値になる。
命題 12.2.
正規な理論 をとる。
任意の -極大整合的集合 Γ と式 A に対し、
Γ⊨A⟺A∈Γ
が成り立つ。
証明.
A の構造に関する帰納法による。
A≡pn のとき。
Γ⊨pn であるとは Γ∈Pn であるということだが、 定義からこれは pn∈Γ と同値である。
A≡X∧Y のとき。
Γ⊨X∧Y であるとは Γ⊨X と Γ⊨Y がともに成り立つことである。
帰納法の仮定により、 これは X∈Γ かつ Y∈Γ がともに成り立つことと同値である。
ここで命題 11.6 により、 これは X∧Y∈Γ とも同値である。
A が要素式以外の他の形のとき、 すなわち A≡⊤, A≡⊥, A≡¬X, A≡X∨Y, A≡X⇀Y のいずれかで書ける場合も、 命題 11.6 から上記と全く同様に従う。
A≡◻X のときは、 命題 11.12 を使うことでやはり同様に示せる。
A≡⬦X のときは、 命題 11.9 を使うことで Γ,Δ∈W に対して Γ∼Δ が Δ⊆⬦−1Γ と同値にもなることを思い出せば、 同じく命題 11.12 から示せる。
これで全ての場合が尽くされたので、 命題の主張が示された。
これを用いると、 正準モデルでの (世界によらない) 妥当性が、 証明可能性と同値になることが分かる。
命題 12.3.
正規な理論 をとる。
任意の式 A に対し、
⊨A⟺⊢A
が成り立つ。
証明.
⊨A が成り立つことは、 任意の世界 Γ∈W に対して Γ⊨A が成り立つことである。
W の定義と命題 12.2 によって、 これは、 任意の -極大整合的集合 Γ に対して A∈Γ が成り立つことと同値である。
命題 11.8 を使えば、 これが ⊢A と同値であることが分かる。
最後に、 これを用いることで、 完全性を次のように述べることができる。
すなわち、 正規な理論は、 その正準モデルを属するようなモデルのクラスに対して完全である。
定理 12.4.
正規な理論 とモデルのクラス に対し、 ∈ ならば、 任意の式 A に対し、
⊨A⟹⊢A
が成り立つ。
さて、 我々は正規な理論として特に K にいくつかのスキーマを追加したものを考えていて、 その中でもさらに K[D], K[T], K[T,B], K[T,4], K[T,5] の 5 種類が重要であると述べてきた。
これらの体系は、 それぞれ Ser, Refl, Refl∩Sym, Pord, Equiv に対応しており、 この対応するモデルのクラスに対して健全であった。
これは定理 9.4 で示した通りである。
そこで、 これらの体系がそれぞれ対応するモデルのクラスに対して完全でもあることを証明したい。
そのためには、 上記の定理により、 K[D], K[T], K[T,B], K[T,4], K[T,5] の正準モデルがそれぞれ Ser, Refl, Refl∩Sym, Pord, Equiv に属することを示せば良い。
そこで次回は、 上記の 5 種類の体系の正準モデルの性質を調べることにする。
それで完全性に関するトピックは一旦閉じることになる。
参考文献
- B. F. Chellas (1980) 『Modal Logic』 Cambridge University Press
- P. Blackburn, M. de Rijke, Y. Venema (2001) 『Modal Logic』 Cambridge University Press