このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

不完全性定理シリーズの背景とシナリオ

論理 雑記

yoriyukiさんのご指摘と質問に個別に答える前に、局所的な説明でまた誤解されるのもナンですから、全体的な話をしておきます。ルデーゲ氏とダボーラ氏のオハナシに少し補足します。

これはまた、本編の下書きでもあります。

●形式的体系からJavaScriptへ

まず、僕自身として「方便だ」との非難を一番覚悟していた部分は、JavaScriptの使用です。termやformulaを出さず、代わりにJavaScriptのソースコード断片を使います。当然に、厳密度は下がりますが、「日常感覚で理解しやすくなるだろう」との目論見。以下でも、この方便による記法を主に使います。

foo, bar, bazなどは、JavaScriptコード断片を表すメタ変数。fooDefなどは、コード断片の文字列化であり、fooDefはJavaScriptが扱える対象データ（String型データ）となります。

コード断片fooに自由変数（に相当するJavaScript変数）がなく、boolean値に評価される（と構文的にみなされる）式であるとき、それを命題コードと呼びます。

コード断片barの自由変数が1つ以下であり、boolean値に評価される式を述語コードと呼びます。便宜上、述語コードの自由変数名は'arg'に固定し、String型変数だけを考えます。そうでない変数のときは、一種のアルファ変換でリネームし、パーズや型変換を使えばいいでしょう。

barが述語コードであるとき、barDefはその文字列化データでした。文字列 "return " + barDef + ";" を定義本体として作った関数をbarPFuncと書くことにして、これを、述語コードbarから作った述語関数と呼びます（「関数としての述語」、とか「述語的関数」のほうがいいと思うが、述語関数が一番簡単だから）。

まとめ：

  • bar -- 述語コード （自由変数の個数(bar) ≦ 1 である論理式、ただし構文は複雑）
  • barDef -- 対応する文字列 （Stringを符号領域としてのcode(bar)）
  • barPFunc -- プログラムとして実装された述語関数 （【λarg.bar】:String→{true, false}、部分関数かも知れない）

また、述語関数にbazという名前がついているときは、対応する述語コードのほうをbazCodeという名で呼びます。

●tryProof関数と証明エンジン

ルデーゲ氏の証明エンジン（機械的定理証明系）により、命題コードfooが証明されるとき、|- foo という書き方（メタな言明）を使います。tryProofの定義（ルデーゲ氏の説明）から：

  • tryProof(barDef, realArg) == true ⇔ |- bar[realArg]
  • tryProof(barDef, realArg) == false ⇔ |- !bar[realArg]

ここで、bar[realArg]は、述語コードに現れる変数argを文字列データrealArgで置き換えたもの。!barは、barの否定を表す述語コード。

ルデーゲ氏とダボーラの主張の違いは次の点：

  • ルデーゲ氏：tryProofがtrueもfalseも返さないこともある。
  • ダボーラ氏：tryProofは常に停止し、必ずtrueかfalseのどちらかを返す。

●健全性

もう一点。通常の不完全性定理と、前提や手法が違うのは、体系の健全性を最初から仮定に入れていることです。つまり、命題コードfooに対して、

  • |- foo ならば、|= foo
= foo は超越的真偽性判定を表すメタな言明。 = の定義をちゃんと与えるのは面倒ですが、fooがbar[realArg]の形をしているときは、次のよう：
  • |- bar[realArg] ⇒ barPFunc(realArg) == true

つまり、「述語コードbarの自由変数を埋めた形を証明できるなら、barに対応する述語関数barPFuncに当該引数を渡した値が確実にtrueとなる」。引数の個数を一般化して、次も許す。

  • |- bar[realArg1, ..., realArgN] ⇒ barPFunc(realArg1, ..., realArgN) == true

以上のことは、証明エンジンの条件として要求します。

●背理法によりダボーラ氏を論破する

※この節は、なぜか「だ・である」調

tryProofは、そのバックエンドである証明エンジンまで含めれば大規模なコードだろうが、原理的には単一のJavaScriptコードにまとめることができ、全体としてboolean値の式とみなせる。つまり、tryProofは2変数の述語関数である。tryProof(arg, arg)は1変数の述語関数とみなせ、対応する述語コードも存在するはず。

次のコードを考える。



var strangeDef = "!tryProof(arg, arg)";

var trueOrFalse = strangePFun(strangeDef, strangeDef);

strangeDefは、必要があれば、（おそらくは）長い長い述語コードとみなしてもよい。いずれにしろ意味的には、式 !tryProof(arg, arg) を計算するコードの文字列化である。

もし、ダボーラ氏の主張のごとく、tryProofが全域なら、!tryProof(arg, arg) （から定義される関数）も全域となる。つまり、strangePFunは全域関数となり、その値はtrueかfalseの2つの可能性しかない。（健全性とあわせれば、証明で真偽が完全に決定できる。）

strangePFun(strangeDef, strangeDef)がtrueの場合：

このとき、tryProof(strangeDef, strangeDef)の値はfalse、よって、tryProofの定義（証明エンジンとの関係）から、|- !strange[strangeDef] 。ここで、述語コード!strangeは、意味的に!!tryProof(arg, arg)だとstrangeDefを見ればわかる。さらにこれは、tryProof(arg, arg)と意味的に同じ（二重否定を除去）。よって、|- !strange[strangeDef] とは、|- tryProofCode[strangeDef, strangeDef] のこと。

