Loading article…
証明論は、数理論理学および理論計算機科学の主要な分野[ 1 ]であり、証明は形式的な数学的対象として扱われ、数学的手法による分析が容易になります。証明は通常、リスト、ボックスリスト、ツリーなどの帰納的に定義されたデータ構造として表現され、これらは与えられた論理体系の公理と推論規則に従って構築されます。したがって、証明論は構文的な性質を持ち、意味論的な性質を持つモデル理論とは対照的です。
証明論の主要な分野には、構造証明論、順序分析、証明可能性論理、証明論的意味論、逆数学、証明マイニング、自動定理証明、証明複雑性などがある。また、コンピュータ科学、言語学、哲学への応用にも多くの研究が集中している。
論理の形式化はゴットロープ・フレーゲ、ジュゼッペ・ペアノ、バートランド・ラッセル、リヒャルト・デデキントといった人物の業績によって大きく進展したが、現代の証明論の歴史は、しばしばデイヴィッド・ヒルベルトによって確立されたと見なされている。ヒルベルトは『数学の基礎』の中で、いわゆるヒルベルト・プログラムを開始した。このプログラムの中心的な考えは、数学者が必要とするすべての高度な形式理論に対して、有限な無矛盾性の証明を与えることができれば、メタ数学的議論によってこれらの理論の基礎付けが可能になるというものであった。メタ数学的議論は、それらの純粋に普遍的な主張（より専門的には証明可能な）すべてが、文は有限的に真である。いったんそのように根拠づけられると、我々はそれらの存在定理の非有限的な意味を気にせず、それらを理想的な実体の存在に関する擬似的な意味を持つ規定とみなす。
このプログラムの失敗は、クルト・ゲーデルの不完全性定理によって実証された。この定理は、ある種の単純な算術的真理を表現するのに十分強いω-無矛盾理論は、自身の無矛盾性を証明できないことを示した。ゲーデルの定式化によれば、 しかし、ヒルベルトのプログラムの改良版が登場し、関連テーマに関する研究が行われてきた。これにより、特に以下のような成果が得られた。
ヒルベルトのプログラムの盛衰と並行して、構造的証明論の基礎が築かれつつあった。ヤン・ウカシェヴィチは 1926年に、論理の推論規則における仮定から結論を導き出すことを許容すれば、ヒルベルトの体系を論理の公理的表現の基礎として改良できると提案した。これに対し、スタニスワフ・ヤシュコフスキ（1929年）とゲルハルト・ゲンツェン（1934年）はそれぞれ独立に、自然演繹計算と呼ばれる体系を提供した。ゲンツェンのアプローチでは、導入規則で表現される命題を主張する根拠と、排除規則で命題を受け入れる結果との間の対称性という考え方が導入され、これは証明論において非常に重要な考え方であることが証明されている。[ 2 ] ゲンツェン (1934) は、論理結合子の双対性をよりよく表現する同様の精神で発展した計算体系であるシーケント計算の概念をさらに導入し、 [ 3 ]直観主義論理の形式化において根本的な進歩を遂げ、ペアノ算術の無矛盾性の最初の組み合わせ論的証明を提供しました。自然演繹とシーケント計算の提示は、証明論に解析的証明の根本的な概念を導入しました。
構造証明論は、証明計算の具体的な内容を研究する証明論の一分野である。最もよく知られている証明計算のスタイルは次の3つである。
これらの手法はそれぞれ、古典的または直観主義的な命題論理や述語論理、ほぼすべての様相論理、そして関連性論理や線形論理といった多くの部分構造論理を、完全かつ公理的に形式化することができる。実際、これらの計算体系のいずれかで表現できない論理は稀である。
証明論者は一般的に、特定の優れた性質を持つ証明計算に関心を持つ。優れた性質の一つに解析性がある。解析的証明の概念はゲンツェンによってシーケント計算に導入され、彼は古典論理と直観主義論理のシーケント計算がカットフリーであることを証明した。
解析性の概念の一つに、カット除去性質がある。証明計算体系は、カット規則を持つ場合にカット除去性質を持つが、証明可能なシーケントはカット規則がなくても証明可能である。ゲンツェンの中間シーケント定理、クレイグの補間定理、およびヘルブランドの定理は、カット除去性質の系として導かれる。
分析性のもう一つの概念は部分式性質。証明は、そのすべての式が後件の部分式である場合に部分式性質を持つ。証明計算は、その証明可能なすべての後件が部分式性質を持つ証明によって証明できる場合に部分式性質を持つ。ほとんどの証明計算では、部分式性質はカット除去性質から導かれるが、必ずしもその逆で。部分式性質を持つ証明計算は無矛盾。なぜなら、空の後件が導出可能であれば、それは何らかの前提の部分式でなければならないが、そうではないからである。
ダグ・プラヴィッツが示したように、ゲンツェンの自然演繹計算も解析的証明の概念を支持している。その定義はやや複雑で、解析的証明は正規形であり、項書き換えにおける正規形の概念と関連している。ジャン＝イヴ・ジラールの証明ネットのような、より特殊な証明計算も解析的証明の概念を支持している。
還元論理で生じる分析的証明の特定の一族は、目標指向型証明探索手続きの大きな一族を特徴づける焦点型証明である。証明体系を焦点型形式に変換できる能力は、カットの許容性が証明体系の構文的一貫性を示すのと同様に、その構文的品質の良い指標となる。[ 4 ]
調和という概念がある。自然演繹体系では、各論理結合子には導入規則と除去規則という一対の規則がある。この一対の規則は、証明を正規化することで最大式を除去できる場合、調和していると言われる。最大式とは、導入された後、除去される式のことである。このような最大式は補題と同様の働きをし、証明を簡潔に記述できるものの、必ずしも必要ではない。正規化された証明では、論理結合子を導入するだけで、除去してはならない。
特定の推論規則は局所的であり、これは望ましい特性である。[ 5 ]例えば、線形論理 の!規則を考えてみよう。 !-ルールが特定のシーケント計算ステップに正しく適用されていることを確認するために確認する必要があるのはそれだけではないだが、各最外の論理結合子として「!」を持つ 。この意味で、この規則は局所的ではない。なぜなら、この規則を適用するには、無数の式をチェックする必要があるからである。
構造証明論は、自然演繹計算における正規化の過程と型付きラムダ計算におけるベータ還元との間に構造的な類似性があることを指摘するカリー＝ハワード対応によって型理論と結び付けられています。これは、ペル・マルティン＝レーフによって開発された直観主義型理論の基礎となっており、しばしば3方向対応へと拡張され、その3番目の要素はデカルト閉圏です。
構造理論におけるその他の研究テーマには、構造証明理論の解析的証明の中心的な考え方を応用して、幅広い論理体系に対する決定手続きや半決定手続きを提供する解析タブローや、部分構造論理の証明理論などがある。
順序数解析は、算術、解析学、集合論のサブシステムに対する組み合わせ論的無矛盾性証明を提供する強力な手法です。ゲーデルの第二不完全性定理は、十分な強さを持つ理論に対して有限的無矛盾性証明が不可能であることを示していると解釈されることがよくあります。順序数解析によって、理論の無矛盾性の無限の内容を正確に測定することができます。無矛盾な再帰的に公理化された理論 T に対して、有限的算術では、ある超限順序数の整礎性が T の無矛盾性を意味することを証明できます。ゲーデルの第二不完全性定理は、そのような順序数の整礎性が理論 T では証明できないことを意味します。
順序分析の結果には、(1)古典的な2階算術と集合論のサブシステムの構成理論に対する一貫性、(2)組み合わせ的独立性の結果、(3)証明可能な全再帰関数と証明可能な整礎順序数の分類が含まれます。
順序分析は、ゲンツェンによって始められ、彼は順序数 ε 0までの超限帰納法を用いてペアノ算術の無矛盾性を証明した。順序分析は、一階および二階算術と集合論の多くの断片に拡張されてきた。大きな課題の一つは、非述語的理論の順序分析である。この方向における最初のブレークスルーは、竹内が順序図法を用いてΠ 1 1 -CA 0の無矛盾性を証明したことである。
証明可能性論理は様相論理であり、ボックス演算子は「～であることが証明可能である」と解釈されます。重要なのは、十分に豊かな形式理論の証明述語の概念を捉えることです。ペアノ算術における証明可能性を捉える証明可能性論理GL（ゲーデル＝レーブ）の基本公理として、ヒルベルト＝ベルネイスの導出可能性条件とレーブの定理（Aの証明可能性がAを意味することが証明可能であれば、Aは証明可能である）の様相類似物を採用します。
ペアノ算術の不完全性および関連理論に関する基本的な結果のいくつかは、証明可能性論理に類似するものが存在する。例えば、GLには、矛盾が証明できない場合、矛盾が証明できないことも証明できないという定理がある（ゲーデルの第二不完全性定理）。また、不動点定理の様相論理における類似物も存在する。ロバート・ソロヴェイは、様相論理GLがペアノ算術に関して完全であることを証明した。つまり、ペアノ算術における証明可能性の命題理論は、様相論理GLによって完全に表現される。これは、ペアノ算術における証明可能性に関する命題推論が完全かつ決定可能であることを直接的に意味する。
証明可能性論理に関するその他の研究では、一階述語論理、多様体証明可能性論理（一方の様相が対象理論における証明可能性を表し、もう一方の様相がメタ理論における証明可能性を表す）、および証明可能性と解釈可能性の相互作用を捉えることを目的とした解釈可能性論理に焦点が当てられてきた。ごく最近の研究では、段階付き証明可能性代数を算術理論の順序分析に応用する試みも行われている。
逆数学は、数学の定理を証明するために必要な公理を特定しようとする数理論理学のプログラムである。 [ 6 ]この分野はハーヴェイ・フリードマンによって創設された。その定義方法は、公理から定理を導出するという通常の数学的手法とは対照的に、「定理から公理へ逆向きに進む」と表現できる。逆数学プログラムは、ZF集合論において選択公理とツォルンの補題が同値であるという古典的な定理など、集合論における結果によって予見されていた。しかし、逆数学の目標は、集合論の公理ではなく、通常の数学の定理の公理を研究することである。
逆算数学では、まず枠組みとなる言語と基本理論（中核となる公理系）から始めます。この枠組みと基本理論は、関心のある定理のほとんどを証明するには不十分ですが、これらの定理を述べるために必要な定義を展開するには十分な力を持っています。例えば、「すべての有界な実数列は上限を持つ」という定理を研究するには、実数と実数列について論じることができる基本体系を用いる必要があります。
基本システムで記述できるが基本システムでは証明できない定理ごとに、その定理を証明するために必要な特定の公理系（基本システムよりも強い）を決定することが目標です。定理Tを証明するためにシステムS が必要であることを示すには、2 つの証明が必要です。最初の証明は、TがSから証明可能であることを示します。これは、システムSで実行できるという正当化を伴う通常の数学的証明です。2 番目の証明は、反転として知られており、 T自体がS を意味することを示します。この証明は基本システムで実行されます。反転により、基本システムを拡張する公理系S ′は、 Tを証明しながらSよりも弱くなることはないことが確立されます。
逆算数学における注目すべき現象の一つは、ビッグファイブ公理系の堅牢性である。強度の順に、これらの系は頭字語で RCA 0、 WKL 0、 ACA 0、 ATR 0、および Π 1 1 -CA 0と名付けられている。逆算的に解析された通常の数学の定理はほぼすべて、これら 5 つの系のいずれかと同等であることが証明されている。最近の研究の多くは、RT 2 2 (ペアに関するラムゼイの定理)のように、この枠組みにうまく収まらない組み合わせ原理に焦点を当てている。
逆数学の研究では、再帰理論や証明論の手法や技術がしばしば取り入れられる。
関数的解釈とは、非構成的理論を関数的理論に解釈する手法である。関数的解釈は通常、2段階で進められる。まず、古典的理論Cを直観主義的理論Iに「還元」する。つまり、Cの定理をIの定理に変換する構成的写像を与える。次に、直観主義的理論Iを量化子を含まない関数の理論Fに還元する。これらの解釈は、構成的理論に対する古典的理論の一貫性を証明するため、ヒルベルトのプログラムの一形態に貢献する。関数的解釈の成功例は、無限理論を有限理論に、非述語的理論を述語的理論に還元することである。
関数解釈は、縮小理論における証明から構成的な情報を抽出する手段も提供する。解釈の直接的な結果として、通常、I または C のいずれかでその全体が証明できる再帰関数は、F の項で表されるという結果が得られる。I において F の追加的な解釈を与えることができれば（これは時として可能である）、この特徴付けは実際には通常、正確であることが示される。多くの場合、F の項は、原始再帰関数や多項式時間で計算可能な関数など、自然な関数クラスと一致することが判明する。関数解釈は、理論の順序分析を行い、証明可能な再帰関数を分類するためにも用いられてきた。
関数解釈の研究は、クルト・ゲーデルによる有限型関数の量化子を用いない理論における直観主義算術の解釈から始まった。この解釈は一般に「弁証法解釈」として知られている。直観主義論理における古典論理の二重否定解釈と併せて、古典算術を直観主義算術に還元するものである。
日常的な数学実践における非公式な証明は、証明論における形式的な証明とは異なります。それらはむしろ、十分な時間と忍耐があれば、専門家が少なくとも原理的には形式的な証明を再構築できるような、高度な概略図のようなものです。ほとんどの数学者にとって、完全な形式的な証明を書くことは、あまりにも衒学的で冗長であるため、一般的には用いられていません。
形式的な証明は、対話型定理証明においてコンピュータの助けを借りて構築されます。重要なのは、これらの証明はコンピュータによって自動的に検証できる点です。形式的な証明の検証は通常簡単ですが、証明を見つけること（自動定理証明）は一般的に困難です。一方、数学文献における非形式的な証明は、検証に数週間の査読を要し、それでもなお誤りが含まれている可能性があります。
言語学では、型論理文法、範疇文法、モンタギュー文法は、構造証明理論に基づく形式体系を適用して、形式的な自然言語意味論を与える。
