## § 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".

#### § 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).