William Alvin Howard

{{short description|American mathematician}}

File:William Alvin Howard May 2004.jpg

William Alvin Howard (born 1926) is a 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 has also been active in the theory of proof-theoretic ordinals. He earned his Ph.D. at the University of Chicago in 1956 for his dissertation "k-fold recursion and well-ordering".{{cite web | url=https://catalog.lib.uchicago.edu/vufind/Record/4242603/Holdings#tabnav | title=Holdings: k-fold recursion and well-ordering | publisher=The University of Chicago Library Catalog | accessdate=2015-05-04}} He was a student of Saunders Mac Lane.

The Howard ordinal (also known as the Bachmann–Howard ordinal) was named after him.

He was the first to carry out an ordinal analysis of the intuitionistic theory $\backslash mathbf\{ID\}^i\_1(\backslash mathcal\; O)$ of inductive definitions.M. Rathjen, "[https://www1.maths.leeds.ac.uk/~rathjen/Sepp-chiemsee.pdf Proof Theory: From arithmetic to set theory]". Accessed 22 February 2024.^p.27

He was elected to the 2018 class of fellows of the American Mathematical Society.{{citation|url=http://ams.org/profession/ams-fellows/new-fellows|title=2018 Class of the Fellows of the AMS|publisher=American Mathematical Society|accessdate=2017-11-03}}