Embed Notice

Is there something like a framework for cut elimination?

As far as I know, to design a system that admits cut you need (1) deep intuition, and (2) to write some of the worst proofs ever conceived

Is there some kind of metatheory for designing proof systems that have "cut elimination by construction"?