カット除去定理

ウィキペディア

カット除去定理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/09/27 05:55 UTC 版)

カット除去定理（カットじょきょていり、英: Cut-elimination theorem）は、シークエント計算の手法の重要性を示す、数理論理学の主要な結果のひとつである。（数理論理学の）基本定理と呼ぶこともある。ゲルハルト・ゲンツェンが1934年に書いた記念碑的論文 "Investigations into Logical Deduction" で、古典論理と直観論理の体系をそれぞれ形式化したシークエント計算の形式的体系 LK 及び LJ において、最初に証明が与えられた。カット除去定理は、シークエント計算の推論規則であるカット規則を用いて証明可能な式には、カット規則を用いない証明図もまた必ず存在することを示したものである。

シークエント

シークエントは複数の文からなる論理表現であり、

$A,B,C,\ldots \vdash P,Q,R,\ldots$

この項目は、数理論理学に関連した書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています。

• 表示
• 編集