The seven virtues of simple type theory (2008)

• Virtue 1: stt has a simple and highly uniform syntax.

• Virtue 2: The semantics of stt is based on a small collection of well-established ideas.

• Virtue 3: stt is a highly expressive logic.

• Virtue 4: stt admits categorical theories of infinite structures.

• Virtue 5: There is a proof system for stt that is simple, elegant, and powerful.

• Virtue 6: Henkin's general models semantics enables the techniques of first-order model theory to be applied to stt and illuminates the distinction between standard and nonstandard models.

• Virtue 7: There are practical extensions of stt that can be effectively implemented.