証明論

証明論について

証明論（しょうめいろん、英語: proof theory）は、数理論理学の重要な分野のひとつであり、証明を数学的な対象として扱い、それに対して形式的に分析を行う学問です。この理論では、証明はインデクティブに定義されたデータ構造に基づいて表現されることが多いです。具体的には、単純なリストや入れ子リスト、木構造などが用いられ、これらは論理体系における公理や推論規則を基に構築されます。

概要

証明論は構文論的な特性を持つ一方で、モデル理論は意味論的な特性を持っています。証明論は哲学的な論理学の一分野と見なすこともでき、そこで主に関心が持たれているのが証明論的意味論です。そのため、構造証明論と呼ばれる技法的な基盤が重要な役割を果たしています。

歴史

証明論の基礎を築いた先人たちには、ゴットロープ・フレーゲ、ジュゼッペ・ペアノ、バートランド・ラッセル、リヒャルト・デーデキントなどがいます。しかし、現代の証明論は主にダフィット・ヒルベルトによって確立されました。ヒルベルトは数学基礎論のためにヒルベルト・プログラムを立て、数学的証明の形式理論の研究を推奨しました。

しかし、このプログラムはクルト・ゲーデルの研究によって強い打撃を受けました。ゲーデルの完全性定理は、ヒルベルトの目指す目標に適しているように見えましたが、後の不完全性定理によって、その目的の不可能性が示されました。これに伴い、証明論における重要な研究はヒルベルト系に基づいて行われました。

同時期にゲルハルト・ゲンツェンも構造証明論の理論を築きました。彼は自然演繹とシークエント計算の基本部分を定義し、直観論理を形式化するための基盤を整えました。また、解析的証明の概念を導入し、ペアノ算術の一貫性についての最初の組合せ的証明に成功しました。

形式的証明と非形式的証明

数学で一般的に用いられる「非形式的」証明は、証明論でいう「形式的」証明とは異なります。一般に、非形式的証明は形式的証明の高度に抽象化されたスケッチにあたります。専門家が適切な時間と忍耐を持てば、非形式的証明からでも形式的証明を再構築することが可能です。

現代の形式的証明は、コンピュータ支援証明によって支援されています。これにより、証明が自動的に検証されることが可能です。しかし、形式的証明の構築は多くの困難がある一方で、非形式的証明は査読を経て確認される間に数週間を要し、誤りが残ることもしばしばあります。

証明計算の種類

主に知られている証明計算には、ヒルベルト計算、自然演繹計算、シークエント計算の3つがあります。これらはさまざまな論理体系の完全かつ公理的な定式化を可能にします。これらの計算に表せない論理体系は非常に少ないです。

一貫性の証明

ヒルベルト・プログラムは証明理論の進展を促しました。このプログラムの核心は、数学者が利用する全ての洗練された形式理論の一貫性を、有限項によって証明できるべきだという考え方です。これにより、それらの理論を超数学的な証明によって基礎付けることができると期待されていました。しかし、クルト・ゲーデルの不完全性定理によって、この理論の限界が明らかになりました。

構造証明論

構造証明論は証明論の一部門であり、解析的証明の記述が可能な証明計算を研究する分野です。ゲンツェンは、シークエント計算によって解析的証明の記法を導入し、その後も自然演繹の記法でも解析的証明が記述できることが示されました。さらに、構造証明論は型理論とも関連し、型付きラムダ計算におけるプロセスとの類似性が示されています。例えば、自然言語の形式意味論にも、この構造証明論を用いた多くの理論が存在しています。

もう一度検索