 Regarding condition (2), STT with axioms of infinity and choice permits the full development of classical number theory and analysis. Church (1959 [BE: 493]) notes that STT with an axiom of infinity and Zermelo set theory (Z) are of “comparable” provability strength but that Z is slightly stronger. (Indeed, the first detailed proof that Z is stronger than STT with infinity is given in a thesis written under Church’s supervision by Kemeny (1949). It is now known that STT with an axiom of infinity is equi-consistent with and has as much provability strength as bounded Zermelo set theory (see Farmer 2008 and the citations therein). Moreover, Church’s STT has turned out to be an important tool in the investigation of automated reasoning and proof verification in computer science. The typed system with λ is particularly well suited for the use and development of programming languages and paradigms (such as Haskell and Functional Programming [Hudak 1989]). Thus, Church succeeded in providing a type theoretical alternative to set theory as a foundation for mathematics. (It’s also worth mentioning that through his work on finite automata, Church contributed in yet another fundamental way to computer science [1960, 1962a].)