## § 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 `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