曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

シリーズ「完全性定理を考える」その4 「等号付き一階述語論理の強完全性定理」というやつ

 このシリーズのなかでたびたび混乱した感じになってしまっていたことがあった。鹿島亮『数理論理学』で証明されている完全性定理は「等号付き一階述語論理の強完全性定理」というやつである。このことをハッキリ意識しておかなくてはならなかった。
 鹿島本では等号を明示的に体系に組み込んでいる。この点はこれまで比較してきた清水義夫『記号論理学』や戸田山和久『論理学をつくる』と大きく違う。鹿島本には不完全性定理の概略も載っているので、はじめからバリバリ算術を扱うつもりで定義しているのである。等号付きの体系にしていることが項の定義*1にも影響していそうなのだけど、それはまあよくわからない。ただし証明中でストラクチャーを定義する際に等号を使って同値類を作っている。これは重要。
 強完全性定理について。清水本では弱完全性定理と強完全性定理を分けて証明している*2。これらもけっこう異なる議論が展開されている。弱完全性定理は強完全性定理が証明できればそこからただちに従う*3ので、強完全性定理さえ証明できればまあよい。弱完全性定理だけを証明するのは強完全性定理よりやや簡単で、しかしなにがどう簡単なのかといわれるとそれもよくわからず、これも今後の課題としたいなあ。

*1:拡大項というのを導入していること。

*2:清水本ではそれぞれ「第1完全性定理」「第2完全性定理」と呼んでいる。

*3:この「ただちに従う」って数学の独特な言い回しだなあ。使い方あってるのだろうか。