ゲーデルの不完全性定理
不完全性定理は他の論理構造と同じく抽象代数による簡易な表現が可能である。リンデンバウム代数(英語版)を次のように定義する。
理論 T {\displaystyle T} のリンデンバウム代数 T L {\displaystyle T_{L}} は,文に順序構造を入れたものである。
順序は、もし理論 T {\displaystyle T} で A ⇒ B {\displaystyle A\Rightarrow B} を証明できるならば A ≥ B {\displaystyle A\geq B} と定義される。
A {\displaystyle A} と B {\displaystyle B} の順序が等しいなら、 A {\displaystyle A} と B {\displaystyle B} を同一視する。
T {\displaystyle T} で無条件に証明可能な文 A {\displaystyle A} は,この順序で最小元となり、 T {\displaystyle T} で ¬ A {\displaystyle \lnot A} を証明できるとき、 A {\displaystyle A} はこの順序の最大元となる。よって最大元でも最小元でもないものは独立命題のみ。つまり不完全であるためにはリンデンバウム代数の位数は3以上であることが要請される。
数学と計算機科学(コンピュータ科学)において、「決定不能」という言葉には二つの異なった意味がある。一つ目は証明論の文脈でゲーデルの定理に関連して使われる意味であり、特定の形式的体系の下で或る命題を証明も反証もできないことを言う。二つ目は計算可能性理論に関連した用法であり、命題ではなく決定問題に適用される。決定問題とは入力に対して答が真か偽のいずれかになるような問題である。ある問題を全ての入力に対して正しく解答するようなアルゴリズムが存在しないとき(すなわち特性関数が計算可能関数でないとき)、そうした問題は決定不能であると言う。
不完全性定理は、自然数論が一つ目の意味で決定不能であることを主張している。一方、述語論理の論理式が充足可能か否かを判定する充足可能性問題は決定問題にあたるが、不完全性定理によって、二番目の意味で決定不能である。つまり、述語論理の論理式が充足不能であれば、その論理式から矛盾を導く証明を見つけることができるが、充足可能であるときにその旨、回答を返すアルゴリズムは存在し得ない。
ゲーデルとポール・コーエンの仕事を合わせて、決定不能命題の確かな実例が得られた。連続体仮説はZFC(集合論における標準的な公理系)の下では証明も否定の証明もできない。
肯定命題 P r o v a b l e A R G ( m , m ) {\displaystyle ProvableARG(m,m)} が証明可能だとすると、
P r o v a b l e A R G ( m , m ) ⇔ P r o v a b l e ( n p m m ) {\displaystyle ProvableARG(m,m)\Leftrightarrow Provable(npmm)}
により
P r o v a b l e ( n p m m ) {\displaystyle Provable(npmm)}
が証明可能である。
このときω無矛盾性を前提すると、 n p m m {\displaystyle npmm} をゲーデル数とする論理式 ¬ P r o v a b l e A R G ( m , m ) {\displaystyle \lnot ProvableARG(m,m)} が証明可能である。
それ故、矛盾が証明されるが、これは自然数論が無矛盾であるという仮定に反する。
菊池, 誠『不完全性定理』(初版1刷)共立出版、2014年10月25日。ISBN 978-4320110960。
フランセーン, トルケル 著、田中一之 訳『ゲーデルの定理:利用と誤用の不完全ガイド』みすず書房、2011年3月25日。ISBN 978-4-622-07569-1。
しかし一方で哲学や神学は、ゲーデルや不完全性定理を自分たちへ結びつけようとしてきた。
アラン・ソーカルとジャン・ブリクモンは、脱近代主義(ポストモダニズム)に対する論評『「知」の欺瞞』の中で、「ゲーデルの定理こそ汲めども尽きぬ知的濫用の泉である」と述べ、レジス・ドブレ、ミシェル・セールらの文章を批判している。また、哲学者によるゲーデル関係の本が、フランセーンの本と同じ頃に書店販売されていたが、哲学者の本は専門誌によって酷評された。その本は全体として読みやすく一般読者からの評判は高かったが、ゲーデルの証明の核(不動点定理)について、根本的な勘違いをしたまま説明していた。同様の間違いは他の入門書などにもあり、田中は
と述べている。哲学者または宗教家が、
といった考えを表明することは珍しくない。しかし、不完全性定理とは「算術の公理系PAや公理的集合論ZFCのような形式体系を扱う数学の定理」であり、哲学や宗教はこの点を踏まえていない。要するに不完全性定理とは、数学内の「形式体系」(フォーマルシステム)についての定理である。確かに、思想・哲学・神学・信仰・聖書・法律・裁判等を「形式」や「体系」や「形式体系」と呼ぶ人も存在するが、それらは数学内の一分野「形式体系」ではない。数学内の「形式体系」を研究し応用できる範囲は、数学や計算機(コンピュータ)である。
嘘つきのパラドックス(「ウソつきの逆理」)には、「この文は偽である」といった代表的表明があるが、このパラドックスも、不完全性定理が誤用されている一例として挙げられている。
不完全性定理が成立しない例としてはユークリッド幾何学、プレスバーガー算術、実閉体と代数的閉体の理論におけるタルスキの定理などがある。
不完全性定理は「『帰納的公理化可能な自然数論を含む理論が、無矛盾(ω無矛盾)であれば』~」という形の定理である。したがって、帰納的公理化可能であっても自然数論を含まない公理系や、帰納的公理化可能でない理論が完全であっても、不完全性定理とは矛盾しない。
真の算術やペアノ算術の無矛盾完全拡大などは無矛盾かつ完全であるが、帰納的公理化可能でない。とくに真の算術は算術的に定義不能である。この結果はタルスキの真理定義不可能性として知られる。
プレスバーガー算術は帰納的公理化可能、無矛盾かつ完全である。プレスバーガー算術は加法しか含まない公理系であり、ゲーデル数によるコード化のテクニックを扱えない。そのため、不完全性定理は適用できない。また、実閉体の理論やユークリッド幾何学も帰納的公理化可能、無矛盾かつ完全であり、(直観に反して)算術を含まないため、不完全性定理は適用できない。したがって実閉体の理論は(計算可能性の意味で)決定可能である。もっと精密にいうと実閉体の理論では量化記号消去が可能である。この事実は数式処理系の実装などに応用されている。
なお、群や環の公理などは、「帰納的公理化可能だが自然数論を含まない無矛盾な公理系」であり、不完全性定理は適用できないが、不完全である。例えば、可換群と非可換群がともに存在することから、健全性定理より、群の公理からは積の可換性は証明も反証もできない。