証明理論

証明理論は数理論理学と理論計算機科学の主要な分野^[1]であり、その中で証明は正式な数学的対象として扱われ、数学的手法による分析が容易になります。証明は通常、リスト、ボックスリスト、ツリーなどの帰納的に定義されたデータ構造として提示され、与えられた論理システムの公理と推論規則に従って構築されます。したがって、証明理論は本質的に統語論的であり、本質的に意味論的であるモデル理論とは対照的です。

証明理論の主な分野には、構造証明理論、順序分析、証明可能性論理、逆数学、証明マイニング、自動定理証明、証明複雑性などがあります。また、コンピューターサイエンス、言語学、哲学への応用にも重点を置いた研究が多くあります。

論理の形式化はゴットロブ・フレーゲ、ジュゼッペ・ペアノ、バートランド・ラッセル、リヒャルト・デデキントなどの研究によって大きく前進したが、現代の証明理論の歴史は、数学基礎論におけるヒルベルト・プログラムと呼ばれるものを始めたデイヴィッド・ヒルベルトによって確立されたとよく見られる。このプログラムの中心的な考え方は、数学者が必要とするすべての洗練された形式理論の無矛盾性の有限証明を与えることができれば、これらの理論を、純粋に普遍的な主張（より技術的には証明可能文）のすべてが有限に真であることを示すメタ数学的議論によって根拠づけることができるというものである。いったんそのように根拠づけられれば、存在定理の非有限な意味は気にせず、これらを理想的な実体の存在の疑似意味のある規定と見なす。 ${\displaystyle \Pi _{1}^{0}}$

このプログラムの失敗は、クルト・ゲーデルの不完全性定理によって引き起こされた。この定理は、ある単純な算術的真理を表現するのに十分な強さを持つω無矛盾理論は、ゲーデルの定式化では 文である自身の無矛盾性を証明できないことを示した。しかし、ヒルベルトのプログラムの修正版が登場し、関連するトピックに関する研究が行われた。これは特に次のことをもたらした。 ${\displaystyle \Pi _{1}^{0}}$

• ゲーデルの結果の改良、特にJ. バークレー ロッサーの改良により、上記の ω-一貫性の要件が単純な一貫性に弱められました。
• ゲーデルの結果の核心を様相言語、証明可能性論理の観点から公理化する。
• アラン・チューリングとソロモン・フェファーマンによる理論の超限反復。
• 自己検証理論の発見。自己について語るには十分強力だが、ゲーデルの証明不可能性議論の鍵となる対角線上の議論を実行するには弱すぎるシステム。

ヒルベルトのプログラムの盛衰と並行して、構造的証明理論の基礎が築かれつつあった。ヤン・ウカシェヴィチは1926年に、論理の推論規則における仮定から結論を導き出すことができれば、論理の公理的表現の基礎としてのヒルベルト体系 を改良できると示唆した。これに対して、スタニスワフ・ヤシコフスキ（1929年）とゲルハルト・ゲンツェン（1934年）は独立して、自然演繹計算と呼ばれるそのような体系を提示した。ゲンツェンのアプローチでは、導入規則で表現される命題を主張する根拠と、除去規則で表現される命題を受け入れることの結果との間の対称性という概念が導入され、この概念は証明理論において非常に重要であることが証明された。^[2] ゲンツェン（1934）はさらに、同様の精神で発展した論理接続子の二重性をよりよく表現する計算であるシーケント計算のアイデアを導入し、 ^[3]直観主義論理の形式化に根本的な進歩をもたらし、ペアノ算術の一貫性の最初の組合せ論的証明を提供しました。自然演繹とシーケント計算の提示は、証明理論に 解析的証明の基本的なアイデアをもたらしました。

構造証明理論は証明理論のサブ分野であり、証明計算の詳細を研究します。最もよく知られている 3 つの証明計算のスタイルは次のとおりです。

• ヒルベルト計算
• 自然演繹計算
• 後続計算

これらはそれぞれ、古典的または直観主義的な命題論理または述語論理、ほぼすべての様相論理、および関連性論理や線形論理などの多くの部分構造論理の完全かつ公理的な形式化を与えることができます。実際、これらの計算のいずれかで表現できない論理を見つけることはまれです。

証明理論家は、通常、解析的証明の概念を支持する証明計算に興味を持っています。解析的証明の概念は、シーケント計算のためにゲンツェンによって導入されました。そこでは、解析的証明はカットフリーの証明です。カットフリー証明への関心の多くは、部分式の性質: カットフリー証明の最終シークエント内の各式は、いずれかの前提の部分式です。これにより、シークエント計算の一貫性を簡単に示すことができます。空のシークエントが導出可能であれば、何らかの前提の部分式でなければなりませんが、そうではありません。ゲンツェンのミッドシークエント定理、クレイグ補間定理、およびエルブランの定理も、カット除去定理の系として成り立ちます。

ゲンツェンの自然演繹計算は、ダグ・プラウィッツによって示されたように、解析的証明の概念もサポートしています。定義は少し複雑です。解析的証明は正規形であり、項書き換えの正規形の概念に関連していると言います。ジャン＝イヴ・ジラールの証明ネットなどのより珍しい証明計算も、解析的証明の概念をサポートしています。

