証明論
証明論（英語: proof theory）は、数理論理学の一分野であり、証明を数学的対象として形式的に表し、それに数学的解析を施す。
概要
証明は帰納的に定義されたデータ構造で表されることが多く、単純なリスト、入れ子リスト、木構造などがある。これらは論理体系の公理や推論規則によって構築される。そのため、証明論には構文論的（言語学の用語を使うと統語論的）性質があるが、対照的にモデル理論には意味論的（形式意味論も参照）性質がある。モデル理論、公理的集合論、再帰理論などと共に数学基礎論の四本柱とされている。証明論は哲学的論理学の一分野と見ることもでき、その場合の主要な興味は証明論的意味論であり、その技法的基礎として構造証明論 (structural proof theory) の考え方がある。
歴史
論理学の確立には、ゴットロープ・フレーゲ、ジュゼッペ・ペアノ、バートランド・ラッセル、リヒャルト・デーデキントといった先人の業績が寄与しているが、現代証明論は一般にダフィット・ヒルベルトが確立したとされる。ヒルベルトは数学基礎論においてヒルベルト・プログラムと呼ばれる試みを立ち上げた。まずクルト・ゲーデルが独創的な研究を行い、ヒルベルト・プログラムに打撃を与えた。彼の完全性定理は、ヒルベルトの全ての数学を1つの有限主義的形式体系に還元するという目的に適っているように思われたが、その後の不完全性定理によってそれが不可能であることが示された。これらの研究はヒルベルト系と呼ばれる証明計算上で行われた。
ゲーデルの証明論に関する研究と並行して、ゲルハルト・ゲンツェンは構造証明論と呼ばれることになる理論の基礎を築いていた。数年の間にゲンツェンは自然演繹とシークエント計算の中核部分を定式化し、直観論理の形式化の基盤を作り、解析的証明の概念を導入し、ペアノ算術の一貫性について初の組合せ的証明を行った。
形式的証明と非形式的証明
数学で日常的に行われている「非形式的」証明は、証明論で言う「形式的」証明とは異なる。しかしながら、それは形式的証明の高度に抽象化されたスケッチのようなもので、専門家が十分な時間と忍耐を持っていれば、非形式的証明から形式的証明を適切に再構築できるようなものである場合が多い。比喩的に言えば、そのような場合に完全な形式的証明を書くことは、機械語でプログラミングをするようなものである。
現代では、形式的証明は一般に計算機支援証明を補助としてコンピュータを使って構築される。また、その証明がコンピュータで自動的に検証される点も重要である。形式的証明の検証は簡単だが、証明そのものをコンピュータが構築すること（自動定理証明）は一般には非常に困難である。一方、数学における非形式的証明は査読による検証に何週間も要し、それでもまだ誤りが含まれていることが多い。
構造証明論
構造証明論は証明論の一分野であり、解析的証明の記述が可能な証明計算を研究する分野である。解析的証明の記法はゲンツェンがシークエント計算で導入したもので、そこではカット除去定理で表されていた。自然演繹の記法でも解析的証明は記述可能であることが Dag Prawitz によって示されている。その定義は若干複雑である。解析的証明は正規形であり、それは項書き換えにおける正規形と関連している。Jean-Yves Girard の proof net のような特殊な証明計算でも解析的証明の記法はサポートされている。
構造証明論は、カリー＝ハワード同型対応によって型理論とも関連している。カリー＝ハワード同型対応は、自然演繹計算における正規化のプロセスと型付きラムダ計算におけるベータ簡約の構造的類似性を示したものである。これはペール・マルティン＝レーフの直観主義的型理論の基盤となっており、カルテシアン閉圏も含めた三者の同型対応に拡張されることが多い。
言語学では、自然言語の形式意味論に構造証明論を用いて定式化したものとして、Type Logical Grammar、範疇文法、モンタギュー文法がある。