§ 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 -> Zcould 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 OR. - 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 False! - 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).
§ References