Diff for "CutFreeProof"

Differences between revisions 1 and 3 (spanning 2 versions)

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

Given , and we can cut from the proof of when is true. Here we consider to be the lemma in the proof of .

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

-  ⇤ ← Revision 1 as of 2006-08-22 16:28:38 → 
  Size: 512
  Editor: dot
  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:
-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:
-{{{#!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 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 ...)$$.
-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]]