証明論
 | この記事には参考文献や外部リンクの一覧が含まれていますが、脚注による参照が不十分であるため、情報源が依然不明確です。 |
証明論（しょうめいろん、英語: proof theory）は、数理論理学の一分野であり、証明を数学的対象として形式的に表し、それに数学的解析を施す。
概要
証明は帰納的に定義されたデータ構造で表されることが多く、単純なリスト、入れ子リスト、木構造などがある。これらは論理体系の公理や推論規則によって構築される。そのため、証明論には構文論的（言語学の用語を使うと統語論的）性質があるが、対照的にモデル理論には意味論的（形式意味論も参照）性質がある。モデル理論、公理的集合論、再帰理論などと共に数学基礎論の四本柱とされている[1]。証明論は哲学的論理学の一分野と見ることもでき、その場合の主要な興味は証明論的意味論であり、その技法的基礎として構造証明論 (structural proof theory) の考え方がある。
歴史
論理学の確立には、ゴットロープ・フレーゲ、ジュゼッペ・ペアノ、バートランド・ラッセル、リヒャルト・デーデキントといった先人の業績が寄与しているが、現代証明論は一般にダフィット・ヒルベルトが確立したとされる。ヒルベルトは数学基礎論においてヒルベルト・プログラムと呼ばれる試みを立ち上げた。まずクルト・ゲーデルが独創的な研究を行い、ヒルベルト・プログラムに打撃を与えた。彼の完全性定理は、ヒルベルトの全ての数学を1つの有限主義的形式体系に還元するという目的に適っているように思われたが、その後の不完全性定理によってそれが不可能であることが示された。これらの研究はヒルベルト系と呼ばれる証明計算上で行われた。
ゲーデルの証明論に関する研究と並行して、ゲルハルト・ゲンツェンは構造証明論と呼ばれることになる理論の基礎を築いていた。数年の間にゲンツェンは自然演繹とシークエント計算の中核部分を定式化し、直観論理の形式化の基盤を作り、解析的証明の概念を導入し、ペアノ算術の一貫性について初の組合せ的証明を行った。
形式的証明と非形式的証明
数学で日常的に行われている「非形式的」証明は、証明論で言う「形式的」証明とは異なる。しかしながら、それは形式的証明の高度に抽象化されたスケッチのようなもので、専門家が十分な時間と忍耐を持っていれば、非形式的証明から形式的証明を適切に再構築できるようなものである場合が多い。比喩的に言えば、そのような場合に完全な形式的証明を書くことは、機械語でプログラミングをするようなものである。
現代では、形式的証明は一般に計算機支援証明を補助としてコンピュータを使って構築される。また、その証明がコンピュータで自動的に検証される点も重要である。形式的証明の検証は簡単だが、証明そのものをコンピュータが構築すること（自動定理証明）は一般には非常に困難である。一方、数学における非形式的証明は査読による検証に何週間も要し、それでもまだ誤りが含まれていることが多い。
証明計算の種類
主な証明計算は以下の3つである。
これらはいずれも、命題論理や述語論理（古典論理または直観論理）、任意の様相論理、多くの部分構造論理（適切さの論理や線型論理）の完全かつ公理的な定式化を可能とする。実際、これらで表せない論理体系は稀である。
一貫性（無矛盾性）の証明
先に述べたように、ヒルベルト・プログラムは証明の形式理論の研究に拍車をかけた。このプログラムの中心となる考え方は、数学者が必要とするあらゆる洗練された形式理論の一貫性を有限項で証明できたとき、それらの理論を超数学的論証を使って基礎付けることができ、それらの純粋に汎用の表明（より技術的に言えば、それらの証明可能な算術的階層 
カテゴリ
- 証明論のページへのリンク
