The seven virtues of simple type theory (2008) [pdf] (imps.mcmaster.ca)

William M. Farmer’s paper revisits simple type theory (STT, a form of higher‑order logic) and makes a pragmatic case for its wider adoption in mathematics, computer science, and engineering education. After tracing the history from Russell’s ramified types through Church’s elegant function‑based formulation, Henkin’s completeness result, and Andrews’ Q and the TPS prover, Farmer presents a distilled version called stt and enumerates seven “virtues” that make it attractive: simplicity, elegance, expressiveness, and practical amenability to mechanization. He recommends teaching STT alongside or instead of first‑order logic in curricula because STT more naturally captures mathematical practice. Technically, STT extends first‑order logic by allowing higher‑order terms (sets, relations, functions), quantification over them, and a typed universe built from base types (individuals ι and truth ∗) and function types (α → β). Church’s lambda abstraction/application and definite description give compact abstraction mechanisms that avoid the verbosity and encodings required in first‑order formalisations (e.g., transitive closure, completeness of reals). The paper highlights that many modern theorem provers and proof assistants (Isabelle, PVS, TPS, and others) are based on Church‑style or constructive variants (Martin‑Löf/Agda/Coq), underlining STT’s central role in formalized mathematics, program verification, and scalable mechanized reasoning.