カット除去定理

混乱を避けるため、ここで「証明」には2つの意味があることに留意してください。1つは、シーケント計算の証明木としての「証明」です。これは数学的対象であり、証明論によって研究される対象です。もう1つは、数学者が通常自然言語で記述する数学的議論としての「証明」です。前者を証明木、後者を証明議論と呼びます。

カット除去定理は証明木に関する定理である。「カット除去定理を証明する」とは、カット除去定理の証明論証を書き出すことを意味する。

カット除去定理の証明は、一般的に次のように行われます。

シーケント計算のすべての推論規則を一覧表示します。証明木とは、各ノードが推論規則の適用を表す木構造のことです。

証明木を抽象言語の式とみなし、書き換え規則を記述する。書き換え規則は次のように定義する。

• 証明木にカットルールが含まれている限り、書き換えルールのいずれかを適用することができます。これを確実にするために、カットルールが出現する可能性のあるあらゆる状況に対して、少なくとも1つの書き換えルールを設計します。
• 書き換え規則は常に木の根を保持します。つまり、同じ後続関係を持つ別の証明木が得られます。

書き換え規則の体系が有限であることを証明すればよい。つまり、いかなる書き換えのシーケンスも有限ステップで終了することを示す必要がある。言い換えれば、書き換え体系が正則であることを示す必要がある。

システムが終了していることを証明するために、通常は順序番号システムを設計します。各証明木について${\displaystyle T}$対応する序数を定義する$\displaystyle o(T)$次に、各書き換えステップが${\displaystyle T\implies T'}$もっている${\displaystyle o(T)>o(T')}$すると、序数が正当に確立されているので、書き換えシステムも正当である。

この考え方は順序分析にもつながる。つまり、システムが終了していることを証明するには、$${\displaystyle \sup _{T{\text{ is a proof tree}}}o(T)}$$整然としている。例えば、ゲンツェンの元の証明の場合、彼は次のことを示した。$${\displaystyle \sup _{T{\text{ is a proof tree}}}o(T)=\epsilon _{0}}$$0 番目のイプシロン数。逆に、ペアノ算術は、より小さい任意の順序数を証明できます。${\displaystyle \epsilon _{0}}$根拠は十分だが、${\displaystyle \epsilon _{0}}$それ自体。したがって、「ペアノ算術の一貫性は、${\displaystyle \epsilon _{0}}$「。

書き換えルールには、一般的に2種類あります。

• 交換法則：カット法則は相互作用なしに1段階上がります。これは、カット式が主式でない場合に発生します。
• 主簡約：カット式が主式であるため、相互作用が発生します。ツリーは新しい枝を伸ばしたり、2つのカットルールを生成したり、新しいセグメントを伸ばしたりする可能性があります。

命題論理LKの典型的なシーケント計算を考えてみましょう。シーケントは有限多重集合である必要があるため、交換規則の煩雑さを無視できます。

カットルールは$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad A,\Pi \vdash \Lambda }{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} .}$$ここでは5つの例を示します。なお、ここでは論理積と論理和の推論規則の「乗法」バージョンを使用しています。これは、カットを排除するのに都合が良いためです。

論理積、左シーケント、交換関係$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad {\frac {A,B,C,\Pi \vdash \Lambda }{A,B\land C,\Pi \vdash \Lambda }}\land _{L}}{\Gamma ,B\land C,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} \quad \implies \quad {\frac {{\frac {\Gamma \vdash \Delta ,A\qquad A,B,C,\Pi \vdash \Lambda }{\Gamma ,B,C,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} }{\Gamma ,B\land C,\Pi \vdash \Delta ,\Lambda }}\land _{L}.}$$カットは単に一歩先に進む${\displaystyle \land _{L}}$相互作用なしに、それは徐々に上昇し、最終的に主要な削減という形で「抵抗」に遭遇するだろう。

