完全性定理って、素人には、そんなにむずかしいわね、確かに。

ぼくの完全性定理の理解がダメだと、(2011-12-14 - /dev/wd0a）でアホ呼ばわりされて、悲しくなったことはゲーデル本食い歩き - hiroyukikojimaの日記の付記に書いたけど、今日のこの人の付記にもまだ「間違っている」と付け足してあるので、仕方ないから、やっぱり定理を正確に引用しようと思う。そのほうが、きちんと理解したい人には有益だろうから。やっぱ、数学にしても、経済にしても、ブログに言葉だけで書こうとすると、専門家にいろいろと細かいことを注意されて、面倒なことになるなあ。う〜ん。
でも、記号の嵐になるし、一般の人にはどうでもいいことだと思うので、一般の読者の(数学記号に慣れてない)かたはスルーしてくだされ。
次の補題は、ゲーデル記念日 - hiroyukikojimaの日記で騒いだ述語論理の完全性定理のひとつながりの証明の一部。

新井敏康『数学基礎論』岩波書店の43ページから引用するけど、ブログに書く都合上、表現や語順などは若干、変更する。

付値νと命題変数p(素論理式のこと)について、p^νを以下のように定義する。
ν(p)=1のとき、p^ν=p。　ν(p)=0のとき、p^ν=¬p。
(¬pはpの否定文)

補題1.5.10　
論理式φは、p_1, p_2, …,p_n以外の命題変数を含まないとして、
ν(φ)＝1ならば、p_1^ν,p_2^ν,…,p_n^ν|-φ
ν(φ)＝0ならば、p_1^ν,p_2^ν,…,p_n^ν|-¬φ

ここで、記号（　Ｔ|- A　）は、Tという命題の集合から命題Aが証明できることを表す。ν(A)は、Ａの付値(真偽)を表す。
この本では、この補題と、「TとAからBが証明でき、Tと¬AからもBが証明できるとき、TだけからBが証明できる」という補題を使って、いわゆる命題論理の完全性定理(φがトートロジーならば、証明体系H_0から証明できる)を導いている。それから、この定理を使って、述語論理の完全性定理を導く手順のことは、ゲーデル記念日 - hiroyukikojimaの日記にあらすじをまとめてある。ぼくの要約が正しいと仮定するなら、(非専門家としての感受性で言えば)痺れるような証明である。

この補題1.5.10からさ、もしも、すべての素論理式p_1, p_2, …,p_nに対して、p_1^ν,p_2^ν,…,p_n^νをそれぞれ公理として導入して、(素論理式って、単なる記号・文字だから、それかその否定を公理にするのは自然なことじゃないかなぁ、とぼくは思ってて、それを書き忘れたのだけどさ、専門家ならそのくらい推論して欲しかったのう)、それを理論Tとすれば、どんな命題φについても、φか¬φかどちらかは、理論Tから(証明体系H_0によって)証明できるんじゃないのかなぁ。なんか言ってること間違ってますか？？　
もしあってるなら、この補題はとてもステキだと思うし、述語論理の完全性定理を証明する手順の鮮やかはすばらしい、と思うんだけど。やっぱり、ぼくはきちんと理解できてないのでしょうかね。