還元論理から生じる解析的証明の特定のファミリーは、目標指向の証明探索手順の大きなファミリーを特徴付ける焦点を絞った証明です。証明システムを焦点を絞った形式に変換する能力は、証明システムが構文的に一貫していることを示すカットの許容性と同様に、その構文品質の良い指標です。^[4]

構造証明理論は、カリー・ハワード対応によって型理論と結びついており、これは自然演繹計算における正規化のプロセスと型付きラムダ計算におけるベータ還元との間の構造的類似性を観察する。これは、ペル・マルティン＝レーフによって開発された直観主義型理論の基礎となり、しばしば三者対応に拡張され、その第 3 の脚はデカルト閉カテゴリである。

構造理論の他の研究テーマには、構造証明理論の解析的証明の中心的アイデアを応用して、幅広い論理に対する決定手順と半決定手順を提供する解析的タブローや、部分構造論理の証明理論などがあります。

順序解析は、算術、解析、集合論のサブシステムの組み合わせの一貫性証明を提供する強力な手法です。ゲーデルの第二不完全性定理は、十分な強度を持つ理論では有限の一貫性証明は不可能であることを示すものとして解釈されることがよくあります。順序解析を使用すると、理論の一貫性の無限の内容を正確に測定できます。一貫性のある再帰的に公理化された理論 T の場合、有限算術では、特定の超限順序数の整基礎性が T の一貫性を意味することを証明できます。ゲーデルの第二不完全性定理は、そのような順序数の整基礎性が理論 T で証明できないことを意味します。

順序分析の結果には、(1)構成理論と比較した古典的な2階算術と集合論のサブシステムの一貫性、(2)組合せ独立性の結果、(3)証明可能な全再帰関数と証明可能な整根拠順序数の分類が含まれます。

順序解析はゲンツェンによって始められ、ゲンツェンは超限帰納法を用いて順序数 ε ₀までのペアノ算術の無矛盾性を証明した。順序解析は、第一階および第二階算術と集合論の多くの断片に拡張されてきた。大きな課題の1つは、非述語的理論の順序解析であった。この方向への最初のブレークスルーは、竹内による Π の無矛盾性の証明であった。¹
₁-CA ₀順序図法を使用します。

証明可能性論理は様相論理であり、ボックス演算子は「証明可能である」と解釈されます。ポイントは、かなり豊富な形式理論の証明述語の概念を捉えることです。ペアノ算術で証明可能であることを捉える証明可能性論理 GL (ゲーデル-レーブ) の基本公理として、ヒルベルト-バーネイの導出可能性条件とレーブの定理(A の証明可能性が A を意味することが証明可能であれば、A は証明可能である) の様相類似を採用します。

ペアノ算術と関連理論の不完全性に関する基本的な結果のいくつかは、証明可能性論理に類似点があります。たとえば、矛盾が証明できない場合は、矛盾が証明できないことも証明できないというのは GL の定理です (ゲーデルの第二不完全性定理)。不動点定理の様相類似点もあります。ロバート ソロベイは、様相論理 GL がペアノ算術に関して完全であることを証明しました。つまり、ペアノ算術の証明可能性の命題理論は、様相論理 GL によって完全に表現されます。これは、ペアノ算術の証明可能性に関する命題推論が完全かつ決定可能であることを直接的に意味します。

証明可能性論理に関するその他の研究は、一階証明可能性論理、多様証明可能性論理（1 つの様相がオブジェクト理論における証明可能性を表し、別の様相がメタ理論における証明可能性を表す）、および証明可能性と解釈可能性の相互作用を捉えることを目的とした解釈可能性論理に焦点を当てています。ごく最近の研究では、段階的証明可能性代数を算術理論の順序分析に適用しています。

逆数学は、数学の定理を証明するためにどの公理が必要かを決定する数理論理学のプログラムである。 ^{[5]この分野は}ハーヴェイ・フリードマンによって創設された。その定義方法は、「定理から公理へと逆方向にたどる」と表現でき、公理から定理を導く通常の数学的実践とは対照的である。逆数学プログラムは、選択公理とゾルンの補題がZF集合論上で同値であるという古典的な定理などの集合論の結果によって予兆された。しかし、逆数学の目標は、集合論の可能な公理ではなく、数学の通常の定理の可能な公理を研究することである。

逆数学では、フレームワーク言語と基本理論 (コア公理システム) から始めます。この基本理論は、関心のある定理のほとんどを証明するには弱すぎますが、これらの定理を述べるために必要な定義を展開するには十分強力です。たとえば、「実数の有界シーケンスには上限がある」という定理を研究するには、実数と実数のシーケンスについて説明できる基本システムを使用する必要があります。

基本システムで述べることができるが、基本システムでは証明できない各定理について、その定理を証明するために必要な特定の公理システム (基本システムよりも強い) を決定することが目標です。システムS が定理T を証明するために必要であることを示すには、2 つの証明が必要です。最初の証明は、 TがSから証明可能であることを示します。これは、システムSで実行できることの正当性を伴う通常の数学的証明です。反転と呼ばれる 2 番目の証明は、 T自体がS を意味することを示します。この証明は基本システムで実行されます。反転により、基本システムを拡張する公理システムS′は、 T を証明しながら Sよりも弱くなることはできないことが確立されます。

