Yoriyukiさんへの返答：内容的なコメント編

くどいですけど、最初に「プログラマのためのゲーデルの不完全性定理」の目的を再確認すると、プログラマ／技術者にわかるように、ゲーデル型不完全性定理の一変種を説明すること。

だから、想定読者はプログラマ／技術者であり、僕なりに想定読者向けに“最適化した”表現を（方便だとのそしりを覚悟で）使ってます。記号論理の使用は最小化します。もちろん、記号論理の基礎知識を伝える目的もあるのだけど、それを予備知識とはしない。

あと、注意： 僕は「超越的」という言葉を、「構成可能性／計算可能性を、まったく意に介さない」という意味で使います。

さて、プログラマにとって関数とは、プログラムで実装された計算可能関数のイメージが強い。超越的な関数を持ち出すときは、なにか明示的に注意しないと、たぶん、暗黙に無意識に計算可能と仮定してしまう。

ちなみに、僕は論理の専門家でもなんでもないし、自然な状態（特に集中や緊張してない状態）ではプログラマ／技術者の感覚なので、意識／意図して頭をスイッチしないと、超越的な議論はやりにくいです。

canProveは全域関数になるのか、と思ってしまいました。これが混乱の１点目。

全域か部分かなんてプログラマは意識しません(笑)。willStopに関しては、「どんなプログラム（ソースコード）に対しても停止性を判定するんだ」という強い仕様を事前に注意しているから、「それは仕様が強すぎて（高望みすぎて）できない」という話し方（ストーリー展開）ができます。

強いて言えば、プログラマにとっての関数は常に部分関数です。なぜなら、入力によって関数（プログラム）の挙動は変わるし、ときに無限走行・暴走します。このことは、日常体験／肌感覚でみんな認識しているはずです。この肌感覚が僕が依拠しようとしている説明の基盤（のひとつ）です。

willStopもcanProveもなんら違いはなく、全域関数としては定義できない(部分関数としては定義できる)ということだと思うのですが？

そうです。どちらも事情は同じなのです。willStopに関して、強い仕様は無理だが、弱い仕様ならそれを実装できます。同様に、canProveも強い仕様（全域）は無理でも弱い仕様で実現できます。問題は、この「弱さ」が無意味なほどに弱いのか？です。僕の「速攻速習編」の最後の注意は、「確かに弱いが、人間やコンピュータがアルゴリズム的に遂行する証明行為と同程度の弱さ（あるいは強さ）だ」と示唆したつもりです。

アルゴリズムと言うと(特に断らない限り)全域関数を意味しませんか。

（少なくともプログラマ的には）そんなことないですよ。アルゴリズムは、プログラムで実装する“モトネタの記述”みたいなもんですから、常に未定義／挙動不可解となる入力が存在するリスクを抱えます。それ（アルゴリズムの実装）が全域になることを保証したいときはよくありますが、もちろんのこと、難しいですよね:-)。

ゲーデルはcanProveのような関数を定義したわけではありません。

ごめんなさい。

一つの考え方としては、p=0から順番にisProof(p,predDef,arg)が成り立つかどうか調べてみる、という方法ですが、この場合trueを返すとき以外は停止しません。

僕が採用したのはこの考え方です。証明可能な命題（の符号達）は、帰納的に枚挙可能です。以下「発端編」を引用：

ともかくも、説明の基本的方針としては、停止しないプログラムって概念を利用する。あと、ゲーデル符号化はコンパイルと解釈して、帰納的に枚挙可能な定理集合は、無限に定理をはき出し続けるプロセスと解釈する。こうして、プログラマにお馴染みの概念だけでゲーデルの不完全性定理を解説できる気がするのだ。

上記のプロセスをproverと呼ぶとして： 関数呼び出しcanProve1(x)は、proverの出力（ある体系の定理）を監視して、xを検出すればtrueを返して停止、¬xを検出すればfalseを返して停止するのです。（毎回proverを起動するのは無駄なので、proverを“バックエンド”として走らせて、出力はデータベースに貯めます； どう？ プログラム的でしょ。）

算術の論理式で書けても、その真理値を求める関数が(部分関数であっても)いつもあるとは限りません。

あー、そういうこと。

「ゲーデルが作ったcanProveは算術の述語であって、計算可能な関数ではありません。」と書いてあったので、算術の述語を“真偽値を値とする関数”とみて「計算可能な関数ではありません」と言っているのかと思った。（だとするとワケワカメ。）

計算可能でないのは、「算術の論理式で書いた算術的命題の、真偽性の判定の関数」ですね。それはまー、認識しているつもりです。ディオファントス方程式系の可解性（解の存在）判定とか、解を求める具体的なアルゴリズムが必ずしも存在しない、といったたぐいの話題と解釈していいですよね。これも、ゲーデル的現象かな、と思います。

僕の予定では、Provable(Subst(Pn, m))のようなものを直接表に出す気はなくて、{x | Provable(x)} で定義される集合の枚挙可能性から、それをプロセス（走行するプログラム）proverを通して利用しようとしているのです。Subst(Pn, m)に相当する操作は、proverのフロントエンドであるcanProve(n, m)にやらせます。それと、自然数n, mではなくて、別な符号化データを使います。

ちなみに、不完全性定理を示す一番簡単な方法は、isValid(s)「sが真である」という計算可能な関数が定義できないことを、willStopが定義できないことと同じように導いて、もし正しくて完全な形式体系があれば、isValidが定義できてしまうことを示すことだと思います。

なるほど。確かにwillStopと並行に話を進めたいのですが、背理法の使いどころは難しいのですよ。どっかで背理法は使いますが、「騙された」感じがしないように使うのは難しいです。

理屈が間違っているのは困りますが、心理的に納得が容易な説明を探しています。体系Sの条件に健全性を入れているのは、構文と意味論をわけるってのが実は分かりにくくて、意味論付きの構文体系のほうが自然だと思うからです。真理値割り当て（isValidです）の定義と健全性の仮定に、無矛盾性が含まれてしまっているのですが、「体系が無矛盾」という概念をあえて取り出して説明するより、「体系が健全」だけで進めたほうがスムーズにいくと思っています。

遭遇のキッカケがなんであれ、袖振れ合うも多生の縁とも申しますから、ゲーデル型不完全性定理の一変種の説明戦略にお知恵を貸していただけると幸いです。もちろん、無理強いしません（できるわけもない）けど。

（ランチ・ドリンク付き税込み580円の店にて）