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.

Zeitschrift für mathematische Logik und Grundlagen der Mathematik

The Zeitschrift für mathematische Logik und Grundlagen der Mathematik was one of the few logic journals around in the mid 20th century. It started publishing in 1955, I think the only logic journals that are older than it are the Journal of Symbolic Logic (1936), the Archiv für mathematische Logik und Grundlagenforschung (1950) and Studia Logica (1953). It didn’t help that it used to be published in the GDR, and so getting copies of old papers from it has always been a minor hassle if you weren’t lucky enough to be near a library with a subscription going back far enough. All the more exciting that I noticed yesterday that Wiley, who owns the successor journal Mathematical Logic Quarterly, is making the complete backset available online. The others are also available back to vol. 1–the JSL through JSTOR, Studia Logica and the Archiv through Springer. Volumes 1-26 of the Archiv are also available free at the GDZ.

I’m not sure if I should count it as a logic journal, but I’d be remiss if I didn’t also note that Fundamenta Mathematicae has been around since 1920, and back issues are available (free) through the Polish Virtual Mathematics Library.

Classic Logic papers, pt. 2: Kruskal’s theorem and Γ0

Looking through my CiteULike database today, I was reminded of this beautiful paper by Gallier, which tells you everything you wanted to know about the ordinal Γ0 and its proof-theoretic relevance. Section 6 is a wonderful overview of the theory of (constructive) countable ordinals.

Jean H. Gallier. What’s so special about Kruskal’s theorem and the ordinal Γo? A survey of some results in proof theory. Annals of Pure and Applied Logic 53 (1991) 199-260.

This paper consists primarily of a survey of results of Harvey Friedman about some proof-theoretic aspects of various forms of Kruskal’s tree theorem, and in particular the connection with the ordinal Γ0. We also include a fairly extensive treatment of normal functions on the countable ordinals, and we give a glimpse of Veblen hierarchies, some subsystems of second-order logic, slow-growing and fast-growing hierarchies including Girard’s result, and Goodstein sequences. The central theme of this paper is a powerful theorem due to Kruskal, the ‘tree theorem’, as well as a ‘finite miniaturization’ of Kruskal’s theorem due to Harvey Friedman. These versions of Kruskal’s theorem are remarkable from a proof-theoretic point of view because they are not provable in relatively strong logical systems. They are examples of so-called ‘natural independence phenomena’, which are considered by most logicians as more natural than the metamathematical incompleteness results first discovered by Gödel. Kruskal’s tree theorem also plays a fundamental role in computer science, because it is one of the main tools for showing that certain orderings on trees are well founded. These orderings play a crucial role in proving the termination of systems of rewrite rules and the correctness of Knuth-Bendix completion procedures. There is also a close connection between a certain infinite countable ordinal called Γo and Kruskal’s theorem. Previous definitions of the function involved in this connection are known to be incorrect, in that, the function is not monotonic. We offer a repaired definition of this function, and explore briefly the consequences of its existence.

Ackermann Award announced

The Ackermann Award is the EACSL‘s award for outstanding dissertations in logic in computer science. This year’s award is shared by

  • Dietmar Berwanger
    RWTH Aachen (Advisor: Erich Graedel)
    Thesis: Games and Logical Expressiveness
  • Stéphane Lengrand
    Université de Paris VII and University of St. Andrews (Advisors: Delia Kesner and Roy Dyckhoff)
    Thesis: Normalization and Equivalence in Proof Theory and Type Theory
  • Ting Zhang
    Stanford University (Advisor: Zohar Manna)
    Thesis: Arithmetic Integration of Decision Procedures

Congratulations to the winners!

The EACSL is now soliciting nominations for the 2008 award. Eligible for the 2008 Ackermann Award are PhD dissertations in topics specified by the EACSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1.1.2006 and 31.12. 2007. The deadline for submission is 15.3.2008. Submission details are here.