今日の論理学:ヘンキンの証明途中

前回の完全性定理の証明の続き。平日なので進捗少なめ

ヘンキンの証明

• まずAPLの完全性を証明する。　
  • その後、　少し手直ししてNDの証明を行う
• 完全性Γ⊨B ⇨ Γ⊢Bの証明を以下の定理で置き換える

[定理43]Γ⊨A ⇔ Γ∪{¬A}は充足可能ではない
[定理40]Γ⊢A ⇔ Γ∪{¬A}は構文論的に矛盾する

• Γ∪{¬A}は充足可能ではない ⇨ Γ∪{¬A}は構文論的に矛盾する
  • そしてこの対偶を証明する

Γ∪{¬A}は構文論的に無矛盾 ⇨ Γ∪{¬A}は充足可能

【定理44:ヘンキンの定理】論理式の集合Γが構文論的に無矛盾 ⇨ Γは充足可能

ヘンキンの定理を証明すれば強い完全性定理が証明されたことになる。

• ヘンキンの定理の証明手順
  • 1.構文論的に無矛盾な式集合Γを充足する割り当てがあることを示せば良い
  • 2.構文論的に無矛盾、だけだとΓに対する情報が乏しく、割り当てが作れない
  • 3.Γを含んだ証明じょう都合の良いΓ*をつくる
  • 4.Γ*を充足できる割り当てを作れることを示す。(というより示せるようにつくる)
  • 5.Γ*はΓを含んでいるから(4)で作ったアサインメントはΓを充足する

極大無矛盾集合(maximally consistent set)

• Γ*は極大無矛盾集合(maximally consistent set)と呼ばれる

【定義】論理式の集合Δが極大無矛盾である ⇔ Δは構文論的に無矛盾であり、Δの要素ではない全ての論理式Aに対しΔ∪{A}は構文的に矛盾している。

ヘンキンの定理を証明するために、極大無矛盾集合を使った以下の2つの補助定理を導入する

【補助定理44-1 リンデンバウムの補助定理(Lindenbaum's lemma)】
Γが構文論的に無矛盾な式の集合である時、Γを部分集合とするような極大無矛盾集合Γ*が少なくとも1つ存在する

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

証明の手順をまとめると以下のようになる。

Γが無矛盾
↓
Γを含むΓ*が存在する
↓
Γ*は充足可能
↓
Γも充足可能

論理学をつくる

つづく...