用語法、述語、数学の命題など
コメント欄のご指摘／ご質問に答えるつもりですが、その前に； どうも釈然としないことがあるんですよ。用語法が食い違っていた、ってのは事実でしょうが、それにしても「用語法って、そんなに問題になるのか？」てのが僕の疑問です。これは、とても気になることです。
僕の用語法が厳密でなかったのは、そのとおりです。が、しかし、理解できない／誤解を招くほどにひどかったでしょうか。言葉（の解釈）にはある程度の幅があり、その弾力性の範囲内でテキトーに使っても、だいたいは通じるものだ、といった楽観主義が僕にはあったのだけど、そうでないとすると考え方を改めねばなりません。
いまだに「用語法だけ」が問題だったとは考えにくいので、「yoriyukiさんは、僕が、ゲーデルの原論文／原証明をたどる説明をすると予測していたのでしょう」という憶測も生まれるのです。
もう一点思い当たるフシは（これも、もちろん憶測です。間違っていたらゴメンナサイ）、「canProve」という名前です。これはもともと、証明エンジンの結果（証明できた／反証できた）を返すだけの関数ですが、「canProve → can prove → provable → |- 」という連想が働いて、超越的でメタな述語と解釈されたような気もしました。そうすれば、
ゲーデルが示したのは、あるφがあって、canProve(φ)もcanProve(¬φ)も共にfalseになること、であってcanProve(φ)がtureでもfalseでもない、と言っているのではありません。
この部分を次のように解釈できると思われます。
ゲーデルが示したのは、あるφがあって、|- φ も |- ¬φ も共に成立しないこと、であって、 |- φ の真偽が決定できない、と言っているのではありません。
僕の憶測（あくまで憶測）をまとめれば、用語法も確かに誤解の要因ではあろうが、次の2点（のどちらか、あるいは両方）も絡んでいるように思えたのです。
- 僕が予定していた方法とは別な証明法を予測していた。
- 「canProve」を、超越的に見ての証明可能を意味する「|-」（または、それを自然数などの符号領域上に移したもの）と受け取った。
もしこういう理由（他の理由でもいいですが）がなくて、単に「用語の使い方が不正確だ」というだけで誤解されたとすれば、ちょっとガックリきてしまいますね。そこまで注意深く言葉を使わなければコミュニケーションが成立しないとなれば、かなり疲れるハナシです。
僕は、言葉の弾力性を利用して、（その許容範囲内で）できるだけ面白おかしく語ろうと意図しているし、それでも正確性がひどく犠牲になることはないはずだ、と楽観していたので。
述語とは何か
まず、「述語」ですが、檜山さんは ...（略）...いずれでしょうか。
場合によりけりで、いずれとも決めてかかってはいません。僕は伝わる範囲内で、場合場合で言葉の使い方はテキトーに変えています。むしろ、変えたほうがコミュニケーションが成立しやすいと思っています。日常会話でも、相手が三歳児と中学生と大人では語彙や表現を変える（つうか、自然に変わる）でしょう。
もっと具体的に答えれば：
- 算術で与えられたプリミティブな述語(普通は等号とか不等号)
- 変数を含む論理式一般が述語と呼ぶことができる(例えばProvable(n)とか)
以上の2つも含めて、「述語」と呼ぶ可能性がある概念を列挙します。
- Xが任意の集合として、f:Xn→{true, false} のような関数（写像）
- 事実上は同じことだが、Xが任意の集合として、Xnの部分集合
気分としては、下の方は「関係」と呼びたいし、Xn→{true, false}の n = 1 のときを特に「述語」と呼びたいのですが、気分に過ぎません。
- 形式的体系の述語記号（あくまで記号）
- 述語記号の意味となる関数または部分集合
この2つを区別せずに、「述語」または「関係」と呼んでしまうことが僕は多いです。
- 自由変数が1つ以下である論理式（1変数で考えるとき）
- そのような論理式から定義される関数または部分集合
論理式をAとして、それに含まれる唯一の自由変数がx（または自由変数を含まない）として、便宜上ラムダ記法を使うと、それから定義される関数は【λx.A】と書いていいでしょう。（【】は意味割り当てです。tを変数を含まないtermだとして、【λx.A】(【t】) = 【A[t/x]】となります。）Aと【λx.A】もあまり区別しないことも、やっぱり多いです。Aにイッパイ自由変数が入っているときや多変数関数を作りたいときは、A←→【λ(x1, ..., xn).A】の対応で考えます。
後者であれば、これを真理関数と見たとき、計算可能でないものは500万個はあります。「1変数（変域は自然数、変数名は便宜上固定する）の述語を表現する論理式がP1, P2, ... と列挙可能だとして、Provable(x)が「xが証明可能」を、Subst(P, m)が「Pに含まれる変数を値mの表現で置き換える」を意味するとして、Provable(Subst(Pn, m)) を2変数の述語（関係）とみれば…」とおっしゃっているので、後者ではないかと思うのですが... だとすれば明確な誤りです。』
「後者」とは「変数を含む論理式一般」ですよね。「これを真理関数と見たとき、計算可能でないものは500万個はあります。」 -- 500万個という数値がなんのことかよくわからないのですが、真理関数とみて計算可能でないものがあるのは了解します。
「後者ではないかと思うのですが... だとすれば明確な誤りです。」 -- くどいですが、後者とは「変数を含む論理式一般を述語と呼ぶ」ことですよね。それが「明確な誤り」ですか？ 論理式はあくまで構文的な対象であり、（真偽を値とする）関数ではないというハナシですか？それなら言いたいことはわかります。それとも、計算可能でない真理関数となるから述語とは呼べないということ？それだとわからない。
JavaScriptと数学の命題
2点目：JavaScriptの真理値を返す関数を述語とみなそう、という発想ですが、この場合止まらない関数も含まれているので、不完全になるのは当たり前な気がします。真偽が定まっていると考えられる数学の命題だからこそ、体系が不完全でしかありえないことに驚きがあるわけで。
これはそのとおりだと思います。数学の命題が、JavaScriptの“命題コード”で表現できて、そのような“埋め込まれた数学命題”の範囲でもやっぱり不完全となることを示す必要があります。
当初、そのことも説明する予定でしたが、今はあきらめ気分です。説明の労力がかかること、それと、「term, formulaの代わりにJavaScriptを使う」という方針では、そこまで行くのに無理があるような気がしているからです。
