これまでのおさらい

• 公理系APLの完全性を証明したい

  • ヘンキンの定理を証明する必要がある
    • 証明で使いたい補助定理をあらかじめ証明しておく
    • 【補助定理44-1 リンデンバウムの補助定理(Lindenbaum's lemma)】→done
    • 【補助定理44-2 極大無矛盾集合の充足可能性補助定理】→前回途中までやったのでこの続き。
      • 補助定理44-2-1 Γ⊢AかつΓ⊆Γであるとき、A∈Γ → 前回やった
      • 補助定理44-2-2 Γ*を極大無矛盾集合とし、AとBを任意の論理式とすると以下が成り立つ→今回やる

• 前回

yuyubu-sub.hateblo.jp

補助定理44-2-2 極大無矛盾集合に成り立つ5つの同値関係の証明

• 補助定理44-2-2 Γ*を極大無矛盾集合とし、AとBを任意の論理式とすると以下が成り立つ　
  • 1.A∈Γ* ⇔ ¬A∉Γ*
  • 2.A∧B∈Γ* ⇔ A∈Γ* かつ B∈Γ*
  • 3.A∨B∈Γ* ⇔ A∈Γ* または B∈Γ*
  • 4.A→B∈Γ* ⇔ A∉Γ* または B∈Γ*
  • 5.A↔︎B∈Γ* ⇔ (A∈Γ* かつ B∈Γ*) または (A∉Γ* かつ B∉Γ*)

1.A∈Γ* ⇔ ¬A∉Γ*

• case1:A∈Γ* ⇨ ¬A∉Γ*
  • A∈Γ*を仮定すると¬A∉Γ*である。
    • A∈Γ*かつ¬A∈Γ*だとΓ*が極大無矛盾集合なのに矛盾してしまうため。

• case2:A∈Γ* ⇦ ¬A∉Γ*

  • ¬A∉Γ*を仮定するとΓ*∪{¬A}は矛盾する。
    • 補助定理44-1-1よりΓ*の何らかの有限部分集合Γ'が存在する
      • Γ'∪{¬A}が矛盾する
    • 定理40よりΓ'⊢Aとなる
      • さらに定理44-2-1よりA∈Γ*である

• 参考:定理40,補助定理44-1-1,44-2-1

【定理40】Γ∪{¬A}が構文論的に矛盾しているΓ⊢_APLA

【補助定理44-1-1】論理式の集合Γが構文論的に矛盾している時、Γの何らかの有限部分集合が構文論的に矛盾している

【補助定理44-2-1】Γ⊢AかつΓ⊆Γ*であるとき、A∈Γ*

• 疑問:定理40はAPLに限定した話だと思うが、ヘンキンの定理の証明の汎用性に影響はないのか。
  • NDやPで簡単に言い換えられるのか。
  • 定理40と同等のものを他の公理系でも用意するのはそれほど難しそうではないが。

2.A∧B∈Γ* ⇔ A∈Γ* かつ B∈Γ*

• case1:A∧B∈Γ* ⇨ A∈Γ* かつ B∈Γ*
  • A∧B∈Γ*と仮定する
  • A∧B⊢A,そしてA∧B⊢B
    • 補助定理44-2-1よりA∈Γ*かつB∈Γ*である
• case2:A∧B∈Γ* ⇦ A∈Γ* かつ B∈Γ*
  • A∈Γ* かつ B∈Γ*と仮定する
    • A,B⊢A∧B
      • 補助定理44-2-1よりA∧B∈Γ*

4.A→B∈Γ* ⇔ A∉Γ* または B∈Γ*(3,5もほぼ一緒)

• case1:A→B∈Γ* ⇨ A∉Γ* または B∈Γ*
  • A→B∈Γ*を仮定する
    • A∉Γ*を仮定するとA∉Γ* または B∈Γ*はトリビアルに成り立つ
    • A∈Γ*を仮定すると{A,A→B}⊂Γ*である
      • A,A→B⊢Bが成り立つので補助定理44-2-1よりB∈Γ*である
        • よってcase1A→B∈Γ* ⇨ A∉Γ* または B∈Γ*は成り立つ
• case2:A∉Γ* または B∈Γ* ⇨ A→B∈Γ*
  • A∉Γ*をの場合は(1)より¬A∈Γ*
    • つまり{¬A}⊂Γ*である
    • ¬A⊢A→B*1である
    • 上記2点より補助定理44-2-1によりA→B⊂Γ*である
  • B∈Γ*の場合は{B}⊂Γ*である
    • B⊢A→Bである*2から、補助定理44-2-1よりA→B⊂Γ*である
• (3),(5)も同様に証明可能なので省略■

補助定理44-2-2の証明の注意点

• A∧B⊢A
• A∧B⊢B
• A,B⊢A∧B
• A,A→B⊢B
• ¬A⊢A→B
• B⊢A→B

はその公理系で成り立つことを示しておく必要がある。(いくつかのものがAPLで成り立つことを証明する練習問題を次回やる)

つづく。。。