
Carnap, R. (1929) Abriss der Logistik, mit besonderer Berücksichtigung der Relationstheorie und ihrer Anwendungen (Outline of Logistic, with Special Consideration of the Theory of Relations and their Applications), Vienna: Springer. (This work includes an early formulation of simple type theory and its applications as a logical framework for the axiomatic method. Examples of axiomatic theories, such as set theory, Peano arithmetic, projective geometry and spacetime topology are given within the simple type theory formulated. The book was later expanded and developed as Carnap (1954).) 

Carnap, R. (1954) Einführung in die symbolische Logik, mit besonderer Berücksichtigung ihrer Anwendungen, Vienna: Springer; trans.
Introduction to Symbolic Logic and its Applications, New York: Dover, 1958. (A simple, clear description of Carnap’s version of simple type theory can be found in this book, which also includes many important applications of type theory to the construction of the different kinds of numbers, the foundations of mathematics, spacetime physics, anthropological kinship theories, and axiomatic biology.) 

Church, A. (1940) ‘A Formulation of the Simple Theory of Types’, Journal of Symbolic Logic
5: 56–68. (Elegant, but somewhat difficult for students with only an introductory understanding of logic.) 

Church, A. (1974) ‘Russellian Simple Type Theory’, Proceedings and Addresses of the American Philosophical Association
47: 21–33. (This paper includes a formulation of simple type theory with a primitive operator for propositional identity.) 

Church, A. (1976) ‘Comparison of Russell’s Resolution of the Semantical Antinomies with That of Tarski’, Journal of Symbolic Logic
41: 747–760. (An intermediate level understanding of logic should suffice to read this paper, which includes some important observations on how ramified, but not simple, type theory can avoid certain semantic and intensional paradoxes.) 

Church, A. (1984) ‘Russell’s Theory of Identity of Propositions’, Philosophia Naturalis
21 (2–4): 513–522. (Reviews Russell’s antinomy about propositions (Russell 1903: §500). Church shows that this antinomy cannot be resolved in simple type theory, given Russell’s view of propositional identity, but it can be resolved in ramified type theory.) 

Chwistek, L. (1922) ‘Über die Antinomien der Prinzipien der Mathematik’ (On the Antinomies of the Principles of Mathematics), Mathematische Zeitschrift
14: 236–243. (Now read mostly for historical interest.) 

Cocchiarella, N.B. (1987) Logical Studies in Early Analytic Philosophy, Columbus, OH: Ohio State University Press. (Chapter 1 includes a detailed description of the theory of logical types in the development of Russell’s views from his 1903 analysis of his paradox to the 1910–13 formulation of his ramified theory. Chapter 2 compares and reconstructs without paradox both Russell’s and Frege’s early versions of logicism. Chapter 5 explains how Russell’s 1925 modifications to his ramified theory commit him to a system too weak for his earlier logicism.) 

Copi, I. (1971) The Theory of Logical Types, London: Routledge & Kegan Paul. (A good, elementary introduction.) 

Gödel, K. (1931) ‘Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I’, Monatshefte für Mathematik und Physik
38: 173–198; trans. ‘On Formally Undecidable Propositions of Principia Mathematica and Related Systems’, in J.
van Heijenoort (ed.) From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Cambridge, MA: Harvard University Press, 1967, 592–617. (A classic, including Gödel’s famous incompleteness theorems as applied to a typetheoretical development of arithmetic.) 

Montague, R. (1974) Formal Philosophy: Selected Papers of Richard Montague, ed.
R.H.
Thomason, New Haven, CT: Yale University Press. (See especially the essays ‘Universal Grammar’ and ‘The Proper Treatment of Quantification in Ordinary English’, for Montague’s development of Church’s simple type theory as an intensional logic.) 

Myhill, J. (1979) ‘A Refutation of an Unjustified Attack on the Axiom of Reducibility’, in G.W.
Roberts (ed.) Bertrand Russell Memorial Volume, London: Allen & Unwin. (Readable with an intermediate level of understanding of logic; explains how the addition of the axiom of reducibility to ramified type theory results in a system essentially different from simple type theory.) 

Quine, W.V. (1936) ‘On the Axiom of Reducibility’, Mind
45: 498–500. (One of the earliest arguments that the addition of the axiom of reducibility to ramified type theory amounts to a system only notationally different from simple type theory.) 

Ramsey, F.P. (1931) ‘The Foundations of Mathematics’, in The Foundations of Mathematics and Other Logical Essays, ed.
R.B.
Braithwaite, London: Routledge & Kegan Paul. (Ramsey’s version of simple type theory, and his arguments why, as a foundation for mathematics, the simple theory is to be preferred to the ramified theory.) 

Russell, B.A.W. (1903) The Principles of Mathematics, Cambridge: Cambridge University Press; 2nd edn, London: Allen & Unwin, 1937; repr. London: Routledge, 1992, esp. ch. 10. (Russell’s first extended discussion of his paradox, along with some proposals for avoiding it. His first rough ideas about a theory of types are described in appendix B, which also contains an account, in §500, of his antinomy about propositions.) 

Russell, B.A.W. (1908) ‘Mathematical Logic as Based on the Theory of Types’, American Journal Of Mathematics
30: 222–262; repr. in Logic and Knowledge, Essays 1901–1950, ed.
R.C.
Marsh, London: Allen & Unwin, 1956, 59–102; repr. London: Routledge, 1992. (Accessible to readers with an intermediatelevel understanding of logic.) 

Russell, B.A.W. (1959) My Philosophical Development, London: Allen & Unwin; repr. London: Routledge, 1993. (An autobiographical account of the development of Russell’s philosophical and logical views.) 

Whitehead, A.N. and Russell, B.A.W. (1910–13) Principia Mathematica, Cambridge: Cambridge University Press, 3 vols; 2nd edn, 1925–7. (Development of the theory of ramified types.) 