Classic logic papers, pt. 3: Normal derivability in classical logic

One of my favorite proof theory papers of all time:

W. W. Tait. Normal derivability in classical logic. In: Jon Barwise, ed., The Syntax and Semantics of Infinitary Languages LNM 72. (Berlin: SPringer, 1968), pp. 204-236.

Springer actually has this available online–which is neat, but of course only if your institution has access to the collection. Here’s an excerpt from Lopez-Escobar’s Zentralblatt review:

In the first part an elimination theorem (which is a generalization of Gentzen’s Hauptsatz), with ordinal bounds, and an Induction Theorem (which gives a bound on the ordinal of a decidable well-ordering in terms of the length of any cut-free derivation of the principle of induction on that ordering) are obtained for [Tait’s infinitary sequent calculus] L. The second part of the paper consists of applications to some familiar theories, or more specifically applications are given for the: predicate calculus, Peano’s arithmetic, ramified (or constructible) set theory, elementary analysis, hyperarithmetical analysis and systems with the Σ11 axiom of choice.

The “ordinal bounds” mentioned specialize to the familiar super-exponential bound for cut-elimination in the case of predicate logic. I think it’s the first published bound on cut-elimination, although Tait was, I think, inspired by Schütte’s cut-elimination proof for arithmetic. I don’t have his Beweistheorie handy to check and compare, sorry.

Leave a Reply

Your email address will not be published. Required fields are marked *