証明論のソースを表示

{{脚注の不足|date=2023年8月}}
'''証明論'''（しょうめいろん、{{lang-en|proof theory}}）は、[[数理論理学]]の一分野であり、[[証明 (数学)|証明]]を[[数学的対象]]として形式的に表し、それに数学的解析を施す。

== 概要 ==
証明は帰納的に定義された[[データ構造]]で表されることが多く、単純な[[リスト]]、入れ子リスト、[[木 (数学)|木構造]]などがある。これらは論理体系の[[公理]]や[[推論規則]]によって構築される。そのため、証明論には'''構文論'''的（言語学の用語を使うと[[統語論]]的）性質があるが、対照的に[[モデル理論]]には[[意味論 (論理学)|意味論]]的（[[形式意味論]]も参照）性質がある。[[モデル理論]]、[[公理的集合論]]、[[再帰理論]]などと共に[[数学基礎論]]の四本柱とされている<ref name="wang">{{cite book|last=Wang|first=Hao|title=Popular Lectures on Mathematical Logic|publisher=Van Nostrand Reinhold Company|date=1981年|isbn=0442231091|pages=3–4|author-link=ハオ・ワン}}</ref>。証明論は哲学的論理学の一分野と見ることもでき、その場合の主要な興味は証明論的意味論であり、その技法的基礎として構造証明論 ([[:en:structural proof theory|structural proof theory]]) の考え方がある。

== 歴史 ==
論理学の確立には、[[ゴットロープ・フレーゲ]]、[[ジュゼッペ・ペアノ]]、[[バートランド・ラッセル]]、[[リヒャルト・デーデキント]]といった先人の業績が寄与しているが、現代証明論は一般に[[ダフィット・ヒルベルト]]が確立したとされる。ヒルベルトは[[数学基礎論]]において[[ヒルベルト・プログラム]]と呼ばれる試みを立ち上げた。まず[[クルト・ゲーデル]]が独創的な研究を行い、ヒルベルト・プログラムに打撃を与えた。彼の[[ゲーデルの完全性定理|完全性定理]]は、ヒルベルトの全ての数学を1つの有限主義的形式体系に還元するという目的に適っているように思われたが、その後の[[ゲーデルの不完全性定理|不完全性定理]]によってそれが不可能であることが示された。これらの研究は[[ヒルベルト系]]と呼ばれる証明計算上で行われた。

ゲーデルの証明論に関する研究と並行して、[[ゲルハルト・ゲンツェン]]は構造証明論と呼ばれることになる理論の基礎を築いていた。数年の間にゲンツェンは[[自然演繹]]と[[シークエント計算]]の中核部分を定式化し、直観論理の形式化の基盤を作り、解析的証明の概念を導入し、[[ペアノの公理|ペアノ算術]]の一貫性について初の組合せ的証明を行った。

== 形式的証明と非形式的証明 ==
数学で日常的に行われている「非形式的」証明は、証明論で言う「形式的」証明とは異なる。しかしながら、それは形式的証明の高度に抽象化されたスケッチのようなもので、専門家が十分な時間と忍耐を持っていれば、非形式的証明から形式的証明を適切に再構築できるようなものである場合が多い。比喩的に言えば、そのような場合に完全な形式的証明を書くことは、[[機械語]]でプログラミングをするようなものである。

現代では、形式的証明は一般に[[計算機支援証明]]を補助としてコンピュータを使って構築される。また、その証明がコンピュータで自動的に検証される点も重要である。形式的証明の検証は簡単だが、証明そのものをコンピュータが構築すること（[[自動定理証明]]）は一般には非常に困難である。一方、数学における非形式的証明は[[査読]]による検証に何週間も要し、それでもまだ誤りが含まれていることが多い。

== 証明計算の種類 ==
主な[[証明計算]]は以下の3つである。
* [[ヒルベルト系|ヒルベルト計算]]
* [[自然演繹]]計算
* [[シークエント計算]]

これらはいずれも、[[命題論理]]や[[一階述語論理|述語論理]]（古典論理または[[直観論理]]）、任意の[[様相論理学|様相論理]]、多くの[[部分構造論理]]（[[適切さの論理]]や[[線型論理]]）の完全かつ公理的な定式化を可能とする。実際、これらで表せない論理体系は稀である。

