If you’ve wondered what all this “cut elimination” business is about, here’s a nice blog entry (on That Logic Blog) which gives a nice introduction. Jon points out that proofs with cut have (at least–depends on the logic) exponential speedup over proofs with cut. This result is due to Statman and Orevkov. Jon points to a really good piece by Alessandra Carbone. She has done really excellent work on proof complexity; y’all should check it out. An interesting investigation of the complexity of cut-elimination (in classical first-order logic) is in “Cut normal forms and proof complexity“, Annals of Pure and Applied Logic 97, by Matthias Baaz and Alexander Leitsch. See also Boolos’s “Don’t eliminate Cut”, Journal of Philosophical Logic 13 (1984) 373-378 (reprinted in Logic, Logic, and Logic). An interesting and underexamined topic is the reverse of cut-elimination: how do you actually make proofs shorter by introducing cuts? Matthias and I have an old paper on that (which I should convert to PDF…). By the way, the deadline for the Studia Logica special issue on cut elimination is fast approaching!