数学的厳密性

数学的厳密性は、数学的証明の厳密な方法と数学的実践の厳密な方法の両方を指すことがある。

数学的厳密さは、数学的証明の一種のゴールドスタンダードとしてしばしば引用される。その歴史は、ギリシャの数学、特に、ユークリッドの『原論』にさかのぼる 。

19世紀まで、この『原論』は非常に厳格で深遠であると見なされていたが、19世紀後半に、ヒルベルトその他の数学者は証明が特定の仮定を暗黙のうちに残していることに気づいた 。これは、すべての仮定を述べる必要があり、暗黙のうちに何も残せないという厳密な証明の考え方に反していた。証明に見られる厳密さのこのギャップに対処するために、ヒルベルトの公理、ビルコフの公理、タルスキの公理などの公理的方法を使用した新しい基礎論が開発された。

19世紀に、「厳密」という用語は、微積分を扱うときに抽象化のレベルが上がることを表すために使用され始め、最終的には数学分析として知られるようになった。コーシーの理論は、オイラーとガウスの古い理論に厳密さを加えた。リーマンの理論は、コーシーの理論に厳格さを加えた。ワイエルシュトラスの理論はリーマンの理論に厳格さを加え、最終的には分析の算術化に至った。1870年代から、この用語は徐々にカントールの集合論に関連付けられるようになった。

数学的厳密性は、アルゴリズムによる証明チェックの快適さとしてモデル化できる。確かに、コンピューターの助けを借りて、いくつかの証拠を機械的にチェックすることが可能である 。形式的厳密性とは、形式言語による高度な完全性の導入であり、 ZFCなどの集合論を使用してそのような証明を体系化できる（自動定理証明を参照）。

公開されている数学的議論は厳密さの基準に準拠している必要があるが、象徴的な言語と自然言語の混合で書かれている。この意味で、書かれた数学的記述は形式的な証明のプロトタイプである。多くの場合、書面による証明は、まだ正式化されていない可能性がある、厳密なものとして受け入れられる。数学者が非公式に書くためにしばしば引用する理由は、完全に正式な証明はより長く扱いにくい傾向があり、それによって議論の線が曖昧になるためである。人間の直感に明白に見える議論は、実際には公理からかなり長い形式的な導出を必要とするかもしれない。特によく知られている例を、ホワイトヘッドとラッセルが、プリンキピア・マテマティカで「1 + 1 = 2」について示している。要するに、書面による記述では、形式よりも理解しやすさが優先される。

それでも、自動定理証明の支持者は、証明の形式化は、非公式の書面による談話のギャップや欠陥を開示することによって、数学的な厳密さを改善すると主張するかもしれない。証明の正しさが争われる場合、形式化は、誤解やあいまいさを減らすのに役立つため、そのような論争を解決する方法である。