構造証明論

数理論理学において、構造証明理論は、意味論的性質が明らかにされる一種の証明である解析的証明の概念をサポートする証明計算を研究する証明理論の下位分野である。証明計算で形式化された論理のすべての定理が解析的証明を持つ場合、証明計算は、一貫性などのことを実証したり、決定手続きを提供したり、定理の対応物として数学的または計算的証拠を抽出したりするために使用できる。これは、モデル理論によく与えられる種類のタスクである。^{[ 1 ]}

解析的証明の概念は、ゲルハルト・ゲンツェンがシーケント計算のために証明論に導入したもので、解析的証明とはカットフリーの証明のことである。彼の自然演繹計算も解析的証明の概念を支持しており、ダグ・プラヴィッツが示したように、その定義はやや複雑で、解析的証明は正規形であり、項書き換えにおける正規形の概念と関連している。

構造証明理論における「構造」という用語は、シーケント計算で導入された技術的な概念に由来する。シーケント計算は、構造演算子と呼ばれる特別な非論理演算子を用いて、推論のどの段階でも主張を表す。${\displaystyle A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}}$ターンスタイルの左側のコンマは通常論理積として解釈される演算子であり、右側のコンマは論理和として解釈されますが、ターンスタイルの記号自体は含意として解釈されます。ただし、これらの演算子と、シーケント計算でそれらが解釈される論理結合子との間には、動作に根本的な違いがあることに注意することが重要です。構造演算子は計算のすべての規則で使用され、部分式の性質が適用されるかどうかを問うときには考慮されません。さらに、論理規則は一方向のみです。論理構造は論理規則によって導入され、一度作成されると削除することはできませんが、構造演算子は導出の過程で導入および削除できます。

シーケントの構文的特徴を特別な非論理演算子として捉えるという考え方は古くはなく、証明論の革新によってもたらされたものです。構造演算子がゲッツェンのオリジナルのシーケント計算のように単純な場合は、それらを分析する必要はほとんどありませんが、ディスプレイ論理（ 1982年にヌエル・ベルナップによって導入） ^{[ 2 ]}のような深層推論の証明計算は、論理結合子と同じくらい複雑な構造演算子をサポートしており、高度な処理を必要とします。

カット除去定理（主定理）は、シーケント計算における重要な結果である。この定理は、カット規則を用いて導出可能なシーケントは、カット規則を用いなくても導出できることを述べている。モーダス・ポネンスの論理原理を一般化したカット規則は、次のように定式化される。

${\displaystyle {\frac {\Gamma \vdash \Delta ,A\quad A,\Pi \vdash \Sigma }{\Gamma ,\Pi \vdash \Delta ,\Sigma }}\quad ({\text{カット}}),}$

どこ、${\displaystyle \ガンマ ,\デルタ ,\パイ ,}$そして${\displaystyle \Sigma }$は数式のシーケンスです。カット式${\displaystyle A}$これは、導入されてから削除される中間補題として効果的に使用されます。この規則を削除することの意義は、結果として得られるカットフリー証明が部分式特性を持つことであり、これにより、カットフリー導出のどこかに現れるすべての式が、最終的な結論シーケントの式の部分式であることが保証されます。したがって、証明は、証明対象の命題に既に存在する概念以外に外部概念を導入する必要がないため、完全に解析的です。このカット特性は、古典論理と直観主義論理の一貫性を示すために使用され、証明論的意味論で使用されます。

自然演繹は、直観的な人間の推論を忠実に反映した推論規則に基づいて前提から論理的結論を導き出す形式体系である。論理と計算の直接的なつながりは、直観主義論理の式と型付きラムダ計算の型との間に直接的な同型性を確立するカリー・ハワード対応によって実現される。この対応において、すべての命題は型と見なすことができ、その命題の証明は対応する型のプログラムに類似する。本質的に、証明とは型の存在を示す構成である。例えば、含意の証明は、${\displaystyle A\to B}$型の項を受け取る関数に対応します${\displaystyle A}$入力として、型の項を生成します${\displaystyle B}$出力として。同様に、論理積の証明${\displaystyle A\land B}$（製品タイプ）は、タイプの項を含むペアに対応します。${\displaystyle A}$およびタイプの用語${\displaystyle B}$この関係は単なる表面的なものではありません。証明を簡略化するために冗長な論理ステップを削除する証明正規化のプロセスは、型付きラムダ計算におけるプログラム実行プロセス、すなわちベータ還元に直接対応しています。この同型性は、論理証明の計算内容、現代の型理論を結びつけ、証明支援システムの設計を導きます。以下の図はこの対応関係を示しています。

