• 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:

• 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.