カット除去定理

カット除去定理（ゲンツェンの主定理）は、シーケント計算の重要性を確立する中心的な結果である。これはもともと、ゲルハルト・ゲンツェンが1934年に発表した画期的な論文「論理的演繹の研究」において、直観主義論理と古典論理をそれぞれ形式化したLJ系とLK系について証明したものである。カット除去定理は、カット規則を用いたシーケント計算の証明を持つ判断は、カットフリー証明、つまりカット規則を用いない証明も持つことを述べている。 ^{[1] [2]}

シークエントは、複数の式を関連付ける論理式で、「」という形式で、 ${\displaystyle A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots }$「${\displaystyle A_{1},A_{2},A_{3},\ldots }$が証明する」と読み、（ゲンツェンによる注釈によると）真理関数「（およびおよび…）ならば（またはまたは…）」と同等であると理解されるべきである。^[3]左側（LHS）は接続詞（and）であり、右側（RHS）は選言（or）であることに注意してください。 ${\displaystyle B_{1},B_{2},B_{3},\ldots }$${\displaystyle A_{1}}$${\displaystyle A_{2}}$${\displaystyle A_{3}}$${\displaystyle B_{1}}$${\displaystyle B_{2}}$${\displaystyle B_{3}}$

LHS には任意の数の式を含めることができます。LHS が空の場合、RHS はトートロジーです。LKでは、RHS にも任意の数の式を含めることができます。RHS に式がない場合は、LHS は矛盾です。一方、LJ では、RHS には 1 つの式のみを含めるか、まったく含めないことができます。ここで、右縮約規則がある場合、RHS に複数の式を含めることは、排中律の許容と同値であることがわかります。ただし、シーケント計算はかなり表現力豊かなフレームワークであり、直観主義論理に対して、RHS に多くの式を含めることを許容するシーケント計算が提案されています。Jean -Yves Girardの論理 LC から、RHS に最大で 1 つの式が含まれる古典論理のかなり自然な形式化を簡単に得ることができます。ここで重要なのは、 論理規則と構造規則の相互作用です。

「カット」はシーケント計算の通常のステートメントにおける推論規則であり、他の証明理論におけるさまざまな規則と同等であり、

1. ${\displaystyle \Gamma \vdash A,\Delta }$

そして

2. ${\displaystyle \Pi ,A\vdash \Lambda }$

推測できる

3. ${\displaystyle \Gamma ,\Pi \vdash \Delta ,\Lambda }$

つまり、推論関係から式の出現を「切り取る」のです。 ${\displaystyle A}$

カット除去定理は、（与えられたシステムに対して）カット規則を使用して証明可能な任意のシーケントは、この規則を使用せずに証明できることを述べています。

右辺に1つの式しかないシーケント計算の場合、「カット」ルールは、

1. ${\displaystyle \Gamma \vdash A}$

そして

2. ${\displaystyle \Pi ,A\vdash B}$

推測できる

3. ${\displaystyle \Gamma ,\Pi \vdash B}$

を定理として考えると、この場合のカット除去は、この定理を証明するために使用される補題をインライン化できることを意味します。定理の証明で補題に言及しているときはいつでも、 の証明の代わりにその出現を代用できます。したがって、カット規則は許容されます。 ${\displaystyle B}$${\displaystyle A}$ ${\displaystyle A}$${\displaystyle A}$

シーケント計算で定式化されたシステムの場合、解析的証明は Cut を使用しない証明です。通常、このような証明は長くなりますが、必ずしも簡単ではありません。ジョージ・ブーロスは、エッセイ「Cut を排除しないで!」 ^[4] で、cut を使用して 1 ページで完了できる導出があるが、その解析的証明は宇宙の寿命では完了できないことを実証しました。

この定理には、多くの豊かな結果が伴います。

• 不合理の証明を認める場合、システムは矛盾しています。システムにカット消去定理がある場合、不合理または空シークエントの証明があれば、カットのない不合理 (または空シークエント) の証明も必要です。通常、そのような証明がないことを確認するのは非常に簡単です。したがって、システムにカット消去定理があることが示されれば、通常、そのシステムが一貫していることはすぐにわかります。
• 通常、このシステムは、少なくとも一階述語論理においては、証明理論的意味論に対するいくつかのアプローチにおいて重要な特性である部分式特性も持ちます。

カット除去は、補間定理を証明するための最も強力なツールの 1 つです。Prolog プログラミング言語につながる重要な洞察である、解決に基づく証明検索を実行できるかどうかは、適切なシステムでカットが許容されるかどうかに依存します。

カリー・ハワード同型性による高階型付きラムダ計算に基づく証明システムの場合、カット除去アルゴリズムは強い正規化特性（すべての証明項が有限数のステップで正規形に簡約される）に対応します。

• 演繹定理
• ゲンツェンのペアノ公理の一貫性証明

• ゲンツェン、ゲルハルト(1935)。 「Untersuchungen über das logische Schließen. I.」。数学的ツァイシュリフト。39 : 176–210。土井：10.1007/BF01201353。
  • Untersuhungen über das logische Schließen I (Archive.org)
  • ゲンツェン、ゲルハルト（1964年） 。「論理的演繹の調査」アメリカ哲学季刊誌。1 （4）：249-287。
• ゲンツェン、ゲルハルト(1935)。 「Untersuchungen über das logische Schließen. II」。数学的ツァイシュリフト。39 : 405–431。土井：10.1007/BF01201363。
  • シュリーセン II の教育 (Archive.org)
  • ゲンツェン、ゲルハルト（1965年）。「論理的演繹の調査」アメリカ哲学季刊誌2 （ 3）：204-218。
• カリー、ハスケル・ブルックス（1977）[1963]。数理論理学の基礎。ニューヨーク：ドーバー出版。ISBN 978-0-486-63462-3。
• クリーネ、スティーブン・コール（2009）[1952]。メタ数学入門。イシ・プレス・インターナショナル。ISBN 978-0-923891-57-2。
• ブーロス、ジョージ（1984年）。「カットを排除しない」。哲学論理ジャーナル。13 （4）：373-378。

• Alex Sakharov。「カット消去定理」。MathWorld。
• ドラガリン、AG (2001) [1994]、「シークエント計算」、数学百科事典、EMS プレス