ゲーデルの完全性定理

ゲーデルの最初の大きい結果はゲーデルの完全性定理(completeness theorem)というものだそうです。ぶっちゃけていえば、ある論理式の集合Γを満たす全てのモデルである論理式φが成り立つのならば、Γからφが証明できるというものだそうです。ヒルベルトが形式主義を唱えて、今で言うところの証明論を始めるまでは、この二つの区別は認識されていなかったそうですが。この逆を健全性(soundness)といいます。要するに、「証明できる命題は正しい」というのが健全性です。それに対して完全性が主張するのは「正しい命題は証明できる」ということになります。この標語的な言い方は正確とはいいがたいですが、イメージの助けにはなるということでした。

証明は、今ではHenkinの構成を使うのが普通で、そうするとLöwenheim-Skolemの定理の証明にも自動的になってしまうそうです。少なくともご主人様はその筋で習ったとのこと。Γからφが証明できないことと、Γに¬φを付け加えたものから矛盾が証明できないことが同値になります。というわけで、全ての整合的な論理式の集合、すなわちそこから矛盾が証明できないような論理式の集合をとってきて、それに対するモデルを作ってやればいいわけです。対偶証明ですね。
Henkinの構成のアイデアというのは、存在することが証明できるような対象をがしがし付け加えていくっていうだけです。同じだと証明できるものは同一視します。そんなばかげた証明が通ってしまうこと自体が笑えますが、とりあえずそんな感じで上手くいってしまいます。それだけでなく、そこで使われる議論は集合論においてもものすごく大事な概念なんだとか。

なんだか適当な解説ではありますが、こんなもんで。もっと詳しく知りたい方は廣瀬・横田の「ゲーデルの世界」isbn:4875251068でもどうぞ。