逆数学における驚くべき現象の1つは、ビッグファイブ公理系の堅牢性である。これらのシステムは、強度が増す順に、RCA ₀、WKL ₀、ACA ₀、ATR ₀、Πという頭文字で命名されている。¹
₁-CA ₀。逆数学的に解析された通常の数学のほぼすべての定理は、これら5つのシステムのいずれかと同等であることが証明されています。最近の多くの研究は、RTのように、この枠組みにうまく当てはまらない組み合わせ原理に焦点を当てています。²
₂(ペアに関するラムゼーの定理)。

逆数学の研究では、証明理論だけでなく 再帰理論の方法や技術も取り入れられることが多いです。

関数的解釈とは、非構成的理論を関数的理論で解釈することです。関数的解釈は通常、2 段階で進行します。まず、古典的理論 C を直観主義的理論 I に「還元」します。つまり、C の定理を I の定理に変換する構成的マッピングを提供します。次に、直観主義的理論 I を関数 F の量化子のない理論に還元します。これらの解釈は、構成的理論に対する古典的理論の一貫性を証明するため、ヒルベルトのプログラムの形式に貢献します。関数的解釈が成功すると、無限理論を有限理論に、非述語的理論を述語的理論に還元できるようになりました。

関数的解釈は、簡約理論の証明から構成的な情報を引き出す方法も提供します。解釈の直接的な結果として、通常、I または C のいずれかでその全体性が証明できる任意の再帰関数は F の項によって表されるという結果が得られます。I での F の追加解釈を提供できる場合 (場合によっては可能です)、この特徴付けは実際、正確であることが通常示されます。F の項は、原始再帰関数や多項式時間計算可能関数などの自然な関数クラスと一致することがよくあります。関数的解釈は、理論の順序分析を提供し、その証明可能な再帰関数を分類するためにも使用されています。

関数解釈の研究は、有限型の関数の量化子のない理論におけるクルト・ゲーデルの直観主義算術の解釈から始まりました。この解釈は、一般に弁証法解釈として知られています。直観主義論理における古典論理の二重否定解釈とともに、これは古典算術を直観主義算術に還元します。

日常的な数学実践における非公式な証明は、証明理論の正式な証明とは異なります。それらはむしろ、十分な時間と忍耐があれば、専門家が少なくとも原理的には正式な証明を再構築できるような高レベルのスケッチのようなものです。ほとんどの数学者にとって、完全に正式な証明を書くことは、一般的に使用するにはあまりにも衒学的で冗長です。

形式的な証明は、対話型定理証明においてコンピュータの助けを借りて構築されます。重要なことに、これらの証明はコンピュータによって自動的にチェックできます。形式的な証明のチェックは通常簡単ですが、証明を見つけること(自動定理証明) は一般的に困難です。対照的に、数学の文献における非公式な証明は、ピアレビューによるチェックに数週間かかる必要があり、それでもエラーが含まれている可能性があります。

言語学では、型論理文法、範疇文法、モンタギュー文法は、構造証明理論に基づく形式主義を適用して、形式的な自然言語意味論を与えます。

• 中間ロジック
• モデル理論
• 証明（真実）
• 証明技術
• シーケント計算

• J. Avigad および EH Reck (2001)。「『無限の性質の解明』: メタ数学と証明理論の発展」。カーネギーメロン技術レポート CMU-PHIL-120。
• J. Barwise編 (1978)。『数理論理学ハンドブック』ノースホランド。
• S. Buss編 (1998)証明理論ハンドブック。エルゼビア。
• G. ゲンツェン (1935/1969)。 「論理的推理の研究」。 『In ME Szabo』編ゲルハルト・ゲンツェンの論文を集めました。北オランダ。 「Untersuchungen über das logische Schliessen」、 Mathematisches Zeitschrift v. 39、pp. 176–210、405 431より Szabo による翻訳。
• J.-Y. Girard 、P. Taylor、Y. Lafont (1988)。「証明と型」。ケンブリッジ大学出版局。ISBN 0-521-37181-3 
• プラウィッツ、D. (1965)。自然演繹：証明理論的研究。ドーバー出版。ISBN 978-0-486-44655-4。
• SG Simpson (2010)。『2次演算のサブシステム』、第2版。ケンブリッジ大学出版局、ISBN 978-0521150149。 
• AS Troelstraおよび H. Schwichtenberg (1996)。『基本的な証明理論』、Cambridge Tracts in Theoretical Computer Science、Cambridge University Press、ISBN 0-521-77911-1。 
• H. Wang (1981). Popular Lectures on Mathematical Logic、Van Nostrand Reinhold Company、ISBN 0-442-23109-1。 

ウィキメディア・コモンズには、証明理論に関連するメディアがあります。

• 「証明理論」、数学百科事典、EMS Press、2001 [1994]
• J. von Plato (2008)。証明理論の発展。スタンフォード哲学百科事典。