命題論理の公理系の完全性証明

論理学を作るp265~のノート。箇条書きで要点をまとめながら精読しています。今まで紙にボールペンでやっていましたが、VScodeでMarkdownで書くほうが楽なので試しにブログエントリにしてみます。

何を証明するか

A1,A2,...,An⊨C ⇔ A1,A2...,An⊢C

セマンティクスとシンタックスで導ける論理式が以下の点において同等であることを示す

つまり、セマンティクスで矛盾する論理式はシンタックスでも矛盾する。逆も然り。前者でトートロジーであるものは後者でもトートロジーである。

個人的にこの点は納得していない。なぜならセマンティクスではトートロジーになるが、シンタックスではトートロジーかどうかわからないような式もあるから。シンタックスではモデルの概念が抜け落ちるから

これはセマンティクス的に言えば真になりそうだが、シンタックス的に言えば真でも偽でもない。上記の文を正しいと私たちができるのは魚と動物と交尾に対する経験的なモデルを知っており、それを暗黙のうちに解釈してしまうから。

...という疑問が個人的に拭えていない。

ちなみにセマンティクスでもシンタックスでも真になる式というのは思いつく

上記の命題はシンタックスでもセマンティクスでも真になる。

※なお本当に全ての動物が交尾をするのか知らない。がその話題は割愛。(個人的には多分交尾をしない動物もいると思う)

Γ⊨B ⇔ Γ⊢B

先に紹介したトートロジー一致は、強い完全性定理の特殊系に過ぎない。　
強い完全性定理ではΓが無限集合であっても構わない
- 例:仮定が全てΓの要素であるようなdeductionがある
  - Γを全部使うわけではないので無限でもいける。

概要
- 一般的にこの向きの証明は健全性の証明と言われる。
  - 任意のdeductionが存在する論理式は(シンタクス)はセマンティクスでもトートロジーとなる。
前提
- Γ⊢B
- Γ={B1,,,Bn-１}
- B=Bn
- 各Bi(i=1...n)は以下のどれかである
  - 1.公理
  - 2.Γの要素
  - 3.先行する2つの式からMPによって得られた式
Γを充足する真理値割り当てVがない場合
- 矛盾の定義より、Γが意味論的に矛盾しているのでどんなBでもΓ⊢Bが可能。
- 以後、Γを充足する割り当てVが存在する場合を証明
(1) Biが公理系であるときAPLの公理系は全てトートロジーであるからVのもとで真となる
(2) BiがΓの要素であるとき、家庭より、VはΓを充足する割り当てのためBiはVの素で真となる
(3) Biが先行する2つの式からMPによって得られた式であるとき
- A→CとAがVの素で真であれば、必ずCもVの元で真である。
- MPは真理を保存する。
Bは公理、ΓにMPを有限回当てはめたものであるから、BはVのもとでも真である
- よってΓ⊨B

概要
- 一般的にこの向きの証明は完全性の証明と言われる。
  - セマンティクス上で(トートロジー、矛盾、帰着)が示せる任意の式はその公理の構文で示すことができる。
deductionごとに証明をする必要がある。
- APL,M,ND
Γ⊢BはΓからBへのdeductionがあることを示しているが、どの公理系での　deductionなのかを示せていない
- 各公理系について証明する必要がある
  - Γ⊨B ⇔ Γ⊢_APLB
  - Γ⊨B ⇔ Γ⊢_NDB
  - なるべく汎用的な方法を使いたい。
    - ⇨ヘンキンの証明を使う
      - 汎用性が高く、まだ出てきていない様相などの公理系にも適用できる。

[定理43]Γ⊨A ⇔ Γ∪{¬A}は充足可能ではない

[定理40]Γ⊢A ⇔ Γ∪{¬A}は構文論的に矛盾する

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

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

続く...