日本大百科全書(ニッポニカ) 「形式主義（数学）」の意味・わかりやすい解説
形式主義（数学）
けいしきしゅぎ
公理主義ともいわれる。ヒルベルトによって提唱された数学の基礎に関する一つの立場である。カントルの集合論を契機として発見された多くの逆理と無限についての論争は、数学の基礎に関する数学理論の発端となるとともに、その解決は、その主要問題の一つともなった。記号論理の方法では、基本概念（「ならば」「かつ」「すべて」など）を記号で表し、通常の推論方法を、式の変形という形式的な法則に還元する。これに加えて、一つの数学的体系で用いられる基本概念をも記号で表せば、その体系における概念、命題などを、記号の組合せ（論理式という）に翻訳できる。さらに、その体系を展開するのに必要な数学上の仮定を、論理式に翻訳して公理として与えれば、その数学の体系を形式化することができる。この形式化された体系のなかでは、その体系の諸定理は論理式として表され、そこで用いられている記号の意味とは関係なく、まったく形式的に導かれることになる。こうして数学の体系は、形式的な公理論に形式化される。公理は、古い考え方では、たとえばユークリッドの幾何でのように、先験的に正しいものと考えられていた。しかし、非ユークリッド幾何が出現して以来、この考え方は放棄されて、理論の単なる仮定と考えられるようになった。公理の正当性は、それらから矛盾が導かれないことによって保証される。矛盾が導かれないことを示すには、非ユークリッド幾何では、座標幾何のなかにその模型をつくり、解析学の無矛盾性に帰着させる方法をとった。
ヒルベルトは、無矛盾性の証明に、従来の方法に加えて、次の考え方を提唱した。すなわち、形式化された証明を、直観的に正しいと納得できる数学の理論（有限の立場という）の対象として扱い（証明論とか超数学という）、その形式化された公理から、肯定と否定がともに形式的に導かれるような論理式が存在しないことを直接に証明しようというのである。この考え方を形式主義という。このヒルベルトの無矛盾性の証明方法に関しては、のちにゲーデルが不完全性定理を証明して、その困難さを示した。
［西村敏男］