現代数学は膨大な証明の集大成として現れます(竹内外史)。
「証明」を対象化する確実な方法はヒルベルトの形式主義
です。形式主義では証明を表現する文章から多義性を除去
するために、いくつかの記号からなる人工的な言語を採用
します。そして記号論理学の方法で数学上の命題をそれら
の記号列で表現します。数学上の命題はその内容を完全に
捨象し、論理的推論は記号列の変形規則として考えます。
こうして便宜上、数学を完全に形式化されたものと見做し
て、その記号列と変形法に対する超数学的な考察によって
数学そのものの論理構造を究明します。さらに超数学的推
論の確実性を保証するためにヒルベルトは「有限の立場」
を提唱しました。「有限の立場」では記号列に対する操作
は有限回に制限されます。
言語：いくつかの無定義概念（関数、述語）を表す記号
変数記号、論理記号、これらの記号から有意義な
命題の形式化である文が一定の規則により生成
公理：真であると想定される文の集合が公理として設定
論理の公理と推論規則：
全数学に共通の論理の公理と推論規則が述語理論
として定義
公理系の取り方はアプリオリには決まらない
論理の公理と推論規則は数学にとってアプリオリに決定
無定義術語の意味は公理系から証明できる諸定理の総体
から陰伏的にのみ定まる
形式主義的公理主義からする数学の本質規定
「数学とは形式的諸関係によって規定される陰伏的理論
(implicit theoruy)である」
形式主義は命題や証明の構造を顕在化するためにその対象に
ついてのイメージの使用を停止するという現象学的エポケー
の所産であり、この還元によって得られたものは記号の有限
列に関する繰り返し操作にすぎず、一片の超越的性格も含ま
ない。
-------倉田令二郎「数学基礎論から見た現代数学」
戻るなら、ここをクリックしてね