William Alvin Howard
William Alvin Howard (December 11, 1926 – March 13, 2026) was a Canadian-born American mathematician and proof theorist best known for his work demonstrating formal similarity between intuitionistic logic and the simply typed lambda calculus that has come to be known as the Curry–Howard correspondence. He was also active in the theory of proof-theoretic ordinals.
Life and career
William Alvin Howard was born in Vancouver, British Columbia, Canada on December 11, 1926.[1] He received an undergraduate degree from the University of British Columbia and later received a master’s degree from the University of Illinois.[1]
Howard earned his Ph.D. at the University of Chicago in 1956 for his dissertation "k-fold recursion and well-ordering".[2] He was a student of Saunders Mac Lane.
The Howard ordinal (also known as the Bachmann–Howard ordinal) was named after him.
Howard was the first to carry out an ordinal analysis of the intuitionistic theory of inductive definitions.[3]p.27
He was elected to the 2018 class of fellows of the American Mathematical Society.[4]
Howard died in Chicago on March 13, 2026, at the age of 99.[1]
References
- ^ a b c "William Alvin Howard". Chicago Tribune. 31 May 2026. Retrieved 31 May 2026.
- ^ "Holdings: k-fold recursion and well-ordering". The University of Chicago Library Catalog. Retrieved 2015-05-04.
- ^ M. Rathjen, "Proof Theory: From arithmetic to set theory". Accessed 22 February 2024.
- ^ 2018 Class of the Fellows of the AMS, American Mathematical Society, retrieved 2017-11-03
External links
- Entry for William Alvin Howard at the Mathematics Genealogy Project
- Howard, W. A.; Kreisel, G. (September 1966). "Transfinite Induction and Bar Induction of Types Zero and One, and the Role of Continuity in Intuitionistic Analysis". The Journal of Symbolic Logic. 3 (3). Association for Symbolic Logic: 325–358. doi:10.2307/2270450. JSTOR 2270450. S2CID 5683782.