シリーズ「完全性定理を考える」その1　存在証拠とヘンキン公理

　一階述語論理の完全性定理は論理学の最重要定理の一つであり、多くの教科書に証明が載っている。で、当たり前だが教科書によって証明のしかたが異なるので、いろいろな教科書の証明を比較することで理解を深めようというのがこのシリーズである。そういう勉強記録の記事ですよ。
　勉強していると愕然としてしまうのだが、述語論理の完全性定理の証明は命題論理のそれよりも格段に難しい。それだけ量化子やら変数の扱いというのはややこしさを孕んでいる。そしてまた変数の扱いをどうするかという点で教科書ごとに個性が出るっぽいのである。
　鹿島亮先生の『数理論理学』(朝倉書店)では他の教科書にはない工夫がいろいろ為されている。その工夫がどうすごいのかを頑張って理解したい。

数理論理学 (現代基礎数学)

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

　今回は鹿島本と清水義夫先生の『記号論理学』(東京大学出版会)を比較する。清水先生は東大で長年教鞭を執っておられたらしく東大出身の論理学者は教わって影響を受けた人が多いようだが、清水先生ご自身の専門分野などはよくわからず*1、本の記述スタイルも独特で、けっこう謎の人である。

記号論理学

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

　述語論理の完全性定理をヘンキンの手法で証明するには、無矛盾な理論のうち先頭に量化記号のついた論理式も真にするようなモデルを作らなければならない。鹿島本では極大かつ無矛盾でありさらに存在証拠というのを持った集合を作る。清水本ではヘンキン公理というのを加えて拡大していった理論を拡大して無矛盾で完全な理論を作り、そこからモデルを定義する。清水本では極大無矛盾集合という言葉は出てこない。やってることは鹿島本とかわらないのだろうけれど、細かいスタイルの違いについてはまた考えることとする*2。
　さて鹿島本。極大無矛盾集合をそのまま使っているわけではなくて、そこに「存在証拠を持つ」という条件を加えたものを KeySet と呼んでそれを使っている。「存在証拠を持つ」の定義は正確に書くといろいろ前提が必要でややこしいが、要するに集合 $\Gamma$ の中に先頭に $\exists$ がついた論理式、例えば $\exists x \phi$ があれば、 $\phi[t/x]$ となるような $t$ がある、そんな集合 $\Gamma$ は存在証拠を持つ、というような感じ（文章ヘタだな）。KeySet というのは極大で無矛盾で存在証拠を持っているような集合のことで、論理式の集合（理論）を KeySet になるように拡大していってモデルを作る。極大無矛盾集合を作る方法は、無矛盾ならば加えて矛盾したら加えない、という（お馴染みの）操作だが、先頭に $\exists$ がついた論理式を加える際は「存在証拠を持つ」ようにもうひとつ論理式を加える。 $\exists x \phi$ を加えたときに $\phi[t/x] \in \Gamma$ を加えても無矛盾性は保たれるので、無矛盾であることと存在証拠を持つことは必ず両立する。この「存在証拠を持つ」ことだが、これが役に立つのはKeySetである $\Gamma$ の性質
　 $(\forall x \phi) \in \Gamma \Longleftrightarrow$ 任意の項 $t$ に対して $\phi [t/x] \in \Gamma$
と
　 $(\exists x \phi) \in \Gamma \Longleftrightarrow$ ある項 $t$ が存在して $\phi [t/x] \in \Gamma$
を証明するときである。命題論理の完全性定理では
　 $(\phi \land \psi) \in \Gamma \Longleftrightarrow (\phi \in \Gamma)$ かつ ( $\psi \in \Gamma$ )
というのを論理結合子ごとに証明していくが、述語論理ではこれの量化子バージョンが必要になるわけだ。
　清水本ではヘンキン公理というのを使っている。というか実は清水本にはヘンキン公理という用語は出てこないのだが、たぶん他の本でヘンキン公理と呼ばれているものだと思う。その公理というのは（鹿島本とスタイルを統一して書くと）
　 $\lnot \forall x \lnot \phi x \to \phi t$ すなわち $\exists x \phi x \to \phi t$
というもの。こう書くと簡単だが、実際は $\phi x$ と個体定項 $t$ という形の論理式をゲーデル数化して枚挙し、その変数 $x$ とかぶらないように個体定項 $t$ を選ぶ、というかなり面倒な作業が必要となる*3。そして理論にヘンキン公理を次々と加えていって拡大し、そこからさらに極大無矛盾になるようにお馴染みの操作をしていく。ヘンキン公理を加えていっても無矛盾性は保たれるので、完全な理論に拡大できる（この事実は「リンデンバウム補題」という名前で出てくる）。ヘンキン公理は、そうして無矛盾で完全になった理論から作られたモデルが量化子の意味をちゃんと定義できることを証明する際に使われる。これは上に書いたような鹿島本のやり方と同じだが、モデルの定義がけっこう違うかもしれないので詳細はまた今度。
　鹿島本と清水本を比較するとどうだろうか。理論を拡大していく操作が清水本ではヘンキン公理を加えることと完全な理論を作ることの二段階必要なのに対して、鹿島本では一発で済んでいる。となると確かに鹿島本のほうがわかりやすい気がする。どうでしょうか。
　というわけで、もっと詳細でボリューミーな記事にしたかったが、まあ勉強記録のためにやっていることなので、ちょっとずつでもどんどん上げていくのがいいかな、という感じなので今回はこんなところで。「また今度」がいろいろ出てきたが、ちゃんと定義や命題を書こうとするとその本がそれまで使ってきた前提も踏まえなければいけなくて難しいということがわかった。それが今回の学びであった。

*1:哲学科出身で、ラッセルの翻訳をやっておられるのはわかっている。

*2:極大ではなく完全が出てくる。ここでいう「完全」はもちろん完全性定理の「完全性」とは別。鹿島本では「完全」「完全性」と呼び分けて区別しているのでそれを踏襲した。

*3:このややこしさを解消するために鹿島本では自由変数として使う変数記号の集合と束縛変数として使う変数記号の集合をあらかじめ分けるという工夫をしている。上の鹿島本の解説ではこのことをごまかして書いてしまっている。この工夫についてはまた今度。