From time to time, I receive requests from mathematicians for recommendations on scientific literature. My recommendation is always chapter 5 of Andrews’ 2002 textbook, in which the higher-order logic Q0 is presented [Andrews, 2002, pp. 210–215], and elementary logic developed (e.g., the derivation of the rule of Modus Ponens [p. 224]). For the full reference, please see the overview.
Further Resources
- Ken Kubota: Foundations of Mathematics (Genealogy and Overview)
- Peter B. Andrews: Q0 (“A Formulation Based on Equality”)
- Ken Kubota: R0 (polymorphic and dependent type theory, a further development of the higher-order logic Q0)
- Homepage of Peter B. Andrews
- Homepage of Ken Kubota