論理学をつくるは公理系の完全性証明まで読み切って無事三部(古典論理学パート)を読み切りました。そこまでの感想とかは改めてメインブログの方に書こうと思います。

おさらい

前回は練習問題を解いただけなので内容の繋がり的には前々回からの続き。

yuyubu-sub.hateblo.jp

前々回

yuyubu-sub.hateblo.jp

公理系の完全性を証明したい
強い完全性定理を証明する
ヘンキンの定理を証明する
- 証明するために補助定理44-1(証明ずみ),補助定理44-2(証明中)を導入
  - 44-2を証明するために補助定理44-2-1,44-2-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を証明する
今回証明する定理を再掲

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

44-2 証明

証明の概略
- 1. Γ*が与えられた時、原始式を充足するassignmennt Vの作り方を示す
- 1. Γ*の原始式以外(複合的論理式)も充足されることを示す
Vを定義する

【真理値割り当て V】 Pを任意の原始式とする。V(P)=T ⇔　P∈Γ*

定義したVの元で以下が成り立つ

Aを任意の論理式とする。この時、V(A)=T ⇔ A∈Γ*

前者は原始式のみについて、後者は論理式全体について言及していることに注意。

Vのもとで真になる式が`Γ*`に含まれていることの証明

[Basis]
- Aが原始式であるときV(A)=T ⇔ A∈Γ*(Vの定義)
[induction steps]
- A,BについてV(A)=T ⇔ A∈Γ*,V(B)=T ⇔ B∈Γ*が成り立ってるとする(帰納法の仮定)
- この時以下の1~5が言えればあらゆる論理式AについてV(A)=T ⇔ A∈Γ*が言える
  - 1.V(¬A)=T ⇔ ¬A∈Γ*
  - 2.V(A∧B)=T ⇔ A∧B∈Γ*
  - 3.V(A∨B)=T ⇔ A∨B∈Γ*
  - 4.V(A→B)=T ⇔ A→B∈Γ*
  - 5.V(A↔︎B)=T ⇔ A↔︎B∈Γ*
- (1)の証明
  - V(¬A)=Tである場合,V(¬A)=Fであるので、帰納法の仮定よりA∉Γ*
    - A∉Γ*のとき補助定理44-2-2より、¬A∈Γ*
  - V(¬A)=Fである場合,V(¬A)=Tであるので、帰納法の仮定よりA∈Γ*
    - A∈Γ*のとき補助定理44-2-2より、¬A∉Γ*
- (2)の証明
  - V(A∧B)=TのときV(A)=TかつV(B)=Tである
    - 帰納法の仮定よりA∈Γ*かつB∈Γ*である
      - 補助定理44-2-2よりA∧B∈Γ*
  - V(A∧B)=FのときV(A)=FまたはV(B)=Fである
    - 帰納法の仮定よりA∉Γ*またはB∉Γ*である
      - 補助定理44-2-2よりA∧B∉Γ*
- (3)の証明
  - V(A∨B)=TのときV(A)=TまたはV(B)=Tである
    - 帰納法の仮定よりA∈Γ*またはB∈Γ*である
      - 補助定理44-2-2の3よりA∨B∈Γ*
  - V(A∨B)=FのときV(A)=FかつV(B)=Fである
    - 帰納法の仮定よりA∉Γ*かつB∉Γ*である
      - 補助定理44-2-2よりA∨B∉Γ*
- (4)の証明
  - V(A→B)=TのときV(A)=FまたはV(B)=T
    - 帰納法の仮定よりA∉Γ*またはB∈Γ*である
      - 補助定理44-2-2の4よりA→B∈Γ*
  - V(A→B)=FのときV(A)=TかつV(B)=F
    - 帰納法の仮定よりA∈Γ*かつB∉Γ*である
      - 補助定理44-2-2の4よりA→B∉Γ*
- (5)の証明
  - V(A↔︎B)=Tのとき(A∈Γ* ∧ B∈Γ*) または (A∉Γ* ∧ B∉Γ*)
    - 帰納法の仮定よりA∉Γ* ∧ B∉Γ*またはA∈Γ* ∧ B∈Γ*である
      - 補助定理44-2-2の4よりA↔︎B∈Γ*
  - V(A↔︎B)=Fのとき(A∉Γ* ∧ B∈Γ*) または (A∈Γ* ∧ B∉Γ*)
    - 帰納法の仮定よりA∉Γ* ∧ B∈Γ*またはA∈Γ* ∧ B∈Γ*である
      - 補助定理44-2-2の4よりA↔︎B∉Γ*◽️
証明の疑問点
- 補助定理44-2-2はならかの式PがΓ*の元になる(∈)条件が書かれているだけである　
- 補助定理44-2-2でΓ*の要素となる式Pの否定(¬P)が必ず¬P∈Γ*となることは44-2-2だけで言えないのではないか？
  - 極大無矛盾集合の定義を持ち出す必要があると思う
    - 自明だから特にやらないということか？

完全性定理からすぐに導かれること

【定理45】APLにAPLでprovableでないどんな論理式を公理図式として付け加えても構文論的に矛盾してしまう。

3.11 コンパクト性定理

Γの全ての有限部分集合が充足可能である ⇨ Γは充足可能である

証明
- Γのあらゆる有限部分集合が充足可能
- Γのあらゆる有限部分集合が無矛盾(健全)
- Γが無矛盾(deductionの有限性)
- Γは充足可能(完全性定理より)◽️

完全性定理の疑問点

「シンタックス、セマンティクスの広がりの一致」と「完全性」どちらが先に証明されて、どちらが導かれるのかの関係がわからない
- 本書だと完全性と証明して、そのあと広がりが一致している、と書いているように読める
- 個人的には完全性の定義が「シンタックス、セマンティクスの広がりの一致」を必要としているように読める
「構文論と意味論の広がりが一致する」が感覚的に理解できない
- 構文論に置けるモデルの欠落というのがかなり大きいはず。