「極大(無矛盾)セオリー」で極大セオリーを紹介したが、極大セオリーTの性質「f∈T か ¬f∈T のどちらか一方が必ず成り立つ」は、完全性と呼ぶことがある。ところが、“完全”という言葉は似て非なる意味で使われていて非常によろしくない(邪悪なオーバーロード!)。
まず、意味論的(モデル論的)完全性と構文論的(証明論的)完全性がある。意味論的完全性には弱い完全性と強い完全性がある。結局、次の3つの意味を文脈で使い分ける:
- 弱い意味論的完全性
- 強い意味論的完全性
- 構文論的完全性
論理式の全体をLとして(それに証明系が付いているとして)、証明可能な論理式の全体をP(provableから)、真(モデル論的に妥当)な論理式の全体をV(validから)とする。“弱い意味論的完全性”は、V⊆P のこと、つまり、「真なる命題は証明できる」と言っている。その逆 P⊆V は健全性で、「証明できる命題は真」のこと。P=V のとき“強い意味論的完全性”が成立している。
通常は、健全な系しか考えない。もし健全でないと、真でないけど証明できる論理式があるわけで、そんな系は(ウソを導くので)使いものにならない。健全性 P⊆V が前もって仮定されていれば、“弱い完全性”V⊆Pは、“強い完全性”P = V を導くので、まー、強い/弱いを区別しなくてもいいか、という気もする。
が、健全(sound)かつ完全(complete)なら完璧(perfect)とでも呼んで欲しかったなぁ -- 「真でない命題さえも証明できる」という、見当はずれに強すぎる系も考察の対象にすることもあるだろうから。“強すぎる系”は“弱すぎる系”よりタチが悪い。矛盾する系は強すぎてまったく使いものにならない。
一方、構文論的完全性には真偽概念は(直接には)関係ない。「f∈T か ¬f∈T のどちらか一方が必ず成り立つ」ようなセオリーT(と背後にある証明系)を完全と呼んでいるだけ。構文論的完全性を否定すると、「f∈T でも ¬f∈T でもないようなfが存在する」となる -- これが(構文的な)不完全性の定義。今さらどうにもならないが、こちらは決定可能性/決定不可能性とでも呼んで欲しかった。ゲーデルの論文でも、"Undecidable Propositions"(英訳) という言い方を使っているし。
用語を区別すれば事情もハッキリする。「決定不可能(構文論的に不完全)なセオリーがある」という言明には、直接には真偽概念が出てこない。決定不可能な命題を実際に作ってみせれば済むことだ。一方、「真だが証明できない命題がある」は、「真だが」と言っているので、(対象の系内の)証明とは別な手段で「真であること」を示さなくてはならない。
実際には、決定不可能性を示すにもどっかで超越的な議論をしなくてはならない(構成的構文論では済まない)から、実質的に命題の解釈や意味論をコソッと使っているとも言えるが、真偽概念を表に出しているかどうかは、区別したほうがいいと思う。
「完全」「不完全」という言葉を無闇とオーバーロードしていることが、このへんを不明確にしていると思うのだが、それは僕が無闇と用語に神経質になっているだけだろうか。