このyoriyukiさんのエントリーに反応しておきます。
まず「なるほど、僕に落ち度があった」と思う点を先に書きます。それは、「ゲーデルの不完全性定理」とか「ゲーデルが示した」と書いてある部分が、“ゲーデル原論文にある定理そのもの”や、“ゲーデルなる人物が史的事実として発表したこと”などを正確に指してないことです。これは、誤解を招く恐れもあるし、「それは事実と違う」と言われても仕方ないでしょう。僕の表現が不十分であり迂闊だったと言えます。
しかし僕としては、「ゲーデルの不完全性定理」シリーズの動機や目的からして、「たいして問題にはなるまい」と気を配ってもいなかったし、今でも問題になるまいと思っています。という次第で、以下に、実際に僕が使った表現／言葉に対しその意図を多少補足し、行き違いや水掛け論のリスクを減らすことにします。この意図の部分は、既に書いているか示唆している内容も多いのですが、それらをまとめて記述します。書く側としては1つのエントリーを囲む関連情報も目も通して欲しいのですが、それを常に要求するのも無理があるので、引用や繰り返しの記述もします。
「不完全性定理」の意味するところ
yoriyukiさんのご指摘の順番に話をします。
まず、「算術体系の決定不可能性」と「ゲーデルの不完全性定理」がゴッチャになり混同しているのではないか、という点。
僕は、第1回で次のように述べています。（「オリジナルと同じです」あたりが突っこまれそうではあるが。）
そこで、プログラミングの諸概念を使って、ゲーデルの不完全性定理の変種（バリアント）を示してみます。この変種は、道具立てはオリジナルと違いますが、背後にある考え方と基本的メカニズムはオリジナルと同じです。
ですから、僕がこのシリーズで「ゲーデルの不完全性定理」という言い方で、「このシリーズが目標としているところの、ゲーデルの不完全性定理の変種」を意味していることがしばしばあります。狭義のゲーデルの不完全性定理そのものと、その変種あるいはその拡大解釈が峻別されてない、という指摘であれば、そのとおりなのですが、そこまで言葉使いに神経質になる必要性は感じません。
僕は、次のタイプの定理は「不完全性定理」と呼んでいいと思っています。
- ある条件を満たす体系Sにおいて、PもPの否定もS内で証明できないような命題Pが存在する。
「ある条件」と一般化／パラメータ化すると、ゲーデル本人だけでなく、タルスキーとかロッサーとかの結果も含まれることになるでしょう。あまり変な「ある条件」を指定してもしょうもないのですが、具体的に僕が予定していた（いる）“ある条件”とは、次のものです。
- 証明とは別に、なんらかの方法（モデル論でも神様でもいいのですが）により、真な命題の集合と偽な命題の集合が確定している。
- 証明可能な命題は真である。
- 反証（否定の証明）が可能な命題は偽である。
この条件は十分に受け入れられやすい（論理的な体系とはそういうものだ、と合意しやすい）し、話も簡単になります。
「ゲーデルの定理」じゃなくて「ゲーデル型の定理」と呼べばよかった？
上記の条件のもとで、PもPの否定も証明できないようなPが存在することを示す（説明する）のが、僕が設定した目標です。今一度繰り返せば、その目標を「ゲーデルの不完全性定理」と呼ぶのは不正確でしょうが、最初に「変種」と断ってあるし、そもそも次のような動機から言っても、ゲーデル原論文の定理そのものの説明は目的になりません。
発端編（http://www.chimaira.org/docs/GodelsIncomplete.htm）より：
僕は、自然言語による説明にはまったく期待を持っていない。かといって、正統的に記号論理から解説するのも手間がかかり過ぎる。抜け道はあるか？ …… あるかもよ。あるような気がしている。
ともかくも、説明の基本的方針としては、停止しないプログラムって概念を利用する。あと、ゲーデル符号化はコンパイルと解釈して、帰納的に枚挙可能な定理集合は、無限に定理をはき出し続けるプロセスと解釈する。こうして、プログラマにお馴染みの概念だけでゲーデルの不完全性定理を解説できる気がするのだ。
「ゲーデル型の定理」とか「不完全性定理の変種」とかの言葉を毎回使えば、誤解を避けられるのでしょうか。
「不完全性」の意味するところ
僕が使っている「不完全」の意味は次のようなことです。
- 体系S内の命題Pで、PもPの否定も証明できないものがあるとき、Sは不完全
この「不完全」という言葉を使って、「ゲーデル型の定理」の一般的かたちを再度述べれば：
- ある条件を満たす体系Sは、不完全になってしまう。
「述語」の意味するところ
次は、「述語」という用語に計算可能性は含まれない、という指摘。
述語は意味のある性質であればよく、真偽値を計算する関数が存在している必要はありません。
ウーン。ここは、「述語」という用語自体を取り出して辞書的に定義を与えているワケじゃないのだけど。willStopとかcanProveという関数は、それが実在するかどうかに関わらず、JavaScriptで書かれたプログラムだという流れ／前提で話をしていたのですけど。そうは受け取れませんか。
僕のその前提のもとでは、関数は最初からアルゴリズム（の記述であるプログラム）として与えられているのです。「述語」は、関数のなかの特定の種別、具体的には“1引数で真偽値を返すもの”と、ここでローカルに定義してます。
おそらく、「ゲーデルの不完全性定理では、」という表現（下に引用）が、先に述べたごとく「狭義のゲーデルの不完全性定理そのもの」と解釈され、かつ「述語」も一般的・絶対的な定義（計算可能とは限らない）であるべきと解釈されたのだと思うけど、この文脈とこの日本語表現で、そう取られるのかな？
ゲーデルの不完全性定理では、
willStop(progDef, someArg)の代わりにcanProve(predDef, someArg)を考えます。この意味は：
- 1引数で真偽値（trueかfalse）を返す関数を述語（predicate）と呼ぶ。
- predDefは、述語の関数定義本体（を表す文字列）である。
- canProve(predDef, arg)は、predDefのargをsomeArgで置換した定義（あくまで文字列！）が、ある機械的定理証明系で証明可能であればtrue、反証可能（否定が証明可能）であればfalseで返す。
「canProve」の意味するところ
次は：
ゲーデルが作ったcanProveは算術の述語（掛け算、足し算、等号、論理記号から定義できる述語）であって、計算可能な関数ではありません。
1変数（変域は自然数、変数名は便宜上固定する）の述語を表現する論理式がP1, P2, ... と列挙可能だとして、Provable(x)が「xが証明可能」を、Subst(P, m)が「Pに含まれる変数を値mの表現で置き換える」を意味するとして、Provable(Subst(Pn, m)) を2変数の述語（関係）とみれば、「n番目の述語にmを代入した命題は証明できる」と内容的に解釈できます。これに対応するものを、算術ではなくて、JavaScriptプログラムの世界で考えたものを僕はcanProveと呼ぶ目論見だったのです。（canProveの値がfalseになる条件は後述。）
で、上の指摘は「ゲーデルがJavaScript書くかいな!? オイッ。ゲーデルは算術でやったんだよ」って指摘でしょうか。であれば「おっしゃるとおり」ですが、先に述べたごとく、「ゲーデルが／は…」を「ゲーデルが／は…した、それに対応するように檜山がJavaScriptプログラムに直した」と読み替えてもらわないと、「記号論理や算術の代わりにJavaScriptを使う」という方針と食い違ってしまい、僕が意図した説明が全然実行できません。
yoriyukiさんは、僕のエントリーが狭義のゲーデルの定理を忠実に紹介したもの、あるいはそうすべきだ、という前提で書かれている印象を受けるのですが、どうでしょう。
それと、「算術の述語は、計算可能な関数ではない」という意味がよくわかりません。P(x)のxに具体的なnを入れたP(n)の値を求める計算手続きがない、ということ？
「canProveがfalseを返す」の意味するところ
まだあります：
反証可能(檜山氏の定義では否定が証明可能)とcanProveがfalse(つまり、肯定が証明できない)ことが混同されています。
引用されている僕の文章に次が含まれます（少し簡略化した）。
canProveは、命題が、ある機械的定理証明系で証明可能であればtrue、反証可能（否定が証明可能）であればfalseを返す。
この文にあるとおり、「canProveがfalseを返すのは否定が証明できるとき」です。「canProveがfalseを返すのは肯定が証明できないとき」と僕は言ってません。（[追記 time="当日17時くらい"]あ、そうか！ canProveって名前が紛らわしかったのだ。truthByProof、変かな？ checkByProofとか？[/追記]）
同じく引用されている僕の「canProveがtrueもfalseも返さない事態が起こりえる」とは、適当な命題（実際には、述語表現の変数を埋めたもの）を選ぶと、次の2つを同時に満たす状況がありえることです。
- canProveがtrueを返さない、すなわち「ある機械的定理証明系で証明可能である」とは言えない。
- canProveがfalseを返さない、すなわち「ある機械的定理証明系で否定が証明可能である」とは言えない。
まとめると、当該の命題は：
そんな命題があれば、ある機械的定理証明系（形式的論理体系のプログラム版）で、証明可能でもないし反証可能（否定が証明可能）でもない命題の例となり、「体系S内の命題Pで、PもPの否定も証明できないものがあるとき、Sは不完全」という定義と付き合わせて、「この機械的定理証明系は不完全だ」と言ってもいいと判断しますが。
最後の段落の：
ところで、canProveが計算可能な関数ではなく、単に数学的な関数(つまり真偽値を、計算可能でなくて良いから返す関数)だとすればどうでしょうか。
この点ですが、僕もそのような関数を考えています。しかし、それはcanProveではありません。例えば、isValidとでも命名すると、こいつは計算ではなくて何か超越的（神がかり）な方法でtrueかfalseを返します。それで、体系Sの条件として僕が（説明に適切だろうと）選んだのは次のことです。（canProve1は、canProveと同様だが1個の命題を引数にするもの。）
- canProve1(x) = true ならば、isValid(x) = true 。
- canProve1(x) = false ならば、isValid(x) = false 。
もし、isValid(x)がどんなxに対しても（trueまたはfalseと）確定しているなら、次の現象が起きます； canProve1(x) がtureでもfalseでもないxを取ってきて、isValid(x)の値を調べてみる：
- tureのとき： xは真だが、canProve(x) = trueではないので証明できない。
- falseのとき： xは偽だが、canProve(x) = falseではないので反証できない。
この状況が“起こりえる状況だ”と説明できれば、「ゲーデルの不完全性定理を、プログラマの常識や日常感覚を前提に説明した」と言っても差し支えないと僕は思います。