論理的双対性と調和は、シーケント計算の対称性によって結び付けられています。シーケントのアーキテクチャは、${\displaystyle \Gamma \vdash \Delta }$、 どこ${\displaystyle \ガンマ ,\デルタ }$これらは式の有限多重集合であり、前件（左）と後件（右）の間に基本的な双対性を確立します。この双対性は、各論理結合子の左および右導入規則によって明示的に実現されます。たとえば、連言（${\displaystyle \land }$）と選言（${\displaystyle \lor }$）は双対です。

${\displaystyle {\begin{array}{ccc}{\text{(}}{\land }{\text{L)}}&{\dfrac {A,B,\Gamma \vdash \Delta }{A\land B,\Gamma \vdash \Delta }}&{\text{(}}{\land }{\text{R)}}&{\dfrac {\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}{\Gamma \vdash \Delta ,A\land B}}\\\\{\text{(}}{\lor }{\text{L)}}&{\dfrac {A,\Gamma \vdash \Delta \qquad B,\Gamma \vdash \Delta }{A\lor B,\Gamma \vdash \Delta }}&{\text{(}}{\lor }{\text{R)}}&{\dfrac {\Gamma \vdash \Delta ,A,B}{\Gamma \vdash \Delta ,A\lor B}}\end{array}}}$

この左右対称性は、反転原理によって導入規則のみによって定義される接続詞の統語的意味と、その消去動作との間のより深い調和を反映している。カット消去定理はこのメタ理論的調和を保証する。カット規則は、 ${\displaystyle {\text{(カット)}}\quad {\dfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Lambda }{\Gamma ,\Sigma \vdash \Delta ,\Lambda }},}$ これは意味的結合の一形態を表しており、その許容性は証明システムが内部的に一貫性があり解析的であることを示している。つまり、証明は、例えば式などの外部概念を参照する必要がない。${\displaystyle A}$結論には含まれていないもの。複雑な式のカットをその部分式のカットにうまく還元することは、左ルールと右ルールの間のキーケース還元を介して、例えば、カットを還元することによって実現されます。${\displaystyle A\land B}$両方によって導入されました (${\displaystyle \land }$R) および (${\displaystyle \land }$L)は、結合子の導入可能性と削除可能性の完璧なバランスを計算によって表現したものです。したがって、カット削除は演算規則が調和していることを検証し、論理体系が一貫性を持ち、その証明が優れた正規化特性を持つことを保証します。

