Foundations of Mathematics

A mathematical theory on the foundations of mathematics. Set theory, introduced in the 19th century, immediately gave rise to paradoxes, but on the other hand it has gradually come to be recognized as a basic and useful concept in mathematics. Motivated by the need to clarify and remove these paradoxes, the essence of mathematical cognition and the relationship between logic and mathematics were discussed, and reflections on the logical structure of mathematics and the logic used in mathematical proofs were generally discussed, resulting in three positions: B. A. W. Russell's logicism, Hilbert's formalism, and Luitzen Egbertus Jan Brouwer's (also known as Broer) intuitionism (1881-1966).

Logicism considered mathematics to be a branch of logic, and attempted to reconstruct mathematics in the form of symbolic logic. This was compiled in the three-volume Principia Mathematica (1910-1913), a large work co-authored with A. N. Whitehead. Formalism formalized mathematics using the method of symbolic logic, considered mathematical proof itself to be the transformation of meaningless symbol strings, and attempted to prove the consistency of the axioms of the formalized mathematics by treating it as a mathematical object. Mathematics that targets formalized mathematics is called metamathematics or proof theory, to distinguish it from formalized mathematics. Intuitionism held that mathematical truths and objects are directly grasped by the meaning and content of thinking about mathematics, and took the position that the law of the excluded middle (the law that propositions can only be true or false) is not a universally correct law even in the logic used for proof.

These three positions, while going through fierce debates, influenced each other and developed into the present-day foundations of mathematics. First, G. Cantor's set theory was axiomatized by Zermelo (1908) and AA Fraenkel (1922), and further refined by J. Neumann (1927) and P. Bernays (1936). Gödel proved that the continuum hypothesis, which had been a problem since the birth of set theory, does not contradict other axioms (1938). Furthermore, R. J. Cohen showed that the denial of the continuum hypothesis does not contradict other axioms (1963), showing that the continuum problem is independent of the axiom system of set theory. In proof theory, G. Gentzen proved the consistency of natural number theory (1936). Furthermore, formal systems, including natural number theory, contain propositions that cannot be proved positive or negative (undecidable) within the formal system, and Gödel (1931) presented the incompleteness theorem, which states that it is impossible to prove that a formal system is consistent within the formal system, demonstrating the difficulty of proving the consistency of analysis and axiomatic set theory from the standpoint of proof theory. This direction was followed by the establishment of the concept of computability through Alonzo Church (1903-1995) and Stephen Cole Kleene (1909-1994)'s recursive functions (1936) and Turing's Turing machines (1936), and developed into the theory of computation, which is now closely linked to information science.

Formal systems have come to include intuitionistic systems, multi-valued logic, modal logic, etc. Various theories have been developed through the set-theoretic interpretation of symbols in formal systems. The first achievement in this field was Godel's completeness theorem (1930), which has been greatly developed into model theory today.

[Toshio Nishimura]

Source: Shogakukan Encyclopedia Nipponica About Encyclopedia Nipponica Information | Legend

数学の基礎に関する数学的理論のことである。19世紀に導入された集合論は、ただちに逆理を発生させたにもかかわらず、他方では数学における基本的で有用な概念であることが漸次認められるようになった。この逆理の解明と除去が動機となって、数学の認識の本質、論理学と数学との関係などが論究され、数学の論理的構造、数学の証明に使われる論理への反省が全般的に論じられるようになり、三つの立場が生じた。すなわち、B・A・W・ラッセルの論理主義、ヒルベルトの形式主義、ブラウアー（ブローエルともよばれる）Luitzen Egbertus Jan Brouwer（1881―1966）の直観主義である。

　論理主義では、数学を論理学の一分科であると考え、記号論理の形で数学を再構成することを試みた。これはA・N・ホワイトヘッドと連名の大著『プリンキピア・マテマティカ』Principia Mathematica全3巻（1910～1913）に集大成された。形式主義では、数学を記号論理の方法で形式化し、数学の証明そのものを、意味をもたない記号列の変換と考え、これを数学的対象とし、その形式化された数学の公理系の無矛盾性を証明しようとした。形式化された数学を対象とする数学を、形式化された数学と区別して、超数学あるいは証明論という。直観主義では、数学的真理や対象が、数学を考えていく意味や内容によって直接にとらえられるものであるという考えにたち、証明に用いる論理でも、排中律（命題については、真か偽かの二つの場合しかないとする法則）を普遍的に正しい法則としては認めない立場をとった。

　これらの三つの立場は、激しい論争を経ながら、互いに他に影響しあい、今日の数学基礎論へと発展した。まず、G・カントルの集合論はツェルメロ（1908）、フレンケルA. A. Fraenkel（1922）によって公理化され、J・ノイマン（1927）、ベルナイズP. Bernays（1936）によって整備された。ゲーデルは、集合論発生以来の問題であった連続体仮説が他の公理と矛盾しないことを証明した（1938）。さらにR・J・コーエンは連続体仮説の否定も他の公理と矛盾しないことを示し（1963）、連続体問題が集合論の公理系から独立であることが示された。証明論では、自然数論の無矛盾性がゲンツェンG. Gentzenによって証明された（1936）。また、自然数論を含む形式的体系は、その形式的体系のなかでは肯定も否定も証明できない（決定不能）命題を含み、さらに「形式的体系が無矛盾である」ことがその形式的体系のなかでは証明できない、という不完全性定理がゲーデルによって示され（1931）、解析学、公理的集合論の無矛盾性を証明論の立場から証明することの困難さが示された。この方向は、チャーチAlonzo Church（1903―1995）やクリーニStephen Cole Kleene（1909―1994）による帰納的関数（1936）、チューリングによるチューリング機械（1936）によって、計算可能という概念が確立するとともに、計算の理論へと発展し、今日では情報科学と密接に結び付くものとなった。

　また、形式的体系は直観主義体系、多値論理や様相論理などを包括するようになった。また、形式的体系の記号に対する集合論的意味づけを通して、各種の理論が展開されている。この方面の最初の成果はゲーデルによる完全性の定理（1930）であり、今日ではモデルの理論として大きく発展している。

［西村敏男］

出典　小学館　日本大百科全書(ニッポニカ)日本大百科全書(ニッポニカ)について　情報 | 凡例