|
|
|
[[File:Hilbert.jpg|thumb|[[ダフィット・ヒルベルト]]]]
形式主義の偉大なる初期の発案者は[[ダフィット・ヒルベルト]]であった。彼の計画は[[ゲーデルの不完全性定理|完全]]でかつ[[無矛盾性|一貫性（{{Lang|en|consistent}}）]]のある数学の全ての公理化を目的としていた。（「一貫性、無矛盾性（{{Lang|en|consistent}}）」ここでは、システムに由来しうる矛盾がないことを意味する。） ヒルベルトは、「有限算術（{{Lang|en|finitary arithmetic}}）」（[[哲学]]的議論にならないために選ばれた[[自然数]]の通例の[[算術]]のサブシステム）に矛盾がないという仮説から数学的体系の一貫性を示すことを目標とした。完全かつ矛盾のない数学システムを作るヒルベルトの目標は、十分に表現の富んだ矛盾のない公理体系はそれ自体の無矛盾性を決して証明できないことを述べた[[ゲーデルの不完全性定理|ゲーデルの第二不完全性定理]]によって致命的な打撃を受けた。そのような公理体系はサブシステムとして有限算術を含んでいるため、ゲーデルの定理はそのような体系の有限算術に対する相対無矛盾性を証明できないことを含意する（もし証明できたとすると、その体系自体の無矛盾性を証明できたことになるが、ゲーデルの定理はこれが不可能であることを示しているためである）。従って、数学の任意の公理システムが実際に無矛盾であることを示すためには、その体系よりもある意味で強い体系の無矛盾性をまず仮定する必要がある。
ヒルベルトは最初は[[演繹主義]]者だった。しかし、上記から明白に、彼は、本質的に意味のある結果をもたらすために、確実な超数学的方法（{{Lang|en|metamathematical method}}）を熟考した。また、彼は有限算術に関しては[[リアリズム|現実主義]]者であった。後に、彼は解釈にかかわらずどんなものであれ、他の意味にある数学はないと考えた。
|
