Cut Elimination Theorem
المؤلف:
Gentzen, G
المصدر:
The Collected Papers of Gerhard Gentzen (Ed. M. E. Szabo). Amsterdam, Netherlands: North-Holland, 1969.
الجزء والصفحة:
...
23-1-2022
1227
Cut Elimination Theorem
The cut elimination theorem, also called the "Hauptsatz" (Gentzen 1969), states that every sequent calculus derivation can be transformed into another derivation with the same endsequent (bottom sequent) and in which the cut rule does not occur.
All derivations without cuts posses the sub-formula property that all formulas occurring in a derivation are sub-formulas of the formulas from the endsequent.
A sharpened form of theorem applies to the classical variant of sequent calculus. This form states that any derivation can be transformed to another derivation with the same endsequent and having the following properties.
1. It has no cuts.
2. It contains a so-called midsequent whose derivation contains no 
and 
, and the only inference rules occurring in the derivation below the midsequent are the 
and 
rules and structural rules.
REFERENCES
Gentzen, G. The Collected Papers of Gerhard Gentzen (Ed. M. E. Szabo). Amsterdam, Netherlands: North-Holland, 1969.
Kleene, S. C. Introduction to Metamathematics. Princeton, NJ: Van Nostrand, 1964.
الاكثر قراءة في المنطق
اخر الاخبار
اخبار العتبة العباسية المقدسة
