来週はオンライン、不完全定理
開式かと意味論と証明論をやっておけば単位は取れそう
- 記号化
- この推論は妥当か?
- モデル
- 証明
命題論理の完全性定理(続き)
Lemma 4(復習:矛盾から証明へ)
Γ ∪ {¬A} が矛盾 → Γ ⊢ A
Γ ∪ {A} が矛盾 → Γ ⊢ ¬A
証明のカン所:
- RAA(背理法)と→I を使って ¬A や A を導く
- 例:¬A を仮定して⊥を導けば、RAAでAが出る
極大無矛盾集合
Definition: Γ* が極大無矛盾とは
- Γ* は無矛盾
- かつ、Γ* ⊆ Γ で Γ が無矛盾なら Γ* = Γ
つまり「これ以上大きくすると矛盾しちゃうギリギリの無矛盾集合」。
Lemma 5(リンデンバウムの補題)
主張: 任意の無矛盾集合 Γ は、ある極大無矛盾集合 Γ* に含まれる
構成法(ステップ)
-
すべての命題を列挙する:A0, A1, A2, …
(命題は可算無限個しかないので可能) -
集合列 Γn を帰納的に定義:
- Γ0 = Γ
- Γn+1 =
- Γn ∪ {An} (もし Γn ∪ {An} が無矛盾なら)
- Γn (それ以外)
-
Γ* = ∪_{n≥0} Γn (全部の和集合)
証明のポイント
(a) 各 Γn は無矛盾:nに関する帰納法。Γnが無矛盾なら、Γn+1の定義から明らか。
(b) Γ は無矛盾*:
- もし Γ* ⊢ ⊥ なら、⊥の証明には有限個の仮定しか現れない
- その有限個の仮定は全部ある Γn に含まれる
- すると Γn ⊢ ⊥ → Γnが無矛盾に矛盾!
(c) Γ は極大無矛盾*:
- Γ* ⊆ Δ で Δ が無矛盾とする
- B ∈ Δ なら B = Am となるmがある
- Γm ⊆ Γ* ⊆ Δ で Δ は無矛盾だから、Γm ∪ {Am} も無矛盾
- 定義より Γm+1 = Γm ∪ {Am} なので Am ∈ Γm+1 ⊆ Γ*
- よって Δ ⊆ Γ* → Δ = Γ*
💡 有限性がキモ! 「証明は有限列」という性質が、Γ* の無矛盾性を保証してる。無限の和集合を取っても、矛盾の証明は有限ステップで届く範囲に収まるから大丈夫。
Lemma 6(極大無矛盾集合は閉じている)
主張: Γ が極大無矛盾なら、証明可能性について閉じている:
証明(背理法):
- Γ ⊢ A とする。もし A ∉ Γ なら…
- Γ は Γ ∪ {A} の真部分集合
- Γ は極大無矛盾だから、Γ ∪ {A} は矛盾していなければならない
- でも Γ ⊢ A だから Γ ∪ {A} でも A は証明できる
- しかも Γ ∪ {A} は Γ の全仮定を含む
- → Γ ∪ {A} ⊢ ⊥ となって、Γ が無矛盾なことに反する
- よって A ∈ Γ
💡 直観的には「極大無矛盾=ギリギリまで膨らんだ集合」だから、証明できるものは全部入ってるはず、という話。
ここまでの流れ
Γ(無矛盾)
↓ Lemma 5(リンデンバウム)
Γ*(極大無矛盾)← これで扱いやすい性質がたくさん!
↓ Lemma 6(閉包性)+ Lemma 7(排中律・含意の性質)
↓ Lemma 8(真理補題)← モデルを構成!
完全性定理
Lemma 7(極大無矛盾の性質:¬ と → の振る舞い)
主張: Γ* を極大無矛盾集合とする。
(1) 排中律的性質:
任意の A について A ∈ Γ* または ¬A ∈ Γ*
(両方は入らない。無矛盾だから。)
証明の考え方:
- Γ* ∪ {A} が矛盾 → Lemma 4より Γ* ⊢ ¬A → Lemma 6より ¬A ∈ Γ*
- Γ* ∪ {A} が無矛盾 → Γ* の極大性より A ∈ Γ*
つまり「Aを追加しても矛盾しないか?」で場合分けする。
(2) 含意の性質:
A → B ∈ Γ* ⇔ (A ∈ Γ* ⇒ B ∈ Γ*)
証明の考え方:
- ⇒方向:A → B ∈ Γ* かつ A ∈ Γ* なら、→E で B が出る → Lemma 6より B ∈ Γ*
- ⇐方向:「A ∈ Γ* ⇒ B ∈ Γ*」を仮定。
- A ∈ Γ* の場合:B ∈ Γ* → Γ* ⊢ A → B が言える
- A ∉ Γ* の場合:Lemma 7(1)より ¬A ∈ Γ* → Γ* ⊢ ¬A → Γ* ⊢ A → B が言える
どちらも ⊢ A → B → Lemma 6より A → B ∈ Γ*
💡 Lemma 7で何をやってるか:「極大無矛盾集合 Γ* は、あたかも一つの真理値割り当て(評価)のように振る舞う」ことを保証してる。¬ と → の扱いが真理表と一致するから、次の真理補題(Lemma 8)で「Γ* から評価を作れる」が言える。
ここまでの流れ
Γ(無矛盾)
↓ Lemma 5(リンデンバウム)
Γ*(極大無矛盾)
↓ Lemma 6(閉包性)
↓ Lemma 7(¬ と → の性質)← いまここ!
↓ Lemma 8(真理補題)← モデルを構成!
完全性定理
Lemma 8(真理補題:極大無矛盾集合からモデルを構成)
主張: Γ* を極大無矛盾集合とする。次のように評価 v を定義する:
このとき、任意の論理式 A について:
つまり「Γ に入ってる式=真になる式」。*
証明の流れ(Aの構造に関する帰納法)
原子命題 A の場合: 定義から直ちに従う。
A ≡ B ∧ C の場合:
A ≡ B → C の場合:
- B→C_v = F ⇔ B_v = T かつ C_v = F
- 帰納法の仮定より B ∈ Γ* かつ C ∉ Γ*
- Lemma 7(2) より B→C ∉ Γ*
- 逆向きも Lemma 7(2) で示せる
これで何が言えたか
Γ(無矛盾)を極大無矛盾集合 Γ* に拡張し、Γ* から評価 v を作ると:
Γ の全式を真にする評価 v が存在する
つまり「無矛盾な式集合には必ずモデル(真にする世界)がある」——これが真理補題の核心。
完全性定理の完成
Corollary 1(系):Γ ⊬ A なら、Γ の全式を真にし A を偽にする評価 v が存在する。
→ すなわち Γ ⊭ A。
対偶を取って:Γ ⊨ A ⇒ Γ ⊢ A(完全性定理)
健全性 Γ ⊢ A ⇒ Γ ⊨ A と合わせて:
Γ ⊢ A ⇔ Γ ⊨ A
証明可能性と論理的帰結の一致——ここに完全性定理が完成した!
全 Lemmas の流れ(おさらい)
Γ ⊬ A
↓
Γ ∪ {¬A} は無矛盾(Lemma 4)
↓
極大無矛盾集合 Γ* ⊇ Γ ∪ {¬A}(Lemma 5: リンデンバウム)
↓
Γ* は証明について閉じている(Lemma 6)
Γ* で ¬ と → が真理表のように振る舞う(Lemma 7)
↓
Γ* から評価 v を構成 → 真理補題(Lemma 8)
↓
v は Γ を真にし、A を偽にする → Γ ⊭ A
↓
対偶:Γ ⊨ A ⇒ Γ ⊢ A 🎉