Peter B. Andrews, an American mathematician and Professor Emeritus at Carnegie Mellon University, passed away on April 21, 2025, at the age of 87. Andrews was a leading figure in the theory and applications of higher-order logic and automated reasoning.
Peter Andrews received his Ph.D. in Mathematics from Princeton University in 1964, where he was advised by the highly influential logician Alonzo Church. Andrews joined the Mathematics Department at Carnegie Mellon University in Pittsburgh in 1963 and remained there for 49 years, retiring in 2012.
Andrews’s research was motivated by a desire to develop tools that could enhance human reasoning with a vision for the eventual formalization of virtually all mathematical, scientific, and technical knowledge, as well as the development of automated reasoning tools to assist in managing this knowledge. He made progress on this vision by focusing his work primarily on automated deduction within Church’s version of higher-order logic based on the Simple Theory of Types.
A major achievement in his career was leading the development of TPS (Theorem Proving System), an automated theorem prover for higher-order classical logic. A subsystem, ETPS (Educational Theorem Proving System), was created to help students learn logic by interactively constructing natural deduction proofs. Andrews worked on this system with his research assistants from 1974 until his retirement.
Andrews also made significant contributions to the foundations of symbolic logic. He is notable for identifying a gap in Jacques Herbrand’s proof of the eponymous Herbrand’s theorem for first-order logic and corresponding with Burton Dreben about it. This collaboration led to a joint paper with Dreben and Stål Aanderaa in 1963, which provided a counterexample to a key lemma in Herbrand’s proof. It was later discovered that Kurt Gödel had privately noted a similar error decades earlier, though he did not publish it. Andrews also noted an error in Leon Henkin’s definition of general models for higher-order logic and provided a fix for it.
His book “An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof,” praised for its clear and concise presentation of logic, is one of the few textbooks that covers both the syntactic and semantic sides of higher-order logic using Church’s Simple Theory of Types.
In recognition of his significant contributions to automated deduction, Peter Andrews received the Herbrand Award in 2003. A Festschrift titled “Reasoning in Simple Type Theory” was published in 2008 in honor of his 70th birthday.
Peter is survived by his wife of nearly 40 years, Catherine Clair “Cate” Andrews, his sons, Lyle Andrews and Bruce (Tobi) Andrews, and his former wife, Linda Fitch. He will be missed.