9月29日に「不完全性定理ゼミ」第0回＝ガイダンス回を行い、10月からは本編ゼミ（第1回から第6回）が始まります。
1回の時間も長く（3時間）全6回なので、トータルの時間はけっこうあります。「ゆっくりジックリやれるな」という気もしますが、予備知識ゼロを標榜しているので、「余裕がある」と安心はできません。今から、先のストーリーを細部まで考えておいたほうがいいよね。
んっ、この記事がネタバレになるんじゃないか？ その心配はないでしょ。内容の話ではなくてメタ内容の話だから。
内容：
ゲーデル化とデータ領域
ゲーデルの不完全性定理の証明を律儀に追うのは、語るのも辛いし聞くのも辛いポイントが幾つかあります。なので、技術的な細部をカットして、“その意義”がドータラの“人間知性”がカンタラの、みたいな話に流れがちなんでしょう。ドータラカンタラは楽しいからね。
辛くなるポイントのひとつ*1は、ゲーデル化をちゃんと追いかけるところです。ゲーデル化は、項／論理式／証明などの構文的対象に対して、自然数を対応させる写像です。構文的対象の集合をSとして、G:S→N という写像がゲーデル化〈ゲーデル符号化 | ゲーデル数化〉です。
写像Gの構成には、自然数の加減乗除、つまり小学生でも出来る計算しか使わないので、特に予備知識が要らないのは事実です。しかし、構文的対象Aに対するG(A)は巨大な数になってしまい、具体的に計算するのはまず不可能です。また、ゲーデル数G(A)を見て、Aを想像するのもほぼ不可能です。「具体的なAに対する具体的な数G(A)が必要なわけじゃない」はおっしゃる通りなんですが、そうは言ってもゲーデル数は扱いにくい。
そこで、なんらかのデータの集合（データ領域）Dを準備して、G:S→D とできないかな、という話になります。DがN（自然数全体の集合）じゃなきゃいけない理由はありません。Dは、我々にとってお馴染みで、確実な操作ができる集合ならいいのです。NをDに埋め込めて、自然数の演算はD内で再現（模倣）できる必要はあります。Dは、算数ができる程度にはリッチなデータ領域です。
プログラミング言語の利用
ゲーデル化を分かりやすくするために、プログラミング言語を使う方法があります。項／論理式／証明なども、プログラミング言語のコード（ソースコード）として記述して、データ領域Dも、そのプログラミング言語が持つデータ領域を利用します。
こういった用途に向いているプログラミング言語にLispがあります。項、論理式、証明などをLispコード（S式ともいう）として書きます。ゲーデル化はとても簡単でクォートするだけです。(foo bar baz) というS式は、「barとbazを引数にしてfooする」という意味ですが、'(foo bar baz) なら単なるリストデータになります。
プログラミング言語のコード構文とデータ構文が同じ（または、とても似ている）という性質をホモアイコニシティ〈homoiconicity〉といいます。Lispはホモアイコニックなプログラミング言語のひとつです。ホモアイコニックなプログラミング言語を使えば、項／論理式／証明などをコード構文で書き、ゲーデル化（による符号）はコードに対応するデータで与えることができます。（←この文や次段落の文の意味が分かりにく理由は、この節最後の段落参照。）
この方法は、自然数にコード化する方法（オリジナルのゲーデル化）の問題点を解消しますが、コードとデータがあまりにもソックリだと、コードとデータの違いを意識できなかったり混乱したりするかも知れません。それと、プログラミング言語を知らない人にプログラミング言語の学習を強いることになるのも、「ウーン、ドウカナ？」と思う点です。
と、ここまで書いて気付いたけど； プログラミング言語の「コード」は、項／論理式／証明などを記述するテキストのことで、ゲーデル化の「コード」のほうは、ゲーデル化された符号データのほうですね。同じ言葉で意味が逆だわ、トホホ。このテの用語法の混乱って、けっこうシリアスな障害になるんだよなー（愚痴る）。
コンパイラとゲーデル化
技術者・プログラマにとって、ゲーデル化（に相当する操作）は実はお馴染みのものです。コンパイラはゲーデル化を実行しているとみなせます。プログラミングの意味でのコード（ソースコード）は、構文的対象です。それをコンパイルした結果はバイナリデータ（バイト列／ビット列）です。コンパイラは、構文的対象の集合Sからデータの集合Dへの写像 G:S→D です。
今述べたように、ゲーデル化をプログラミングシステムに埋め込んで説明すれば、技術者・プログラマにとっての日常的経験・直感により、比較的に分かりやすい説明になります。実際僕は、この説明方法をよく使います。
バイナリデータの領域は、2進数表記*2を通じて自然数の領域と1：1対応します。この単純な対応があるので、オリジナルのゲーデル化のデータ領域＝Nと繋げるのも容易です。バイナリデータと自然数を同一視すると、コンパイラは、プログラミング言語のソースコードの領域SからNへの写像となるので、そのまんまゲーデル化です。
この説明方法は、特定の職業・趣味の人々のツールへの慣れ・親しみに依拠しているので一般性はないですね。技術者・プログラマにしろ、コンパイラの中身をよく知ってる人はそうはいないわけで、ゲーデル化の定義を明示的には与えず、ブラックボックスのまま扱う説明方法です。
心理的なインパクト
ゲーデルの不完全性定理が人々を驚かせる理由として、データ領域に自然数の全体Nを使っていることが大きいと思います。自然数は、ほんとに初等的なデータで、知らない人はいません。自然数の計算は、みんな慣れ親しんだ操作です。
そんな自然数に関する命題のなかに、証明も反証（否定の証明）もできない命題があるなんて、ビックリですよね。自然数は分かりきっているモノと感じているからです。これが、複雑怪奇・謎なデータ領域Dに関する命題のなかに、証明も反証もできない命題があるよ、って話だと、そこまでのインパクトはないでしょう。
となると、十分に慣れ親しんでいて、分かりきっていると感じられるデータ領域を選ばないと、不完全性定理の心理的インパクトは損なわれることになります。この観点から、S式の集合やバイナリデータの集合はどうなんでしょうかね？
Lispの説明では、S式〈S-expression〉のこと、あるいはS式全体からなる集合をSexと書きます（書くことがあります）。データ領域としてSexを使った場合の不完全性定理のステートメントは：
- Sexに関する命題のなかに、証明も反証もできない命題がある。
じゃ、どうする
全面的にプログラミング言語／プログラミング・システムを使う案は却下です。先に述べたように「特定の職業・趣味の人々のツールへの慣れ・親しみに依拠している」のがヨロシクナイと思うからです。
項／論理式／証明の書き方は、通常の（比較的標準的な）数学・論理の記法を採用します。これらの項／論理式／証明は、ゲーデル化の写像Gに渡す引数になるので、その意味ではデータとみなす必要があります -- 文字列データとみなすのが妥当でしょう。すると、写像Gの域〈domain〉は、文字列全体の集合Stringの部分集合となります。
では、Gの行き先はどこ？ ゲーデルのオリジナルである G:S→N だと具体的な計算ができないし、G:S→String は混乱しそうだし。ウーム。テキスト（文字列）として書かれた項／論理式／証明をパーズした結果であるツリーはどうかな？
例えば、算術式 5 + 12 に対して G("5 + 12") の値は：
+ ／ ＼ 5 12
+, 5, 12 などの原子記号（トークン）は、ツリーに付いた文字列ラベル "+", "5", "12" だと解釈すれば、文字列データ、または文字列データをもとにした複合構造データの世界で話が済みます。S式と同じっちゃ同じだけど、構文領域側にS式構文を採用しないので、構文側とデータ側の混乱は起きないでしょう。
まだ考える余地はあるし、変更の可能性もあるけど、現状ではこんな方針かな。
