Abstracts.2020.Hauptsatz

Dag Prawitz's proof of Takeuti's conjecture

by Tjeerd Fokkens

Abstract

In 1953 Gaisi Takeuti stated, in analogy with Gentzen’s Hauptsatz for first order logic, his bold conjecture which is also known as the Hauptsatz for Simple Type Theory (STT). The statement says that the cut-rule in STT’s sequent calculus is admissible. Independently of each other, Moto-o Takahashi and Dag Prawitz proved the conjecture 14 years later. Using results from Schütte, we’re going through Prawitz’s proof in detail, trying to understand the main challenges and how they are overcome.

Resources

• Slides

References

1. Gaisi Takeuti. 1953. On a Generalized Logic Calculus.
2. Kurt Schütte. 1960. Syntactical and Semantical Properties of Simple Type Theory.
3. Moto-o Takahashi. 1967. A Proof of Cut-Elimination Theorem in Simple Type-Theory [sic].
4. Dag Prawitz. 1968. Hauptsatz for Higher Order Logic.

Bibliography

1. Alonzo Church. 1940. A Formulation of the Simple Theory of Types.
2. J. Lambek and P. J. Scott. 1986. Introduction to Higher Order Categorical Logic. Note: Presents a Gentzen-style proof system for (intuitionistic) STT (with comprehension instead of λ-abstraction).
3. J. Roger Hindley. 1997. Basic Simple Type Theory.
4. William M. Farmer. 2008. The Seven Virtues of Simple Type Theory. Note: Presents a Hilbert-style proof system for (classical) STT (with λ-abstraction instead of comprehension).
5. Philip Johnson-Freyd. 2014. Second-Order Classical Sequent Calculus.
6. Thierry Coquand. 2006–2018. Type Theory in The Stanford Encyclopedia of Philosophy.
7. Anupam Das and Thomas Powell. 2018. The Sequent Calculus and Cut-Elimination. Note: Lecture 4 of Introduction to Proof Theory.
8. Christoph Benzmüller and Peter Andrews. 2006–2019. Church’s Type Theory in The Stanford Encyclopedia of Philosophy.