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. But then I don’t think the original paper actually emphasizes that. The main point in that regard is that when you translate axioms from a theory, you can assign the right kinds of ordinals.
Rick Statman made an interesting point, viz., that it’s also important to verify that the infinitary derivations that you get when you translate derivations into Tait calculus are (primitive) recursively described, and that this is preserved when you eliminate the cuts–if this weren’t the case, you wouldn’t be able to carry out the cut-elimination proof in extensions of PRA.
I have this strange feeling that I have seen this movie before, probably in “Proof Theory and Logical Complexity”, 1987: The ordinals are not that important (with arguments); primitive recursive definability of an omega-proofs/…; cut elimination and subformula property for Pi_1^1 formulas (and for Pi_2^1 in never written/published second volume or papers about p-tykes and dilators); and even more, that the cut-elimination process works even for not well-founded proofs.
I had a question about something from that talk. Tait said that we didn’t need negation because we could do with complementation instead. This just seems to be pushing a conceptual bump around, from negating an inclusion statement to an inclusion in a complement. Was the point there that it simplifies the cut elimination procedure? Something like: we don’t need a separate negation step in the induction since inclusions in complements will be among the atomic sentences that the base case dealt with, or some such?
Shawn, yes that’s the idea. In the classical case, instead of having negation in the language, we can just have negated and unnegated atoms. Then the only rules are for conjunction and disjunction (this includes the quantifiers, since we’re in an infinitary setup). Only one side to the sequents, so you only need to deal with the rules for these two.