Submitted by Richard Zach on November 11, 2008 - 5:10pm.
Sitting in a talk at CMU by Bill Tait on cut elimnation for predicative systems. His approach, in contrast to Rathjen and Takeuti, is to try to get the cut-elimination proof to be mostly (or even, only) about the proofs, and not about proofs and (mostly) ordinal notation systems. He's using the original Tait calculus, in which formulas are all propositional, but infinitary. His cut-elimination theorem applies in all kinds of cases (essentially up through predicative arithmetic), which I hadn't realized before.