§ Why cut elimination?

§ Cut implies consistency of first order logic (FOL)

§ References