| Cut-elimination |
Website Links For Theorem |
Information AboutCut-elimination |
| CATEGORIES ABOUT CUT-ELIMINATION THEOREM | |
| mathematical theorems | |
| proof theory | |
|
A . However, that the sequent calculus is a fairly expressive framework, and there have been sequent calculi for intuitionistic logic proposed that allow many formulae in the RHS, and from Jean-Yves Girard 's logic LC is it easy to obtain a rather natural formalisation of classical logic where the RHS contains at most one formula; it is the interplay of the logical and structural rules that is the key here. "Cut" is a rule in the normal statement of the Sequent Calculus , and equivalent to a variety of rules in other Proof Theories , which, given : (1) and : (2) allows one to infer : (3) That is, it "cuts" the occurrences of the formula "C" out of the inferential relation. The cut-elimination theorem states that (for a given system) any sequent provable using the rule Cut can be proved without use of this rule. If we think of as a theorem, then cut-elimination simply says that a lemma used to prove this theorem can be inlined. Whenever the theorem's proof mentions lemma , we can substitute the occurrences for the proof of . Consequently, the cut rule is Admissible . For systems formulated in the sequent calculus, Analytic Proof s are those proofs that do not use Cut. Typically such a proof will be longer, of course, and not necessarily trivially so. In his essay "Don't Eliminate Cut!" George Boolos demonstrated that there was a derivation that could be completed in a page using cut, but whose analytic proof could not be completed in the lifespan of the universe. The theorem has many, rich consequences. Once a system is shown to have a cut elimination theorem, it is normally immediate that the system is Consistent . Normally also the system has the Subformula Property , an important property in several approaches to Proof-theoretic Semantics . Cut elimination is one of the most powerful tools for proving Interpolation Theorem s. The possibility of carrying out proof search based on Resolution , the essential insight leading to the Prolog programming language, depends upon the admissibility of Cut in the appropriate system. |
|
|