The Seven Virtues of Simple Type Theory

William M. Farmer

2007

Abstract

Simple type theory, also known as higher-order logic, is a natural
extension of first-order logic which is simple, elegant, highly
expressive, and practical.  This paper surveys the virtues of simple
type theory and attempts to show that simple type theory is an
attractive alternative to first-order logic for practical-minded
scientists, engineers, and mathematicians.  It recommends that simple
type theory be incorporated into introductory logic courses offered by
mathematics departments and into the undergraduate curricula for
computer science and software engineering students.