Differences between revisions 2 and 3
⇤ ← Revision 2 as of 2007-04-18 16:12:39 →
Size: 512
Editor: fw
Comment:
← Revision 3 as of 2020-01-26 23:16:51 → ⇥
Size: 511
Editor: scot
Comment:
Deletions are marked like this. Additions are marked like this.
Line 1: Line 1:
Essentially, a cut-free proof is a proof that does not use a lemma. That is  Essentially, a cut-free proof is a proof that does not use a lemma. That is:
Line 3: Line 3:
{{{#!latex2
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 ...)$.		 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 ...)$$.
Line 6: Line 5:
The ability to eliminate $C$ in the above is called the cut-elimination theorem.
}}}		 The ability to eliminate $$C$$ in the above is called the cut-elimination theorem.
Line 9: Line 7:
For more information set [http://en.wikipedia.org/wiki/Cut-elimination Cut-elimination] For more information set [[http://en.wikipedia.org/wiki/Cut-elimination Cut-elimination]]

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)