Differences between revisions 1 and 2
Revision 1 as of 2006-08-22 16:28:38
Size: 512
Editor: dot
Comment:
Revision 2 as of 2007-04-18 16:12:39
Size: 512
Editor: fw
Comment:
Deletions are marked like this. Additions are marked like this.
Line 4: Line 4:
Given $(A\wedge B\wedge ...)\vdash C$, and $C\vdash (D\vee E\vee ...)$ we can cut $C$ from the proof of $(D\vee E\vee ...)$ when $(A\wedge B\wedge ...) $ is true. Here we consider $C$ to be the lemma in the prove of $(D\vee E\vee ...)$. Given $(A\wedge B\wedge ...)\vdash C$, and $C\vdash (D\vee E\vee ...)$ we can cut $C$ from the proof of $(D\vee E\vee ...)$ when $(A\wedge B\wedge ...) $ is true. Here we consider $C$ to be the lemma in the proof of $(D\vee E\vee ...)$.

Essentially, a cut-free proof is a proof that does not use a lemma. That is

Given $(A\wedge B\wedge ...)\vdash C$, and $C\vdash (D\vee E\vee ...)$ we can cut $C$ from the proof of $(D\vee E\vee ...)$ when $(A\wedge B\wedge ...) $ is true. Here we consider $C$ to be the lemma in the proof of $(D\vee E\vee ...)$.

The ability to eliminate $C$ in the above is called the cut-elimination theorem. 

For more information set [http://en.wikipedia.org/wiki/Cut-elimination Cut-elimination]

CutFreeProof (last edited 2020-01-26 23:16:51 by scot)