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.