証明論
出典: フリー百科事典『ウィキペディア（Wikipedia）』
証明論（英: Proof theory）は数理論理学の一分野であり、証明を数学的オブジェクトとして形式的に表し、それに数学的解析を施す。証明は帰納的に定義されたデータ構造で表されることが多く、単純なリスト、入れ子リスト、木構造などがある。これらは論理体系の公理や推論規則によって構築される。そのため、証明論には統辞論的性質があるが、対照的にモデル理論には意味論的性質がある。モデル理論、公理的集合論、再帰理論などと共に数学基礎論の四本柱とされている[1]。証明論は哲学的論理学の一分野と見ることもでき、その場合の主要な興味は証明論的意味論であり、その技法的基礎として構造証明論（structural proof theory）の考え方がある。
目次 |
[編集] 歴史
論理学の確立には、ゴットロープ・フレーゲ、ジュゼッペ・ペアノ、バートランド・ラッセル、リヒャルト・デーデキントといった先人の業績が寄与しているが、現代証明論は一般にダフィット・ヒルベルトが確立したとされる。ヒルベルトは数学基礎論においてヒルベルト・プログラムと呼ばれる試みを立ち上げた。まずクルト・ゲーデルが独創的な研究を行い、ヒルベルト・プログラムに打撃を与えた。彼の完全性定理は、ヒルベルトの全ての数学を1つの有限主義的形式体系に還元するという目的に適っているように思われたが、その後の不完全性定理によってそれが不可能であることが示された。これらの研究はヒルベルト系と呼ばれる証明計算上で行われた。
ゲーデルの証明論に関する研究と並行して、ゲルハルト・ゲンツェンは構造証明論と呼ばれることになる理論の基礎を築いていた。数年の間にゲンツェンは自然演繹とシークエント計算の中核部分を定式化し、直観論理の形式化の基盤を作り、解析的証明の概念を導入し、ペアノ算術の一貫性について初の組合せ的証明を行った。
[編集] 形式的証明と非形式的証明
数学で日常的に行われている「非形式的」証明は、証明論による「形式的」証明とは異なる。それは言わば、形式的証明の高度に抽象化されたスケッチのようなもので、専門家が十分な時間と忍耐を持っていれば、非形式的証明から形式的証明を再構築できる。多くの数学者にとって、完全な形式的証明を書くことは、機械語でプログラミングするようなものである。
形式的証明は一般に計算機支援証明を補助としてコンピュータを使って構築される。また、その証明がコンピュータで自動的に検証される点も重要である。形式的証明の検証は簡単だが、証明そのものをコンピュータが構築すること（自動定理証明）は一般に非常に困難である。一方、数学における非形式的証明は査読による検証に何週間も要し、それでもまだ誤りが含まれていることが多い。
[編集] 証明計算の種類
主な証明計算は以下の3つである。
これらはいずれも、命題論理や述語論理（古典論理または直観論理）、任意の様相論理、多くの部分構造論理（適切さの論理や線型論理）の完全かつ公理的な定式化を可能とする。実際、これらで表せない論理体系は稀である。
[編集] 一貫性（無矛盾性）の証明
先に述べたように、ヒルベルト・プログラムは証明の形式理論の研究に拍車をかけた。このプログラムの中心となる考え方は、数学者が必要とするあらゆる洗練された形式理論の一貫性を有限項で証明できたとき、それらの理論を超数学的論証を使って基礎付けることができ、それらの純粋に汎用の表明（より技術的に言えば、それらの証明可能な算術的階層 
）が有限項的に真であることを示す。そのように基礎付けられたとき、有限項的でない定理群は観念的実体の擬似的規定であるとみなすことができ、無視することができる。
このプログラムの誤りはクルト・ゲーデルの不完全性定理で明らかとなった。不完全性定理は、何らかの数学的真理を表現できる程度に強力な任意のω無矛盾な理論は、ゲーデルの定式化では となるそれ自体の一貫性（無矛盾性）を証明できないことを示した。
その後、さらに研究は進み、以下のような成果が得られている。
- ゲーデルの結果の洗練が行われ、特にジョン・バークリー・ロッサーは、ω無矛盾性ではなく単純な無矛盾性で済むようにした。
- ゲーデルの業績の核心部分を様相言語で公理化した可能性論理 (provability logic)
- アラン・チューリングと Solomon Feferman による理論の超限的反復
- 比較的新しい self-verifying theories の発見（自身を語ることができるほど強力な体系だが、ゲーデルの証明不可能性の論証の鍵となった対角線論法を適用できるほど強力でない理論体系）
[編集] 構造証明論
構造証明論は証明論の一分野であり、解析的証明の記述が可能な証明計算を研究する分野である。解析的証明の記法はゲンツェンがシークエント計算で導入したもので、そこではカット除去定理で表されていた。自然演繹の記法でも解析的証明は記述可能であることが Dag Prawitz によって示されている。その定義は若干複雑である。解析的証明は正規形であり、それは項書き換えにおける正規形と関連している。Jean-Yves Girard の proof net のような特殊な証明計算でも解析的証明の記法はサポートされている。
構造証明論は、カリー＝ハワード同型対応によって型理論とも関連している。カリー＝ハワード同型対応は、自然演繹計算における正規化のプロセスと型付きラムダ計算におけるベータ簡約の構造的類似性を示したものである。これはペール・マルティン＝レーフの直観主義的型理論の基盤となっており、カルテシアン閉カテゴリも含めた三者の同型対応に拡張されることが多い。
言語学では、自然言語の形式意味論に構造証明論を用いて定式化したものとして、Type Logical Grammar、範疇文法、モンタギュー文法がある。
[編集] 関連項目
[編集] 脚注
- ^ Wang, Hao (1981年). Popular Lectures on Mathematical Logic. Van Nostrand Reinhold Company, 3–4. ISBN 0442231091.
[編集] 参考文献
- J. Avigad, E.H. Reck, 2001 .“Clarifying the nature of the infinite”: the development of metamathematics and proof theory. Carnegie-Mellon Technical Report CMU-PHIL-120.
- A. S. Troelstra, H. Schwichtenberg. Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0-521-77911-1
- G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, Collected Papers of Gerhard Gentzen. North-Holland, 1969.
- L.Moreno-Armella & B.Sriraman (2005).Structural Stability and Dynamic Geometry: Some Ideas on Situated Proof. International Reviews on Mathematical Education. Vol. 37, no.3, pp.130-139 [1]
