今日の論理学:リンデンバウムの補助定理の証明

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

• 公理系APLの完全性を証明したい
  • ヘンキンの定理を証明する必要がある
    • 【補助定理44-1 リンデンバウムの補助定理(Lindenbaum's lemma)】
    • 【補助定理44-2 極大無矛盾集合の充足可能性補助定理】→これは次回やる

今日はリンデンバウムの補助定理の証明をなぞる

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

論理学をつくる

証明概略

• 任意の無矛盾な式集合Γのスーパーセットになる極大無矛盾集合Γ*をつくる方法を示す
• その手順で作ったΓ*が極大無矛盾集合になっていることを示す

ΓをΓ*に拡張する方法

• 任意の論理式の集合は枚挙可能である。
  • 自然数の番号をつけて一列に並べることができる
• 全ての論理式を枚挙した列が与えられているとする
• 無矛盾なΓに対して、矛盾しないならΓ*の要素として付け加えるという操作を続ける。

手順

式集合の系列Γ₀,Γ₁,...をつくる

• (1)Γ₀ = Γ
• (2) A_iを枚挙した論理式のi番目の要素とする
  • Γi∪{A_i}が無矛盾の場合
    • Γ_i+i = Γi∪{A_i}
  • Γi∪{A_i}が無矛盾で無い場合
    • Γ_i+i = Γi
• (3) 上記手順を無限回繰り返した集合Γ* = ∪_i=0^∞Γ_iを極大無矛盾集合とする。

上記の操作で作成した式集合Γ*は以下の要素を満たしている。

• 系列Γ₀,Γ₁...に現れる式を全て含む
• Γ∈Γ*である

Γ*が極大無矛盾集合であることの証明

Γ*が極大無矛盾集合であることを証明するためには以下の2つの証明が必要である

• (1)構文論的に無矛盾であることの証明
• (2)極大であることの証明

(1)構文論的に無矛盾であることの証明

• 前半:数学的帰納法を用いて、Γ₀,Γ₁...に現れる任意のΓ_nが構文論的に無矛盾であることを示す。
• 後半:Γ₀,Γ₁...が構文論的に無矛盾である時,Γ* = ∪_i=0^∞Γ_iも無矛盾であることを示す

前半

• 前半:数学的帰納法を用いて、Γ₀,Γ₁...に現れる任意のΓ_nが構文論的に無矛盾であることを示す。

• [Basis] Γ₀は無矛盾と仮定したΓであるため(Γ₀=Γ)無矛盾である

• [Induction step] Γ_k+1より前にある全ての集合が無矛盾であると仮定する
  • この時、Γ_k+1も無矛盾であることを示す。
    • 定義よりΓ_k+1は以下のどちらかとなる
      • 1.Γk∪{A_k}
      • 2.Γk
    • A_kを加えても矛盾しない場合のみΓ_k+1は前者になるので、1は無矛盾である。
    • 2は帰納法の仮定により無矛盾である■

後半

• 後半:Γ₀,Γ₁...が構文論的に無矛盾である時,Γ* = ∪_i=0^∞Γ_iも無矛盾であることを示す
• 次の補助定理を使う

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

• Γ*が矛盾している時Γ*に矛盾している部分集合Γ'が存在する
• Γ'野中の最も大きい番号の式をA_jとする
  • Γ'に含まれる式はΓ_j+1に含まれている
    • Γ_j+1は矛盾しているΓ'を含むため、これもまた矛盾している
      • これはΓ₀,Γ₁...に現れる任意のΓ_nが構文論的に無矛盾という前半と矛盾する■

note:本書中では「前半と矛盾する」、という書き方ではなく「仮定に反する」と書かれているが、その仮定はどこにもないので、「前半」の間違いだと思う。

これは、系列Γ0,Γ1,...のあらゆる要素が無矛盾であるという仮定に反する。■(p271)

(2)極大であることの証明

背理法を使う。

• 背理法の仮定:Γ*が無矛盾だが極大ではないとする
  • 上記の仮定でΓ*∪{A_j}を無矛盾とするA_j∉Γ*が存在する
    • "矛盾した集合を含む集合は全て矛盾している"
      • 上記の対偶は"無矛盾な集合の部分集合は全て無矛盾である"
      • Γ_j∪{A_j}はΓ*∪{A_j}の部分集合である
        • Γ*∪{A_j}が無矛盾ならばΓ_j∪{A_j}も無矛盾
          • とするとΓ*の構成ルールよりΓ_j+1=Γ_j∪{A_J}
          • A_j∈Γ_j+1よりA_j∈Γ*
            • これは仮定に反するので背理法の仮定は矛盾
            • よってΓ*∪{A_j}が無矛盾かつA_j∉Γ*となるA_jは存在しない
            • つまりΓ*は付け加えても無矛盾性を保つ式は全て含んでいる=Γ*は極大■

次回

次回は【補助定理44-2 極大無矛盾集合の充足可能性補助定理】を証明します。

これにより

• ヘンキンの定理が証明される
• 公理系APLの完全性が証明される

というドミノ倒し的なことが起こるはず。そして公理系を証明すると、この本の古典論理学パートはおしまいです。