健全性から、|- tryProofCode[strangeDef, strangeDef] ⇒ tryProof(strangeDef, strangeDef) == trueとなる。だがこれは、「tryProof(strangeDef, strangeDef)の値はfalse」と矛盾する。

よって、strangePFun(strangeDef, strangeDef)がtrueの場合はあり得ない。

strangePFun(strangeDef, strangeDef)がfalseの場合：

同様。

●最初の記述との比較

混乱を避けるため、今回は、次のように表現を変えました。

  • 述語 → 述語関数、述語コード
  • canProve → tryProof
  • 機械的証明系 → 証明エンジン
  • cannotProveDef → strangeDef
  • if文 → 否定記号!
  • provableOrNot → trueOrNot

オリジナル（僕の最初の記述）を引用します。

ゲーデルの不完全性定理では、willStop(progDef, someArg)の代わりにcanProve(predDef, someArg)を考えます。この意味は：

  • 1引数で真偽値（trueかfalse）を返す関数を述語（predicate）と呼ぶ。
  • predDefは、述語の関数定義本体（を表す文字列）である。
  • canProve(predDef, someArg)は、predDefのargをsomeArgで置換した定義（あくまで文字列！）が、ある機械的定理証明系で証明可能であればtrue、反証可能（否定が証明可能）であればfalseを返す。

この状況で、次のコードを考えます。



 var cannotProveDef = 

  "if (canProve(arg, arg)) {return false;} else {return true;}";

 var provableOrNot = canProve(cannotProveDef, cannotProveDef);

 alert(provableOrNot);
停止問題と同じ議論でパラドックス（正確には矛盾）が生じます。

さらに冒頭の「ゲーデルの不完全性定理では、」を、「ゲーデルの不完全性定理の一変種に対して檜山が予定している証明では、」に変更してください。結局は今回のこの説明とまったく同じになります（短すぎたが）。

今回、「停止問題と同じ議論でパラドックス（正確には矛盾）が生じます。」を実行してみたわけです。これはまた、yoriyukiさんの次の指摘と近い方式だと思います。

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

●なぜ、ルデーゲ（旧ゲーデル）氏が登場したか

僕は次のようにも書いてます。

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

敵役のダボーラ氏を登場させて、背理法を使いやすくなったと思います。しかし、背理法で「…が不可能」とわかっても、それは、「我々（人間やコンピュータ）は何ができないのか？」には答えますが、「我々は何ができるのか？」には答えてない気がするのです。

人間／コンピュータの証明行為が全能でないこと、超越的真偽判定と同じことはできないことはわかりました。では、人間／コンピュータはどこまでならできるのか。それを、やれるところまでやり切った人物がストーリー上必要だったのです。その人物を何も考えずに「ゲーデル」と書いてしまったのが僕の大失敗ですが。

しかし、停止問題とは異なり、「だからcanProveなんてあり得ない」とは言えません。なぜなら、ゲーデルは非常によくできたcanProveをホントに作ってしまったからです。

ただし！ ゲーデルは嘘つきでもホラ吹きでもないので、「canProveは、どんな述語定義に対しても必ずtrueかfalseを返す」とは言ってません。確実な前提と確実な推論から導かれる結果は、ゲーデルが定義したcanProve関数（に相当するアルゴリズム）は完全ではないということです。「完全ではない」の意味は、canProve(predDef, someArg)がtrueもfalseも返さない事態が起こりえるということです。これは、証明可能でも反証可能でもない命題の存在を示します。

この部分が、後で書き直したルデーゲ氏の正直な説明に相当します。「完全でない」ことは、上の背理法から既に言えてます。「嘘つきでもホラ吹きでもない」は、ダボーラ氏との比較により鮮明になっていると思います。

最後の文：

「アルゴリズム的に行為する限り、人間もcanProve以上のことは出来ない」と言うのがより適切でしょう。

このcanProveは、tryProofと証明エンジン一式に相当します。止まる保証がないので、「セミアルゴリズム的」と言うべきでしょうが :-)。

●ゲーデルの証明ではないこと

これは憶測ですが、yoriyukiさんは僕が、ゲーデルの原論文／原証明をたどる説明をすると予測していたように思えます。が、それは最初からまったく考えてません。ω無矛盾のような概念をうまく消化して説明できる自信がありません。それより、超越的な真偽概念と健全性を使ってしまうほうを選んだわけです。これには2つのメリットがあります。

  1. 全体に、説明が簡略化される。
  2. 「完全ではない」と背理法で示すとき、停止性と同じ論法が使える。

と、そういう事情です。よって、一般論として、次の諸点をどなたかに批判されても「いまさらどうにもならない」のです。

  1. 形式化をさぼっている。JavaScriptでイイカゲンに代用している。
  2. 健全性を最初から仮定している。仮定として強すぎるし、妥当性／健全性の定義もあいまいである。
  3. いずれにしろ、ゲーデル本人の原論文とは似ても似つかない。

最初から、それらを捨てて、分かりやすさを取ったのですから。僕のシナリオ自体は、最初から今まで何一つ変更してません！ それは、今回の説明をふまえて、第一回、発端編、第二回を読み直してもらえば、おそらく了解できることでしょう。