The eminent proof theorist and philosopher of mathematics William Walker (“Bill”) Tait died March 15, 2024 in Chicago. He was 95.

Bill was born on January 22, 1929, in Freeport, NY, and received a BA from Lehigh University in 1952 where he was taught by Adolph Grünbaum. He undertook graduate studies in philosophy (1952–54) and mathematics (1955–58) at Yale University, and spent the 1954/55 academic year at the University of Amsterdam as a Fulbright Scholar. After receiving his PhD from Yale (under the supervision of Frederic Fitch with a thesis on “The theory of partial recursive operators”) in 1958, Bill held appointments at Stanford University (1958–64) and the University of Illinois at Chicago Circle (1965–71) before joining the University of Chicago Department of Philosophy as Professor in 1972. He was a member of the Institute for Advanced Study in 1961/62, a Guggenheim Fellow 1968/69, and a Visiting Professor of Mathematics at the University of Aarhus in 1971/72. He retired from teaching in 1996 but remained active scientifically. He was elected a Fellow of the American Academy of Arts and Sciences in 2002 and delivered the Tarski Lectures in 2016.

Bill’s work up until 1980 concentrated on proof theory, specifically cut-elimination, functional interpretations, the ε-substitution method, type theory and lambda calculus. In Tait (1966), he proved the consistency of second order logic, settling the Takeuti conjecture positively. (Prawitz and Takahashi each independently settled Takeuti’s conjecture for the full simple theory of types a year or two later.) His two most well-known contributions are perhaps the development of the Schütte-Tait method of proving cut elimination (Tait 1968) and the method of proving normalization for lambda calculus using Tait computability predicates (Tait 1967). He is also sometimes credited with the observation that the Curry–Howard correspondence between formulas and types and proofs and lambda terms extends to normalization of natural deduction and reduction of the corresponding lambda term.

After 1981, Bill published extensively in the philosophy of mathematics and its history. His philosophical essays are collected in Tait (2005), and more recent essays can be found on his website. His most influential contribution in the philosophy of mathematics is what’s come to be known as “Tait’s thesis”: the identification of Hilbert’s “finitary standpoint” with what’s primitive recursively computable and provable in primitive recursive arithmetic PRA (Tait 1981, 2002, 2019).

You may be interested in reading about Bill’s way into logic and philosophy in his own words.

Tait’s thesis was a target of my dissertation, and Bill did me the honor of engaging deeply with my criticisms. I’m persuaded by his arguments in favor of Tait’s thesis—according to Ken Taylor, who I believe was a student of Bill, this makes me a “Taiter Tot”. He was very supportive of my early career (I owe invitations to present my work at the University of Chicago as well as my first invited talk at an ASL conference to him). We’ve both been involved in a project to edit and translate Paul Bernays’s philosophical writings, and corresponded regularly over the last couple of decades. He visited Calgary in 2004 (I got to take him hiking in Banff National Park), and he attended a workshop I organized at BIRS in 2007. He was a wonderful and inspiring person and I will always remember him fondly.

Tait, W. W. (1966). ‘A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic’, Bulletin of the American Mathematical Society 72/6: 980–3. DOI: 10.1090/S0002-9904-1966-11611-7

Tait, W. W. (1967). ‘Intensional interpretations of functionals of finite type I’, The Journal of Symbolic Logic 32/2: 198–212. DOI: 10.2307/2271658

Tait, W. W. (1968). ‘Normal derivability in classical logic’. Barwise J. (ed.) The Syntax and Semantics of Infinitary Languages, Lecture Notes in Mathematics, pp. 204–36. Springer: Berlin, Heidelberg. DOI: 10.1007/BFb0079691

Tait, W. W. (1981). ‘Finitism’, The Journal of Philosophy 78/9: 524–46. DOI: 10.2307/2026089

Tait, W. W. (2002). ‘Remarks on finitism’. Sieg W., Sommer R., and Talcott C. (eds) Reflections on the Foundations of Mathematics. Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, pp. 410–9. Association for Symbolic Logic and A K Peters.

Tait, W. W. (2005). The Provenance of Pure Reason: Essays in the Philosophy of Mathematics and Its History. New York: Oxford University Press.

Tait, W. W. (2019). ‘What Hilbert and Bernays meant by “finitism”’. Mras G. M., Weingartner P., and Ritter B. (eds) Philosophy of Logic and Mathematics Proceedings of the 41st International Ludwig Wittgenstein Symposium, pp. 249–62. De Gruyter. DOI: 10.1515/9783110657883-015

(Photo credit: Jean-Yves Girard, courtesy of Bill Tait)