特定の推論規則は局所的であり、これは望ましい特性である。^{[ 3 ]}例えば、線形論理 の!規則を考えてみよう。$${\displaystyle {\frac {\vdash A,?B_{1},\dots ,?B_{n}}{\vdash !A,?B_{1},\dots ,?B_{n}}}}$$ !-ルールが特定のシーケント計算ステップに正しく適用されていることを確認するために${\displaystyle {\frac {\vdash A,B_{1},\dots ,B_{n}}{\vdash A',B_{1},\dots ,B_{n}}}}$確認する必要があるのはそれだけではない${\displaystyle A'=?A}$だが、各${\displaystyle B_{i}}$ 最外の論理結合子として !を持つ。この意味で、この規則は局所的ではない。なぜなら、この規則を適用するには、無数の式をチェックする必要があるからである。

より身近な例として、古典的なシーケント計算LKでは、ORの推論規則は次のようになります。$${\displaystyle {\frac {A,\Gamma \vdash \Delta \quad B,\Gamma \vdash \Delta }{A\lor B,\Gamma \vdash \Delta }}(\lor \vdash ),\quad {\frac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}(\vdash \lor _{1}),\quad {\frac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}(\vdash \lor _{2})}$$ルール${\displaystyle \lor \vdash }$ローカルではない。ステップで正しく適用されたことを確認するため$${\displaystyle {\frac {A,\Gamma \vdash \Delta \quad B,\Gamma '\vdash \Delta '}{C,\Gamma \vdash \Delta }}}$$それだけでなく、${\displaystyle C=A\lor B}$しかし、${\displaystyle \Gamma =\Gamma ',\Delta =\Delta '}$ルール${\displaystyle \vdash \lor _{1},\vdash \lor _{2}}$ローカルです。^{[ 4 ]}

局所性はもともと並列論理プログラミングの考察から着想を得たものである。その考え方は以下の通りである。大きなシーケント${\displaystyle \Gamma \vdash \Delta }$データは、複数のプロセッサと複数のメモリ位置に分散して格納される場合があります。ローカル推論ステップは限られた量の相互作用で実行できますが、非ローカル推論ステップは任意の量の相互作用で実行できます。たとえば、具体的には、${\displaystyle {\frac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}}$プロセッサは新しいシーケンシャルを生成する必要がある${\displaystyle \Gamma '\vdash \Delta '}$、したがって${\displaystyle \Gamma '}$単に同じメモリ アドレスを指しているだけです${\displaystyle \Gamma }$、 そして${\displaystyle \Delta '}$を指摘する${\displaystyle A\lor B}$続いて、2 番目のメモリ アドレス${\displaystyle B,\Delta }$対照的に、ルールを適用する${\displaystyle \lor \vdash }$2 つのシーケントが同一であることを確認する必要があり、${\displaystyle O(n)}$オペレーションでは、${\displaystyle n}$は、シーケント内の数式の数です。

ハイパーシーケントフレームワークは、通常のシーケント構造をシーケントの多重集合に拡張し、異なるシーケントを区切るために追加の構造結合子 | (ハイパーシーケントバーと呼ばれる) を使用します。これは、例えば、様相論理、中間論理、部分構造論理の解析計算を提供するために使用されてきました^{[ 5 ] [ 6 ] [ 7 ]}ハイパーシーケントは構造です

${\displaystyle \Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}$

それぞれ$\displaystyle \Gamma _{i}\vdash \Delta _{i}}$は、ハイパーシーケントの構成要素と呼ばれる通常のシーケントです。シーケントと同様に、ハイパーシーケントは集合、多重集合、またはシーケンスに基づいて構築でき、構成要素は単一結論シーケントまたは多重結論シーケントになります。ハイパーシーケントの式の解釈は、検討対象の論理に依存しますが、ほぼ常に何らかの形式の選言です。最も一般的な解釈は、単純な選言として解釈することです。

${\displaystyle (\bigwedge \Gamma _{1}\rightarrow \bigvee \Delta _{1})\lor \dots \lor (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

中間論理の場合、またはボックスの選言として

${\displaystyle \Box (\bigwedge \Gamma _{1}\rightarrow \bigvee \Delta _{1})\lor \dots \lor \Box (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

様相論理の場合。

ハイパーシーケントバーの選言的解釈に沿って、本質的にすべてのハイパーシーケント計算には外部構造規則、特に外部弱化規則が含まれる。

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma \vdash \Pi }}}$

そして外部収縮規則

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}}}$

ハイパーシーケントフレームワークの表現力は、ハイパーシーケント構造を操作するルールによって向上します。重要な例として、様相分割ルール^{[ 6 ]が挙げられます。}

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma ,\Omega \vdash \Box \Pi ,\Theta }{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma \vdash \Box \Pi \mid \Omega \vdash \Theta }}}$

様相論理S5の場合、${\displaystyle \Box \Sigma }$つまり、${\displaystyle \Box \Sigma }$形式は${\displaystyle \Box A}$。

別の例として、中間論理LCの通信規則^{[ 6 ]}が挙げられる。

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Omega \vdash A\qquad \Sigma _{1}\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m}\mid \Theta \vdash B}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma _{1}\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m}\mid \Omega \vdash B\mid \Theta \vdash A}}}$

通信ルールにおける構成要素は、単一結論のシーケントであることに注意してください。

入れ子構造シーケント計算は、構造の2面計算に似た形式化である。

• サラ・ネグリ、ヤン・フォン・プラトー（2001）。構造証明論。ケンブリッジ大学出版局。ISBN 978-0-521-79307-0。
• アン・シャープ・トロエルストラ;ヘルムート・シュヴィヒテンベルク(2000)。基本的な証明理論(第 2 版)。ケンブリッジ大学出版局。ISBN 978-0-521-77911-1。