Abstraction Logic (Founder's Edition)

Abstraction logic is a new logic combining exceptional simplicity with astonishing generality. It combines the best features of first-order logic and higher-order logic, while avoiding their respective drawbacks. It manages to do so because it is based on a simple understanding of the mathematical universe, its operations and, in particular, its operators. Abstraction algebra encodes this understanding as a formal language, generalising abstract algebra. It is the right setting for the treatment of alpha equivalence. Abstraction logic then turns abstraction algebra into a logic by considering truth values as a partially ordered substructure of the mathematical universe. A key property of this logic is that formulas are merely terms. Among the presented proof systems are natural deduction, which is sound if truth values form a complete lattice, and sequent calculus, which is sound if truth values form a complete bi-Heyting algebra. By constructing the Rasiowa model, we prove that natural deduction is a complete proof system for abstraction logic.

This is the first book on abstraction logic. It presents abstraction logic in its most recent and comprehensive form, and supersedes all previous publications on abstraction logic.

About the Author

Steven Obua holds a Diplom in mathematics with a focus on computer science from the Technische Universität München (TUM), where he also spent time studying at the University of San Francisco. He earned his PhD in interactive theorem proving from TUM, and as a member of the Isabelle development team during his doctoral studies, he made significant contributions to the Flyspeck project, which successfully verified the proof of the Kepler conjecture.

His postdoctoral research included work on the verification of Microsoft's hypervisor and a brief but influential period at École Polytechnique Fédérale de Lausanne exploring the design of a novel theorem proving system. At the University of Edinburgh, he was the researcher co-investigator for ProofPeer, an EPSRC-funded project pioneering collaborative theorem proving.

Dr. Obua's career spans both academia and industry, where he has worked in content management, insurance, mobile app development, hardware and software formal verification, gaming and computer-aided design. He is currently developing Practal, a new system that aims to empower vision through precision, based on abstraction logic.