ゲーデルの不完全性定理
青本和彦(編); 上野健爾(編); 加藤和也(編); 神保道夫(編); 砂田利一(編); 高橋陽一郎(編); 深谷賢治(編); 俣野博(編) ほか『岩波 数学入門辞典』(第1刷)岩波書店、2005年9月29日。ISBN 978-4000802093。
日本数学会(編)『岩波 数学辞典』(第4版第3刷)岩波書店、2011年10月25日。ISBN 978-4000803090。
Gödel, Kurt; Hirzel, Martin (2000-11-27), “On formally undecidable propositions of Principia Mathematica and related systems I” (PDF), Boulder: 173-196, http://hirzels.com/martin/papers/canon00-goedel.pdf
Gödel, Kurt (2002), “Some metamathematical results on completeness and consistency, On formally undecidable propositions of Principia mathematica and related systems I, and On completeness and consistency”, in van Heijenoort, Jean, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Source Books in the History of the Sciences (Fourth Printing ed.), Harvard University Press, pp.
理学博士・数学基礎論研究者である菊池誠の『不完全性定理』によれば、数学史上で「数学の正しさと無矛盾性に対する確信が揺らいだことがかつて一度だけあった」。19世紀末~20世紀初めには、数学の中でいくつも逆理が発見され、数学の基礎についての「不安の時代」が発生した。そうして数学の無矛盾性や「そもそも定理や証明とは何なのか」といった哲学的な問いに対し、伝統的な哲学の手法ではなく数学の手法(形式主義)で答える試みがなされ、そこから数学の一分野「数学基礎論」が生まれた。
数学の世界全体の無矛盾性を「有限の立場」で証明して数学を危機から救おうとしたヒルベルト・プログラムが、実現不可能であることをゲーデルの不完全性定理が明らかにした。ヒルベルト・プログラムは破綻した一方で、公理的集合論が整備されて「無矛盾」と見なされたこと、「算術の世界の無矛盾性」が証明されたことなどによって「不安の時代」は終わり、数学基礎論が哲学から決別した。数学基礎論上で不完全性定理は、哲学的なものとしてでなく、数学的な応用可能性として重視されるようになった。またこの定理は、電子技術を伴うコンピュータ科学(計算機科学)の重要な基本定理でもある。
前掲書によると、20世紀初めは数学者と哲学者は共に数学の基礎について論じていたが、「今では数学者と哲学者は極めて疎遠である」。数学についての哲学的議論を、数学者は「最近の数学を無視した色褪せた100年前の論争の焼き直し」と見なしている。不完全性定理を含む数学分野(数学基礎論)を数学者が「哲学のようなもの」と呼ぶ場合、それは「哲学のような深い立派なもの」ではなく「哲学のようなツマラナイコト」を意味していると言う。
概要でも説明したように、ゲーデル数というテクニックを使って間接的に自己言及を可能とし、ゲーデル文を構成する。コンピュータでは全てのデータを一意な数値で表しており、特に文字列や論理式そして論理式の列も数値で表す。このように、論理式を数値で表す行為を論理式のゲーデル数化といい、命題 P {\displaystyle P} に対応する数値を P {\displaystyle P} のゲーデル数という。
ゲーデル数化により、論理式に関する様々な性質を論理式として表すことができる。たとえば、
A x i o m ( x ) {\displaystyle Axiom(x)} : x {\displaystyle x} は公理のゲーデル数である。
M P ( x , y , z ) {\displaystyle MP(x,y,z)} : x {\displaystyle x} をゲーデル数に持つ論理式と y {\displaystyle y} をゲーデル数に持つ論理式からモーダスポネンスにより z {\displaystyle z} をゲーデル数に持つ論理式が導ける。
といった論理式を作ることができる。ここで、 A x i o m {\displaystyle Axiom} や M P {\displaystyle MP} の引数が論理式自身ではなく自然数であることが重要である。
否定命題 ¬ P r o v a b l e A R G ( m , m ) {\displaystyle \lnot ProvableARG(m,m)} が証明可能とすると、 P r o v a b l e ( n p m m ) {\displaystyle Provable(npmm)} は真である。このとき Σ 1 {\displaystyle \Sigma _{1}} 完全性より P r o v a b l e ( n p m m ) {\displaystyle Provable(npmm)} は証明可能である。
一方 ¬ P r o v a b l e A R G ( m , m ) {\displaystyle \lnot ProvableARG(m,m)} は
「 m {\displaystyle m} をゲーデル数に持つ論理式に m {\displaystyle m} を代入したものは証明不能」
という意味である。