数学で用いる論理を含み、自然数の理論が展開でき、その公理系、推論規則を実際に与えることができるような形式的体系では、その体系が無矛盾であれば、肯定も否定も証明できない(決定不能)ような命題(その体系で形式化された論理式)がある、という定理である。ゲーデルによって証明された(1931)。ゲーデルは、形式的体系で用いる記号として自然数を採用し、「論理式」「証明」といった概念を数論の概念に直し、「定理である」「無矛盾である」といった命題を数論の命題にし、決定不能な命題Aを構成するきわめて一般的な手法によって定理を証明した。この手法は、ペアノの自然数論、ツェルメロ‐フレンケルの集合論など、知られているほとんどの形式的体系に適用できる。さらに、もとの形式的体系に、このAあるいはAの否定を公理として加えれば、同じ手法で、拡張された体系で決定不能なA′が構成される。また、この数論の命題Aは、形式化されない数学では、数論的に正しい命題であることがわかり、数学の体系の形式化の限界を示すものといえる。命題Aを、「その形式的体系から矛盾が証明できない」、すなわち「その形式的体系は無矛盾である」という。同様に決定不能な命題につくりかえることができる。これから、自然数論を含む数学の形式的体系の無矛盾は、その形式的体系のなかでは証明されないことになり、こうした体系の無矛盾性の証明の困難さを示している。
[西村敏男]
(桂利行 東京大学大学院教授 / 2007年)
出典 (株)朝日新聞出版発行「知恵蔵」知恵蔵について 情報
宇宙事業会社スペースワンが開発した小型ロケット。固体燃料の3段式で、宇宙航空研究開発機構(JAXA)が開発を進めるイプシロンSよりもさらに小さい。スペースワンは契約から打ち上げまでの期間で世界最短を...
12/17 日本大百科全書(ニッポニカ)を更新
11/21 日本大百科全書(ニッポニカ)を更新
10/29 小学館の図鑑NEO[新版]動物を追加
10/22 デジタル大辞泉を更新
10/22 デジタル大辞泉プラスを更新