選言、左シーケント、交換法$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad {\frac {A,B,\Pi \vdash \Lambda \qquad C,\Sigma \vdash \Theta }{A,B\lor C,\Pi ,\Sigma \vdash \Lambda ,\Theta }}\lor _{L}}{\Gamma ,B\lor C,\Pi ,\Sigma \vdash \Delta ,\Lambda ,\Theta }}\operatorname {Cut} \quad \implies \quad {\frac {{\frac {\Gamma \vdash \Delta ,A\qquad A,B,\Pi \vdash \Lambda }{\Gamma ,B,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} \qquad C,\Sigma \vdash \Theta }{\Gamma ,B\lor C,\Pi ,\Sigma \vdash \Delta ,\Lambda ,\Theta }}\lor _{L}.}$$カットは一段階上に移動し、${\displaystyle \lor _{L}}$。

同一性公理、主要規則$${\displaystyle {\frac {{\overline {A\vdash A}}^{\operatorname {Id} }\qquad A,\Pi \vdash \Lambda }{A,\Pi \vdash \Lambda }}\operatorname {Cut} \quad \implies \quad A,\Pi \vdash \Lambda .}$$このようにして、一部の切り込みは、証明ツリーの葉を相殺することによって、最終的に消滅する可能性がある。

弱化、左続、主規則$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad {\frac {\Pi \vdash \Lambda }{A,\Pi \vdash \Lambda }}\operatorname {Weak} _{L}}{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} \quad \implies \quad {\frac {\Pi \vdash \Lambda }{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Weak} ^{*}.}$$ここ${\displaystyle \operatorname {Weak} ^{*}}$は、左弱化と右弱化の有限個の適用を表します。カット公式${\displaystyle A}$右前提の弱化によって導入されるため、${\displaystyle A}$は使用されていません。左前提は破棄され、元の後件はから復元されます。${\displaystyle \Pi \vdash \Lambda }$弱体化させることによって。

収縮、主要規則$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad {\frac {A,A,\Pi \vdash \Lambda }{A,\Pi \vdash \Lambda }}\operatorname {Contr} _{L}}{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} \quad \implies \quad {\frac {{\frac {\Gamma \vdash \Delta ,A\qquad {\frac {\Gamma \vdash \Delta ,A\qquad A,A,\Pi \vdash \Lambda }{\Gamma ,A,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} }{\Gamma ,\Gamma ,\Pi \vdash \Delta ,\Delta ,\Lambda }}\operatorname {Cut} }{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Contr} ^{*}.}$$ ここ${\displaystyle \operatorname {Contr} ^{*}}$これは、左縮約と右縮約の有限個の適用を表します。右前提の縮約は、カット式の2つの出現箇所を特定しました。${\displaystyle A}$書き換えではまず、${\displaystyle A}$すると、もう一方の発生箇所に対抗してカットします${\displaystyle A}$最後の縮約形は、複製されたコピーを特定します。${\displaystyle \Gamma }$そして${\displaystyle \Delta }$。

ほとんどの書き換え規則は、切り込みを葉に近づけるか、あるいは木の長さが長くなる可能性を犠牲にして切り込みを消去することによって、切り込みを単純に排除していく。唯一の例外は、主規則である縮約の場合である。この場合、1つの切り込みの代わりに2つの切り込みが現れ、木は大幅に大きく成長した。これは依然として終了する書き換え規則であるが、これを証明するには注意が必要である。

本質的に縮約原理規則により、カット除去は証明のサイズを指数関数的に増加させる。カリー・ハワード対応により、カット除去は単純型ラムダ項のベータ縮約に対応する。書き換えはベータ縮約に対応する。縮約規則をまたいだ書き換えは、形式のベータ縮約に対応する。${\displaystyle (\lambda fx.f(fx))t}$、およびベータ還元$${\displaystyle \underbrace {(\lambda fx.f(fx))\cdots (\lambda fx.f(fx))} _{n{\text{ times}}}}$$かかるかもしれない${\displaystyle ^{n}2}$時間、表記はテトレーションです。

量化子規則には同様の主簡約があり、偶発的な捕捉を避けるために、固有変数は書き換え前に必ず名前が変更されるという通常の条件が付いています。たとえば、主カットは${\displaystyle \forall _{R}}$そして${\displaystyle \forall _{L}}$左側の規則で使用されている項を右側の規則からの固有変数証明に代入し、結果として得られるインスタンスでカットすることで簡略化されます。したがって、書き換えステップはエンドセテンシーを保持しつつ、カットを置き換えます。${\displaystyle \forall x\,A(x)}$インスタンスのカットによって${\displaystyle A(t)}$。