これまでの流れのおさらい

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

  • ヘンキンの定理を証明する必要がある
    • 【補助定理44-1 リンデンバウムの補助定理(Lindenbaum's lemma)】→前回やった
    • 【補助定理44-2 極大無矛盾集合の充足可能性補助定理】→今回と次回やる。

• 証明する定理のおさらい

【補助定理44-2 極大無矛盾集合の充足可能性補助定理】
極大無矛盾集合Γ*が与えられると、Γ*に含まれる全ての式を真にする首尾一貫した真理値割り当てが決まる。つまり、極大無矛盾集合は充足可能である

補助定理44-2 極大無矛盾集合の充足可能性補助定理の証明

• 極大無矛盾集合Γ*に対する真理値割り当てが存在することを示す
• 補助定理44-2-1 Γ⊢AかつΓ⊆Γ*であるとき、A∈Γ*

• 補助定理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∉Γ*)

    補助定理44-2-1の証明

• 証明(背理法):Γ⊢AかつΓ⊆Γ*であるとする

  • 背理法の仮定:A∉Γ*とする
    • Γ*∪{A}は矛盾
    • この時矛盾するあるΓ'⊆Γ*となるΓ'が存在する
      • Γ'⊢¬Aである
      • 前提よりΓ⊢A
      • Γ'∪Γ⊢A,¬AなのでΓ'∪Γは矛盾
      • Γ⊆Γ*かつΓ'⊆Γ*なのでΓ'∪Γ⊆Γ*
        • よってΓ*の部分集合が矛盾しているのでΓ*も矛盾
          • 仮定に反するのでA∉Γ*とした背理法の仮定は誤り■

補助定理44-2-2の証明は明日。(ネスぺ前日なのでやらないかも)

続く。。。