「プログラマのためのJavaScript」の番外シリーズ -- いやっ、ホントに。
これはシリーズのハブエントリーです。番号を（0じゃなくて）1にしたのは、全体目次だけじゃなくて内容が含まれるから。
※ 印刷時にはサイドバーは消えるはずです、お試しください。
シリーズ全体目次（予定）
- （この記事；総論）
- 速攻速習編
- 自己適用からゲーデル化へ
- 「展望」への緊急パッチ（オハナシだよ）
- Reflective JavaScript
- 停止問題の構造
- 不完全性定理の構造
今回の内容：
- ゲーデルの不完全性定理とプログラミング
- ゲーデルが示したこと
- 不完全性定理の兄弟 -- 停止問題
- JavaScript使うんだもんね
- 関連する記事（参考）
●ゲーデルの不完全性定理とプログラミング
「ゲーデル」（人名；Kurt Godel、'o'の上に点々が付いてる）や彼の「不完全性定理」とかって、名前くらいは聞いたことがあるでしょ。えっ、ない？ ゲーデルって人は「論理体系で出来ることには限界があるよ」ってことをハッキリと示して（それが不完全性定理）、人々をがっかりさせたのです（喜んだ人もいますが、もちろん）。
「不完全性定理は、人間の知性／理性の限界を示した」とか言う人（例：オッペンハイマー）もいるけど、ゲーデルの定理は、あくまでも論理体系の能力／機能に関するものです。（形式的な）論理体系は一種の抽象機械ですから、不完全性定理の主張を「計算機で出来ることには限界があるよ」と言い換えても差しつかえないでしょう。ですが、「計算機で出来ることの限界」＝「人間の知性／理性の限界」であるかどうかは自明な問題ではありません（難しいから議論の対象にはしません:-)）。
まー、いずれにしても、ゲーデルの不完全性定理は、計算機やプログラミングと無関係ではありません。ゲーデルが展開した論法は、計算機／プログラミングに馴染＜なじ＞みがある人には十分に理解可能です。
そこで、プログラミングの諸概念を使って、ゲーデルの不完全性定理の変種（バリアント）を示してみます。この変種は、道具立てはオリジナルと違いますが、背後にある考え方と基本的メカニズムはオリジナルと同じです。
●ゲーデルが示したこと
ゲーデルの歴史的論文は、"On Formally Undecidable Propositions of Principia Mathematica and Related Systems"（原文はドイツ語；1930年受理、1931年出版）というタイトルです。"Principia Mathematica and Related Systems"とは、要するに（形式的な）論理体系のことです。論理体系のなかに、formal（形式的、機械的）には真偽が決定できない（Undecidableな）命題（Propositions）があるぜ、ってことね。
以下でしばしば登場する「形式的」（formal, formally）って言葉は、「記号の機械的操作に基づく」って意味だと理解してください。だから、形式的な論理体系とは、命題（言明、主張）が記号で表現されていて、推論はその記号を機械的に操作して進めるようなシステムですね。形式的な体系は、コンピュータ上に実装できます。言葉を換えれば、コンピュータ上に実装できるような記号計算の体系を、形式的体系と呼んでいるってことです。
“形式的な論理体系”における命題（記号的表現）とは、例えば、「∀x.(x2 = 1 → x = 1)」、「¬∃x.(x2 < 0)」とか；それぞれ「どんなxでも、xの自乗が1ならばxは1である」、「xの自乗が負になるようなxは存在しない」って意味です。いま、変数xは整数の範囲で考えるとしています。
上の例のように、我々が日常自然言語で述べた整数に関する命題は、記号的な表現に翻訳できます。そして、それらの命題には真偽が定まっているでしょう。もちろん、命題に曖昧さが残らないように十分な取り決めをします。例えば、「x2 = 1 → x = 1」は、xが自然数（負ではない）なら真ですが、-1を考えると真ではありません。変数が走る領域もシッカリと決めないといけませんね。そもそも、「ならば」（記号表現では→）の解釈とかもハッキリさせておかないと、「1を自乗すると間違いなく1なんだから、これは真じゃん」とかイチャモンがつきます。（「ならば」「任意のx（記号的に∀x）」の通常の解釈では、自乗して1だが、それ自身は1ではない数があれば、「∀x.(x2 = 1 → x = 1)」は偽です。）
命題の記号的な表現、その解釈などを曖昧さなく“もの凄くキッチリと”決めれば、どの命題も真偽が決まるだろうと期待されます。その内容が難し過ぎると「真偽が決まる」も怪しい気がするので、内容的には整数とその加減乗除くらいに制限しましょう。“その程度”の命題を算術的的命題と呼びます。
算術的な命題の真偽を実際に確認するには、推論を重ねて証明するか、その否定を証明して反証（証明による反駁＜はんばく＞）するかです。反例を構成して反駁することも否定の証明（反証）の一種です。これは、別に算術的命題に限らなくて、論理的な命題を論理的に示すときの一般的な手順ですね。
ゲーデル以前には、多くの人が、真な命題はいずれは証明されるだろう（そして、偽な命題はいずれは反証されるだろう）と期待していました。証明や反証ができてない命題があるのは、我々の努力や能力が足りないせいであり、「いつか証明／反証されるはず」と考えていたわけです。しかし、算術的命題のなかにも、証明も反証もできないものが存在することをゲーデルは示したのです。
●不完全性定理の兄弟 -- 停止問題
ゲーデルが示した決定不可能な命題は、原理的に証明も反証もできないもので、努力や能力とは何の関係もありません。証明（反証も含む）は、ルールにしたがった手続きであり、機械的な行為です。ゲーデルの結果は、機械的行為では真偽判定が出来ない、と言っています。
真偽判定に限らず、機械的手続きでは出来ないことは色々あります。機械的手続きで計算できない関数、機械的手続きでは列挙できない集合なども存在します。「機械的手続きでは出来ないことがある」という事態を総称して、ここではゲーデル的現象と呼びましょう。
コンピュータに関連したゲーデル的現象があります。「停止問題の決定不可能性」はそのひとつで、プログラムが停止するか（無限に走り続けないか）どうかを決定する手段が原理的に存在しないことを意味します。
「停止問題の決定不可能性」は、「ゲーデルの不完全性定理」と近い、というか兄弟のようなものです。このシリーズでは最初に「停止問題の決定不可能性」を紹介し、ほぼ同様な議論で「ゲーデルの（第一）不完全性定理」を示す予定です。
●JavaScript使うんだもんね
ゲーデルの不完全性定理では、機械的定理証明系の概念（証明可能性の定義）が必要ですが、停止問題（の決定不可能性）は、コンピュータとプログラミングの基礎知識だけで、問題なく完全に理解可能です。逆に、停止問題を理解することを目標として、“基礎知識”を習得するのはよい考えだと思います。その“基礎知識”には次が含まれます。
停止問題が理解できれば、細部はともかくとして、ゲーデルの不完全性定理の実質的内容をつかみ取ることができるはずです。
最後に、冒頭で「『プログラマのためのJavaScript』の番外シリーズ」と言った理由をあかしておきます。停止問題と不完全性定理の説明にJavaScriptを使うからです。このような説明に、JavaScriptはけっこう向いているようです。
●関連する記事（参考）
僕がなんでこんなことを書く気になったかは、次の記事を見てください。
僕のネタモト（情報源）もこれに書いてあります。ただし、今後「発端編」記事を前提にすることはありません。
形式的体系に慣れるには、次の記事が参考になるかもしれません。
自分で言うのもなんですが、上記記事は形式的体系への入門として割とよくできていると思います。
