§ Why cut elimination?
- Morally spekaing, gives control over the formulae that occur in a proof.
- If we can conclude that
(X -> Y; Y -> Z)|(X -> Z), then the proof of
X -> Z could be arbitrarily complex, since
Y might be something crazy.
- If we have
cut, we know that such arbitrarily crazy things cannot happen, as the
cut rule is the only rule where we are forced to synthesize something "out of thin air".
- Example of use of cut
§ Cut implies consistency of first order logic (FOL)
- suppose we have cut for FOL
- If FOL is inconsistent, then there would be a proof of
False starting from no premises.
- To be more formal, one could write
|- False or
True |- False.
- Written in terms of sequent calculus, this would be
 |-  (recall that the LHS is interpreted with
AND, RHS with
- But by cut, this would mean that the proof of
 |-  would involve only the the symbols in
Sym() U () which is the empty set!
- Since there is no trivial proof of
False with zero symbols, and all other derivation rules need symbols, there cannot be a proof of
- To repeat: a proof of
True |- False or
 |-  could be
cut-eliminated so it is forced to contain only the sumbols in
Sym() U Sym() = EMPTYSET. This is absurd, and thus there is no proof of
True |- False, which implies that the theory is consistent (assuming soundness).