このページはゲーデルの第一不完全性定理で証明された、肯定の証明も否定の証明もできないゲーデル文の性質を、コンピュータプログラムの動作で表現するとどうなるだろうと考えて作成したものだ。コンピュータのプログラム言語では命令文はパーサにかけられ、文法を解析された後、実行コードに変換されて実際に作動する。形式的体系の命題の証明可能性を調べるコンピュータプログラムがあったとすると、ある命題が証明可能であるときは、まず、その命題が構文解析され中間コード(その命題の証明である命題の列)が作成された後、そのコードが「証明可能」と判定され「証明可能である」と最終出力されるだろう。構文解析は一般に再帰呼び出しを使ったプログラムが使われる(形式的体系における文の定義もそうである)。したがって、ゲーデル文の場合はこの構文解析の時点で無限の再帰が起きてしまうために、構文解析後の中間出力ができず、「証明可能である」という出力も「否定の証明が可能である」という出力も出来なくなるのではないかと考えた訳である。
アイディアの概要はこうである。「X は証明不可能である」という文の真偽を判定するためには文 X が、「証明不可能である」という述語が定める文の集合に含まれているかどうかを判定する必要がある。そのためにはパーサーはまずこの「証明不可能である」という述語をスタックに積んでおき、文 X を取りだして文を確定したあと、その文が「証明不可能な文」の集合に含まれるかどうかを判定する必要がある。「猫は犬の集合の要素である(という文)は証明不可能である」という文の場合、先ず「証明不可能である」という述語がスタックに積まれる。次に「犬の集合の要素である」という述語がスタックに積まれ、最後に「猫」という主語が解析される。「猫」という主語も、「犬の集合の要素である」という述語もこれ以上分解できないので、「猫は犬の集合の要素である」という文は確定できる。したがって「猫は犬の集合の要素である(という文)は証明不可能である」は真偽を判定できる。
それでは「対角式が証明不可能である(という語)の対角式が証明不可能である」という文の場合はどうであろうか。この場合も「証明不可能である」という述語がスタックに積まれ、「対角式が証明不可能である（という語)の対角式」という文がとりだされる。これはさらに語を加工して文に変換する「対角式」という演算子がスタックに積まれ、「対角式が証明不可能である」という語が取りだされる。「対角式が証明不可能である」というのは語であって文ではないのでこれ以上分解できない。したがって、これを「対角式」という演算子によって文に変換すると「対角式が証明不可能である(という語)の対角式が証明不可能である」というもとの文になる。この文は演算子「対角式」を含んでいるのでそのままでは確定した文とはいえない。したがってこれをまたパーサーは解析しなくてはならなくなり、構文解析が無限に続くために真とも偽とも出力ができなくなってしまうのである。
また、このような無限再帰がおこる文を文として認めたとしても、「対角式が証明不可能である(という語)の対角式が証明不可能である」という命題は、「この命題は証明不可能である」という命題と同じ性質がある。なぜならこの命題は「対角式が証明不可能である(という語)の対角式」という文が「証明不可能である」とのべているが、「対角式が証明不可能である(と言う語)の対角式」というのは「対角式が証明不可能である(という語)の対角式が証明不可能である」というこの命題自身の文になるからである。したがって、この命題が真であれば、この命題は証明不可能であるし、この命題が偽であると仮定すると、この命題は証明可能となり、偽な命題が証明可能となることはないので矛盾する。したがって、この命題は証明も、否定の証明もできないのである。
ここで面白いのは、肯定の証明も否定の証明もできないゲーデル文の発生する仕組みが「証明不可能である」という述語の実質的な定義に依存していないということである。つまり、証明可能性をどのように公理で定義しようとも、「証明不可能である」という述語を使った形式的体系ではゲーデル文が発生してしまう。したがって、どのような形式的体系を持ってしても、証明もその否定の証明もできない命題が発生してしまうのである。これは、どんな無矛盾な理論でもその無矛盾性をその理論で証明することは不可能であるという定理につながっていく。
ある国に高性能の嘘発見機があった。その嘘発見機は一種の証明機械で、それに命題を入力すると命題が証明可能であれば「正」、命題の否定が証明可能であれば「否」を出力する。例えば、「三角形の内角の和は180度である」という命題は「正」である。また「犬は猫である」は「否」である。その国の政府はこの嘘発見機を利用して司法機構を簡素化して費用を削減しようと計画していたのである。
この嘘発見機の動作確認のために、その国の中央論理研究所では日夜研究が続けられていた。ある研究員は、「 X は証明可能」という変数 X を含んだ文について研究していた。これば、変数 X を含んでいるので完全な命題ではない。X に色々な命題を代入すると真偽が判定可能な命題となるのである。たとえば、「「１たす１は２」は証明可能」という命題を嘘発見機に入力したとしよう。「１たす１は２」は証明可能なので、入力した文は証明可能である。したがって、嘘発見器の出力は「正」である。
また、別の研究員は対角式という特殊な文を研究していた。「「赤い」は赤い」というように主語と述語が同じ語でできている文である。この文も嘘発見器にかけることができる。「赤い」という語は赤くはないので、機械は「否」と出力した。そこで彼は次に「Xは対角式が証明不可能」という文を試してみた。X に「赤い」を入れてみたのである。「「赤い」は対角式が証明不可能」という文を機械にかけたところ「正」と出力された。「赤い」の対角式「「赤い」は赤い」は誤りなので、誤りの文は証明不可能であるから、この命題は結局「正」なのである。
面白くなったこの研究員は「「対角式が証明不可能」は対角式が証明不可能」という文を入力してみたのである。そうしたところ機械はいつまで待っても「正」とも「否」とも出力しなかったのである。入力命題が真であれば、入力命題の主語の「対角式が証明不可能」という語の対角式を展開してできる命題「「対角式が証明不可能」は対角式が証明不可能」は証明不可能であるはずである。ところがこの展開した命題はもとの入力命題と全く同じものである。入力命題が証明不可能なのに嘘発見器が「正」と出力することはできない。また、入力命題が偽であったとすると、主語を展開してできる「「対角式が証明不可能」は対角式が証明不可能」という命題は証明可能なので、この命題に対し嘘発見器は「正」と出力しなければならない。ところがこれまたもとの命題と同じものなので、偽な命題を「正」と出力することはないのである。結局、嘘発見器は「正」とも「否」とも出力しないことで、「「対角式が証明不可能」は対角式が証明不可能」という命題が真であることを証明したのである。
ところがもっと恐ろしいことが起こってしまった。件の研究員があろうことか、「この機械が無矛盾である」という命題を入力したら、またまた、機械が黙り込んでしまったのである。なぜなら嘘発見器が「この機械が無矛盾である」の入力に対して「正」を出力したとすると、「この機械が無矛盾ならば「「対角式が証明不可能」の対角式が証明不可能」が証明不可能」という命題も「正」となるはずである。ところが後件の中の「「対角式が証明不可能」の対角式が証明不可能」という部分は「「対角式が証明不可能」の対角式」である。するともとの命題は「この機械が無矛盾ならば「対角式が証明不可能」の対角式が証明不可能」になってしまう。後件の「「対角式が証明不可能」の対角式が証明不可能」という命題は証明不可能な命題なので前件の「この機械が無矛盾ならば」という命題も証明可能になることはない。したがって、嘘発見器は「この機械が無矛盾である」という命題に「正」とも「否」とも出力できないのである。
こうして、全ての命題の真偽を嘘発見機に判定させるという計画は挫折した。それだけでなく、嘘発見機が無矛盾に働いているという保証さえ得られなくなった。「出力が間違っていないので無矛盾に働いているだろう」と信じることしか出来ないと言うことが分かってしまったのである。政府は嘘発見機による合理化計画を断念し、人間による作業の役割も見直すことを決定した。