Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

You are looking at an archived page. The website has moved to richardzach.org.

Submitted by Richard Zach on Tue, 10/09/2007 - 6:14am

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 LanguagesLNM 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 ?_{1}^{1}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.

- Richard Zach's blog
- Log in to post comments

- Open Logic Project
- The LogBlog is Moving!
- Academic Genealogy Graphed
- CfP: Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics
- In Memoriam: Grigori Mints
- Previously Unknown Turing Manuscript Going to Auction
- Carnap (and Goodman and Quine) and Linguistics (Guest post by Darin Flynn)
- Carnap on "Syntax" vs "Semantics"