== 一貫性（無矛盾性）の証明 ==
先に述べたように、[[ヒルベルト・プログラム]]は証明の形式理論の研究に拍車をかけた。このプログラムの中心となる考え方は、数学者が必要とするあらゆる洗練された形式理論の一貫性を有限項で証明できたとき、それらの理論を超数学的論証を使って基礎付けることができ、それらの純粋に汎用の表明（より技術的に言えば、それらの証明可能な[[算術的階層]] <math>\Pi^0_1</math>）が有限項的に真であることを示す。そのように基礎付けられたとき、有限項的でない定理群は観念的実体の擬似的規定であるとみなすことができ、無視することができる。

このプログラムの誤りは[[クルト・ゲーデル]]の[[ゲーデルの不完全性定理|不完全性定理]]で明らかとなった。不完全性定理は、何らかの数学的真理を表現できる程度に強力な任意の[[Ω無矛盾|ω無矛盾な理論]]は、ゲーデルの定式化では <math>\Pi^0_1</math> となるそれ自体の一貫性（無矛盾性）を証明できないことを示した。

その後、さらに研究は進み、以下のような成果が得られている。
* ゲーデルの結果の洗練が行われ、特に[[ジョン・バークリー・ロッサー]]は、ω無矛盾性ではなく単純な無矛盾性で済むようにした。
* ゲーデルの業績の核心部分を様相言語で公理化した[[証明可能性論理]] ([[:en:provability logic|provability logic]])
* [[アラン・チューリング]]と[[ソロモン・フェファーマン]]による理論の超限的反復
* 比較的新しい [[自己検証理論]] の発見（自身を語ることができるほど強力な体系だが、ゲーデルの証明不可能性の論証の鍵となった対角線論法を適用できるほど強力でない理論体系）

== 構造証明論 ==
構造証明論は証明論の一分野であり、解析的証明の記述が可能な証明計算を研究する分野である。解析的証明の記法はゲンツェンがシークエント計算で導入したもので、そこでは[[カット除去定理]]で表されていた。自然演繹の記法でも解析的証明は記述可能であることが Dag Prawitz によって示されている。その定義は若干複雑である。解析的証明は[[自然演繹#一貫性、完全性、正規形|正規形]]であり、それは[[項書き換え]]における正規形と関連している。[[:en:Jean-Yves Girard|Jean-Yves Girard]] の [[:en:proof net|proof net]] のような特殊な証明計算でも解析的証明の記法はサポートされている。

構造証明論は、[[カリー＝ハワード同型対応]]によって[[型理論]]とも関連している。カリー＝ハワード同型対応は、自然演繹計算における正規化のプロセスと[[型付きラムダ計算]]におけるベータ簡約の構造的類似性を示したものである。これは[[ペール・マルティン＝レーフ]]の[[直観主義的型理論]]の基盤となっており、[[カルテシアン閉圏]]も含めた三者の同型対応に拡張されることが多い。

[[言語学]]では、[[自然言語]]の[[形式意味論]]に構造証明論を用いて定式化したものとして、Type Logical Grammar、[[範疇文法]]、[[モンタギュー文法]]がある。

== 出典 ==
{{Reflist}}

== 参考文献 ==
*J. Avigad, E.H. Reck, 2001 .[http://www.andrew.cmu.edu/user/avigad/Papers/infinite.pdf “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'' [http://www.springerlink.com/content/n602313107541846/?p=74ab8879ce75445da488d5744cbc3818&pi=0]

== 関連項目 ==
* [[証明 (数学)]]
* [[部分構造論理]]

== 外部リンク ==
{{SEP|proof-theory-development|The Development of Proof Theory|証明論の発展}}
* {{MathWorld|urlname=ProofTheory|title=Proof Theory}}

{{Mathematical logic}}
{{Logic}}
{{DEFAULTSORT:しようめいろん}}
[[Category:メタ論理学]]
[[Category:数理論理学]]
[[Category:数学に関する記事]]
[[Category:証明論|*]]