シリーズ「完全性定理を考える」その2　無限に広がる変数記号

　一階述語論理の完全性定理の証明をちゃんと理解するためにいろんな教科書の見比べるシリーズの第2回です。鹿島亮先生の『数理論理学』は特に工夫をいろいろしているようなので、今回もそれです。

作者:鹿島亮
発売日: 2009/10/01
メディア: 単行本

　哲学系ではわりと標準的な教科書っぽい清水義夫先生の『記号論理学』の証明と比較しますよ今回も。

作者:清水義夫
発売日: 1984/11/01
メディア: ハードカバー

　鹿島本の工夫で特に目立っているのが、変数記号の集合を自由出現する変数記号用の ${\mathbb F}$ と束縛出現する変数記号用の ${\mathbb B}$ に分けておく、というものである*1。使用する論理式の集合を、束縛出現する変数記号が ${\mathbb F}$ に入っていて自由出現する変数記号が ${\mathbb B}$ に入っているものに制限しておく。これが証明のなかでどう使われているか見てみる。
　鹿島本では完全性定理で扱う理論は閉論理式の集合なので、理論 $\Gamma$ 中に出現する変数記号全体の集合を ${\mathbb B}$ として、出現しない変数記号全体の集合を ${\mathbb F}$ としておけばよい。鹿島本ではモデル存在定理を証明する際に「 $\Gamma$ の未使用変数が無限ならば」という条件を加えたものを証明する*2。この条件があれば ${\mathbb F}$ は無限集合になることが容易にわかり、そのおかげで第1回で扱った KeySet を構成することが可能になる*3。「存在証拠を持つ」ように ${\mathbb F}$ から変数記号を持ってきてそれを項として論理式を作るのである。
　ややこしいのだが、清水本では理論が閉論理式だけではないようだ。また、そもそも個体変項と個体常項のありかたが鹿島本とは違っている*4。個体変項と個体常項を分けているので、ヘンキン公理の後件を作るための個体常項は無限にある。よってヘンキン公理を無限に作れる。
　こうして見ると鹿島本よりも清水本のほうが簡単で良さそうなのだがそうでもない。鹿島本ではストラクチャーの対象領域の要素とその要素の名前との区別を詳しく議論している。名前はあらかじめ定数記号として用意されていないので、これを厳密に扱おうとして話が複雑になっているようだ。清水本ではこのあたりがよくわからない。しかし、最終的に証明のうちではこの区別は必要ないとわかる。
　謎だったのは、普通は $\exists xFx$ という形の論理式が真なのはある定数 $a$ について $Fa$ が真のとき、みたいにするもので、鹿島本でも（対象領域の要素の名前を定数記号として加えたうえで）そうしているのだが、完全性定理の証明の際の存在証拠を作るところでは変数 $y$ をとってきて $Fy$ みたいにする。変数でいいのかな、とも思ったのだが、けっきょく変数も含めた項（自由変数が ${\mathbb F}$ の要素）から対象領域を作ってモデルを定義するのでこれでよいっぽい。変数の名前が定数記号に加わる。
　最終的に項とその名前の区別が必要なくなるのならそんなに厳密に区別しなくても良さそうなものだが、この厳密さは論理学において重要なのだろうと思う。これがないと数学的にまずいのかどうかはわからない。いろいろわからなくなってきたのでまた次回。
　自然言語ばかりで数学っぽさに欠ける記事になってしまったと反省。あとから読み返してわかるのだろうか。

*1:鹿島本はここでは「自由変数」「束縛変数」と書かない。あくまで記号の話だからか。

*2:ここからその条件のないモデル存在定理も証明できて、完全性定理も証明されたことになる。

*3:KeySet の構成ができる条件として「 ${\mathbb F}$ の要素で $\Gamma$ に現れない変数記号が無限個ある」というのがあるが、この定義だと ${\mathbb F}$ の要素はそもそも $\Gamma$ に現れない。

*4:このへんは鹿島本における変数の名前とか定数の定義にからんでくる話と思われるのでまた今度