In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general. In programming language theory, a branch of computer science, type theory can refer to the design, analysis and study of type systems, although some computer scientists limit the term's meaning to the study of abstract formalisms such as typed λ-calculi.
Bertrand Russell invented the first type theory in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox. This theory of types features prominently in Whitehead and Russell's Principia Mathematica. It avoids Russell's paradox by first creating a hierarchy of types, then assigning each mathematical (and possibly other) entity to a type. Objects of a given type are built exclusively from objects of preceding types (those lower in the hierarchy), thus preventing loops.
Alonzo Church, inventor of the lambda calculus, developed a higher-order logic commonly called Church's Theory of Types,[1] in order to avoid the Kleene–Rosser paradox afflicting the original pure lambda calculus. Church's type theory is a variant of the lambda calculus in which expressions (also called formulas or λ-terms) are classified into types, and the types of expressions restrict the ways in which they can be combined. In other words, it is a typed lambda calculus. The article Church's Type Theory in the Stanford Encyclopedia of Philosophy is devoted to this subject.
Today many other such calculi are in use, including Per Martin-Löf's Intuitionistic type theory, Jean-Yves Girard's System F and the Calculus of Constructions. In typed lambda calculi, types play a role similar to that of sets in set theory.
Origin of Russell's Theory of Types: In a letter to Gottlob Frege (1902) Russell announced his discovery of the paradox in Frege's Begriffsschrift.[2] Frege promptly responded, acknowledging the problem and proposing a solution in a technical discussion of "levels". To quote Frege:
Incidentally, it seems to me that the expression "a predicate is predicated of itself" is not exact. A predicate is as a rule a first-level function, and this function requires an object as argument and cannot have itself as argument (subject). Therefore I would prefer to say "a concept is predicated of its own extension".[3]
He goes about showing how this might work but seems to pull back from it. As a consequence of what has become known as Russell's paradox both Frege and Russell had to quickly amend works that they had at the printers. In an Appendix B that Russell tacked on to his 1903 The Principles of Mathematics one finds his "tentative" "theory of types".[4]
The matter plagued Russell for about five years (1903–1908). Willard Quine in his preface to Russell's (1908a) Mathematical logic as based on the theory of types[5] presents a historical synopsis of the origin of the theory of types and the "ramified" theory of types: Russell proposed in turn a number of alternatives: (i) abandoning the theory of types (1905) followed by three theories in 1905: (ii.1) the zigzag theory, (ii.2) theory of limitation of size, (ii.3) the no-class theory (1905–1906), then (iii) readopting the theory of types (1908ff)".
Quine observes that Russell's introduction of the notion of "apparent variable" had the following result: "the distinction between 'all' and 'any': 'all' is expressed by the bound ('apparent') variable of universal quantification, which ranges over a type, and 'any' is expressed by the free ('real') variable which refers schematically to any unspecified thing irrespective of type". Quine dismisses this notion of "bound variable" as "pointless apart from a certain aspect of the theory of types".[6]
Quine explains the ramified theory as follows: "It has been so called because the type of a function depends both on the types of its arguments and on the types of the apparent variables contained in it (or in its expresion), in case these exceed the types of the arguments".[7] Stephen Kleene in his 1952 Introduction to Metamathematics describes the ramified theory of types this way:
- The primary objects or individuals (i.e. the given things not being subjected to logical analysis) are assigned to one type (say type 0), the properties of individuals to type 1, properties of properties of individuals to type 2, etc.; and no properties are admitted which do not fall into one of these logical types (e.g. this puts the properties 'predicable' and 'impredicable' ... outside the pale of logic). A more detailed account would describe the admitted types for other objects as relations and classes. Then to exclude impredicative definitions within a type, the types above type 0 are further separated into orders. Thus for type 1, properties defined without mentioning any totality belong to order 0, and properties defined using the totality of properties of a given order belong to the next higher order. ... But this separation into orders makes it impossible to construct the familiar analysis, which we saw above contains impredicative definitions. To escape this outcome, Russell postulated his axiom of reducibility, which asserts that to any property belonging to an order above the lowest, there is a coextensive property (i.e. one possessed by exactly the same objects) of order 0. If only definable properties are considered to exist, then the axiom means that to every impredicative definition within a given type there is an equivalent predicative one (Kleene 1952:44-45).
But because the stipulations of the ramified theory would prove (to quote Quine) "onerous", Russell in his 1908 Mathematical logic as based on the theory of types[8] also would propose his axiom of reducibility. By 1910 Whitehead and Russell in their Principia Mathematica would further augment this axiom with the notion of a matrix -- a fully extensional specification of a function. From its matrix a function could be derived by the process of "generalization" and vice versa, i.e. the two processes are reversible -- (i) generalization from a matrix to a function (by using apparent variables) and (ii) the reverse process of reduction of type by courses-of-values substitution of arguments for the apparent variable. By this method impredicativity could be avoided.[9]
Eventually Emil Post (1921) would lay waste to Russell's "cumbersome"[10] Theory of Types with his "truth functions" and their truth tables. In his "Introduction" to his 1921 Post places the blame on Russell's notion of apparent variable: "Whereas the complete theory [of Whitehead and Russell (1910, 1912, 1913)] requires for the enunciation of its propositions real and apparent variables, which represent both individuals and propositional functions of different kinds, and as a result necessitates the cumbersome theory of types, this subtheory uses only real variables, and these real variables represent but one kind of entity, which the authors have chosen to call elementary propositions".
At about the same time Ludwig Wittgenstein made short work of the theory of types in his 1922 work Tractatus Logico-Philosophicus in which he points out the following in parts 3.331–3.333:
3.331 From this observation we get a further view – into Russell's Theory of Types. Russell's error is shown by the fact that in drawing up his symbolic rules he has to speak of the meanings of his signs.
3.332 No proposition can say anything about itself, because the propositional sign cannot be contained in itself (that is the whole "theory of types").
3.333 A function cannot be its own argument, because the functional sign already contains the prototype of its own argument and it cannot contain itself...
Wittgenstein proposed the truth-table method as well. In his 4.3 through 5.101, Wittgenstein adopts an unbounded Sheffer stroke as his fundamental logical entity and then lists all 16 functions of two variables (5.101).
The notion of matrix-as-truth-table appears as late as the 1940-1950's in the work of Tarski, e.g. his 1946 indexes "Matrix, see: Truth table"[11]
Russell in his 1920 Introduction to Mathematical Philosophy devotes an entire chapter to "The axiom of Infinity and logical types" wherein he states his concerns: "Now the theory of types emphatically does not belong to the finished and certain part of our subject: much of this theory is still inchoate, confused, and obscure. But the need of some doctrine of types is less doubtful than the precise form the doctrine should take; and in connection with the axiom of infinity it is particularly easy to see the necessity of some such doctrine".[12]
Russell abandons the axiom of reducibility: In the second edition of Principia Mathematica (1927) he acknowledges Wittgenstein's argument.[13] At the outset of his Introduction he declares "there can be no doubt ... that there is no need of the distinction between real and apparent variables...".[14] Now he fully embraces the matrix notion and declares "A function can only appear in a matrix through its values" (but demurs in a footnote: "It takes the place (not quite adequately) of the axiom of reducibility"[15]). Furthermore, he introduces a new (abbreviated, generalized) notion of "matrix", that of a "logical matrix . . . one that contains no constants. Thus p|q is a logical matrix".[16] Thus Russell has virtually abandoned the axiom of reducibility,[17] but in his last paragraphs he states that from "our present primitive propositions" he cannot derive "Dedekindian relations and well-ordered relations" and observes that if there is a new axiom to replace the axiom of reducibility "it remains to be discovered".[18]
In the 1920s, Leon Chwistek[19] and Frank P. Ramsey[20] noticed that, if one is willing to give up the vicious circle principle, the hierarchy of levels of types in the "ramified theory of types" (see the History section for more on this) can be collapsed.
The resulting restricted logic is called the theory of simple types[21] or, perhaps more commonly, simple type theory.[22] Detailed formulations of simple type theory were published in the late 1920s and early 1930s by R. Carnap, F. Ramsey, W.V.O. Quine, and A. Tarski. In 1940 Alonzo Church (re)formulated it as simply typed lambda calculus.[23] and examined by Gödel in his 1944. A survey of these developments is found in Collins (2012).[24]
Kurt Gödel in his 1944 Russell's mathematical logic gave the following definition of the "theory of simple types" in a footnote:
- By the theory of simple types I mean the doctrine which says that the objects of thought (or, in another interpretation, the symbolic expressions) are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such relations, etc. (with a similar hierarchy for extensions), and that sentences of the form: " a has the property φ ", " b bears the relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of types fitting together. Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded. That the theory of simple types suffices for avoiding also the epistemological paradoxes is shown by a closer analysis of these. (Cf. Ramsey 1926 and Tarski 1935, p. 399).".[25]
He concluded the (1) theory of simple types and (2) axiomatic set theory, "permit the derivation of modern mathematics and at the same time avoid all known paradoxes" (Gödel 1944:126); furthermore, the theory of simple types "is the system of the first Prinicipa [Principia Mathematica] in an appropriate interpretation. . . . [However], many symptoms show only too clearly, however, that the primitive concepts need further elucidation" (Gödel 1944:126).
The following system is Mendelson's (1997, 289–293) ST. ST is equivalent with Russell's ramified theory plus the Axiom of reducibility. The domain of quantification is partitioned into an ascending hierarchy of types, with all individuals assigned a type. Quantified variables range over only one type; hence the underlying logic is first-order logic. ST is "simple" (relative to the type theory of Principia Mathematica) primarily because all members of the domain and codomain of any relation must be of the same type. There is a lowest type, whose individuals have no members and are members of the second lowest type. Individuals of the lowest type correspond to the urelements of certain set theories. Each type has a next higher type, analogous to the notion of successor in Peano arithmetic. While ST is silent as to whether there is a maximal type, a transfinite number of types poses no difficulty. These facts, reminiscent of the Peano axioms, make it convenient and conventional to assign a natural number to each type, starting with 0 for the lowest type. But type theory does not require a prior definition of the naturals.
The symbols peculiar to ST are primed variables and infix Failed to parse (Missing texvc executable; please see math/README to configure.): \in . In any given formula, unprimed variables all have the same type, while primed variables (Failed to parse (Missing texvc executable; please see math/README to configure.): x' ) range over the next higher type. The atomic formulas of ST are of two forms, Failed to parse (Missing texvc executable; please see math/README to configure.): x=y
(identity) and Failed to parse (Missing texvc executable; please see math/README to configure.): y\in x'
. The infix symbol Failed to parse (Missing texvc executable; please see math/README to configure.): \in
suggests the intended interpretation, set membership.
All variables appearing in the definition of identity and in the axioms Extensionality and Comprehension, range over individuals of one of two consecutive types. Only unprimed variables (ranging over the "lower" type) can appear to the left of 'Failed to parse (Missing texvc executable; please see math/README to configure.): \in ', whereas to its right, only primed variables (ranging over the "higher" type) can appear. The first-order formulation of ST rules out quantifying over types. Hence each pair of consecutive types requires its own axiom of Extensionality and of Comprehension, which is possible if Extensionality and Comprehension below are taken as axiom schemata "ranging over" types.
- Identity, defined by Failed to parse (Missing texvc executable; please see math/README to configure.): x=y\leftrightarrow\forall z' [x\in z'\leftrightarrow y\in z']
.
- Extensionality. An axiom schema. Failed to parse (Missing texvc executable; please see math/README to configure.): \forall x[x\in y' \leftrightarrow x\in z'] \rightarrow [y'=z']
.
- Let Failed to parse (Missing texvc executable; please see math/README to configure.): \Phi(x)
denote any first-order formula containing the free variable Failed to parse (Missing texvc executable; please see math/README to configure.): x
.
- Comprehension. An axiom schema. Failed to parse (Missing texvc executable; please see math/README to configure.): \exists z'\forall x[x\in z'\leftrightarrow \Phi(x)]
.
- Remark. Any collection of elements of the same type may form an object of the next higher type. Comprehension is schematic with respect to Failed to parse (Missing texvc executable; please see math/README to configure.): \Phi(x)
as well as to types.
- Infinity. There exists a nonempty binary relation Failed to parse (Missing texvc executable; please see math/README to configure.): R
over the individuals of the lowest type, that is irreflexive, transitive, and strongly connected: Failed to parse (Missing texvc executable; please see math/README to configure.): \forall x,y [x\neq y\rightarrow[xRy\vee yRx]]
.
- Remark. Infinity is the only true axiom of ST and is entirely mathematical in nature. It asserts that Failed to parse (Missing texvc executable; please see math/README to configure.): R
is a strict total order, with a domain identical to its codomain. If 0 is assigned to the lowest type, the type of Failed to parse (Missing texvc executable; please see math/README to configure.): R
is 3. Infinity can be satisfied only if the (co)domain of Failed to parse (Missing texvc executable; please see math/README to configure.): R
is infinite, thus forcing the existence of an infinite set. If relations are defined in terms of ordered pairs, this axiom requires a prior definition of ordered pair; the Kuratowski definition, adapted to ST, will do. The literature does not explain why the usual axiom of infinity (there exists an inductive set) of ZFC of other set theories could not be married to ST.
ST reveals how type theory can be made very similar to axiomatic set theory. Moreover, the more elaborate ontology of ST, grounded in what is now called the "iterative conception of set," makes for axiom (schemata) that are far simpler than those of conventional set theories, such as ZFC, with simpler ontologies. Set theories whose point of departure is type theory, but whose axioms, ontology, and terminology differ from the above, include New Foundations and Scott–Potter set theory.
Church’s type theory has been extensively studied by two of Church’s students, Leon Henkin and Peter B. Andrews. Since ST is a higher order logic, and in higher order logics one can define propositional connectives in terms of logical equivalence and quantifiers, in 1963 Henkin developed a formulation of ST based on equality, but in which he restricted attention to propositional types. This was simplified later that year by Andrews in his theory Q0.[26] In this respect ST can be seen as a particular kind of a higher-order logic, classified by P.T. Johnstone in Sketches of an Elephant, as having a lambda-signature, that is a higher-order signature that contains no relations, and uses only products and arrows (function types) as type constructors. Furthermore, as Johnstone put it, ST is "logic-free" in the sense that it contains no logical connectives or quantifiers in its formulae.[27]
Polymorphism is a programming language feature that allows values of different data types to be handled using a uniform interface. The concept of parametric polymorphism applies to both data types and functions. A function that can evaluate to or be applied to values of different types is known as a polymorphic function. A data type that can appear to be of a generalized type (e.g., a list with elements of arbitrary type) is designated polymorphic data type like the generalized type from which such specializations are made.
Dependent type is a type that depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like ATS, Agda and Epigram.
An example is the type of n-tuples of real numbers. This is a dependent type because the type depends on the value n.
Main article:
Type systemThe most obvious application of type theory is in constructing type checking algorithms in the semantic analysis phase of compilers for programming languages. Definitions of type system vary, but the following one due to Benjamin C. Pierce roughly corresponds to the current consensus in the programming language theory community:
[A type system is a] tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.[28]
In other words, a type system divides program values into sets called types — this is called a type assignment — and makes certain program behaviors illegal on the basis of the types that are thus assigned. For example, a type system may classify the value "hello" as a string and the value 5 as a number, and prohibit the programmer from adding "hello" to 5 based on that type assignment. In this type system, the program
"hello" + 5
would be illegal. Hence, any program permitted by the type system would be provably free from the erroneous behavior of adding strings and numbers.
Type theory is also widely in use in formal theories of semantics of natural languages, especially Montague grammar and its descendants. The most common construction takes the basic types Failed to parse (Missing texvc executable; please see math/README to configure.): e
and Failed to parse (Missing texvc executable; please see math/README to configure.): t
for individuals and truth-values, respectively, and defines the set of types recursively as follows:
- if Failed to parse (Missing texvc executable; please see math/README to configure.): a
and Failed to parse (Missing texvc executable; please see math/README to configure.): b
are types, then so is Failed to parse (Missing texvc executable; please see math/README to configure.): \langle a,b\rangle
.
- Nothing except the basic types, and what can be constructed from them by means of the previous clause are types.
A complex type Failed to parse (Missing texvc executable; please see math/README to configure.): \langle a,b\rangle
is the type of functions from entities of type Failed to parse (Missing texvc executable; please see math/README to configure.): a
to entities of type Failed to parse (Missing texvc executable; please see math/README to configure.): b
. Thus one has types like Failed to parse (Missing texvc executable; please see math/README to configure.): \langle e,t\rangle
which are interpreted as elements of the set of functions from entities to truth-values, i.e. characteristic functions of sets of entities. An expression of type Failed to parse (Missing texvc executable; please see math/README to configure.): \langle\langle e,t\rangle,t\rangle
is a function from sets of entities to truth-values, i.e. a (characteristic function of a) set of sets. This latter type is standardly taken to be the type of natural language quantifiers, like everybody or nobody (Montague 1973, Barwise and Cooper 1981).
Gregory Bateson introduced a theory of logical types into the social sciences; his notions of double bind and logical levels are based on Russell's theory of types.
- Mendelson, Elliot, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
- W. Farmer, The seven virtues of simple type theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267–286.
- ^ Alonzo Church, A formulation of the simple theory of types, The Journal of Symbolic Logic 5(2):56–68 (1940)
- ^ Russell's (1902) Letter to Frege appears, with commentary, in van Heijenoort 1967:124-125.
- ^ Frege (1902) Letter to Russell appears, with commentary, in van Heijenoort 1967:126-128.
- ^ cf Quine's commentary before Russell (1908a) Mathematical Logic as based on the theory of types in van Heijenoort 1967:150
- ^ cf commentary by W. V. O. Quine before Russell's (1908a) Mathematical logic as based on the theory of types in van Hiejenoort 1967:150-153
- ^ Quine's commentary before Russell (1908a) Mathematical logic as based on the theory of types cf van Heijenoort 1967:151
- ^ Quine's commentary commentary before Russell (1908a) Mathematical logic as based on the theory of types cf van Heijenoort 1967:151
- ^ Russell (1908a) Mathematical Logic as based on the theory of types in van Heijenoort 1967:153-182
- ^ cf in particular p. 51 in Chapter II The theory of Logical Types and *12 The Hierarchy of Types and the Axiom of Reducibility pp. 162-167. Whitehead and Russell (1910-1913, 1927 2nd edition) Principia Mathematica
- ^ Post (1921) Introduction to a general theory of elementary propositions in van Heijenoort 1967:264-283, in particular p. 265"
- ^ Tarski 1946, Introduction to Logic and to the Methodology of Deductive Sciences, Dover republication 1995
- ^ Russell 1920:135
- ^ cf "Introduction" to 2nd edition, Russell 1927:xiv and Appendix C
- ^ cf "Introduction" to 2nd edition, Russell 1927:i
- ^ cf "Introduction" to 2nd edition, Russell 1927:xxix
- ^ The vertical bar " | " is the Sheffer stroke. cf "Introduction" to 2nd edition, Russell 1927:xxxi
- ^ "The theory of classes is at once simplified in one direction and complicated in another by the assumption that functions only occur through their values and by the abandonment of the axiom of reducibility" cf "Introduction" to 2nd edition, Russell 1927:xxxix
- ^ These quotes from "Introduction" to 2nd edition, Russell 1927:xliv-xlv.
- ^ L. Chwistek, Antynomje logikiformalnej, Przeglad Filozoficzny 24 (1921) 164–171
- ^ F.P. Ramsey, The foundations of mathematics, Proceedings of the London Mathematical Society, Series 2 25 (1926) 338–384.
- ^ Gödel 1944, pages 126 and 136-138, footnote 17: "Russell's mathematical logic" appearing in Kurt Gödel: Collected Works: Volume II Publications 1938-1974, Oxford University Press, New York NY, ISBN 978-0-19-514721-6(v.2.pbk).
- ^ This does not mean the theory is "simple", it means that the theory is restricted: types of different orders are not to be mixed: "Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded." Gödel 1944, pages 127, footnote 17: "Russell's mathematical logic" appearing in Kurt Gödel: Collected Works: Volume II Publications 1938-1974, Oxford University Press, New York NY, ISBN 978-0-19-514721-6(v.2.pbk).
- ^ A. Church, A formulation of the simple theory of types, Journal of Symbolic Logic 5 (1940) 56–68.
- ^ J. Collins, A History of the Theory of Types: Developments after the Second Edition of 'Principia Mathematica'. LAP Lambert Academic Publishing (2012). ISBN 978-3-8473-2963-3, esp. chs. 4-6.
- ^ Gödel 1944:126 footnote 17: "Russell's mathematical logic" appearing in Kurt Gödel: Collected Works: Volume II Publications 1938-1974, Oxford University Press, New York NY, ISBN 978-0-19-514721-6(v.2.pbk).
- ^ Stanford Encyclopedia of Philosophy: Church's Type Theory" – by Peter Andrews (adapted from his book).
- ^ P.T. Johnstone, Sketches of an elephant, p. 952
- ^ Types and Programming Languages, Benjamin C. Pierce, The MIT Press, Cambridge, MA. (2002), ISBN 0-262-16209-1.
- Constable, Robert L., 2002, "Naïve Computational Type Theory," in H. Schwichtenberg and R. Steinbruggen (eds.), Proof and System-Reliability: 213–259. Intended as an type theory counterpart of Paul Halmos's (1960) Naïve Set Theory
- Andrews B., Peter (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed.. Kluwer Academic Publishers.. ISBN 978-1-4020-0763-7.
- Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3. http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html. Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics.
- Collins, Jordan E. (2012). A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'. LAP Lambert Academic Publishing. ISBN 978-3-8473-2963-3. Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of 'Principia Mathematica'.
- Cardelli, Luca, 1997, "Type Systems," in Allen B. Tucker, ed., The Computer Science and Engineering Handbook. CRC Press: 2208–2236.
- Thompson, Simon, 1991. Type Theory and Functional Programming. Addison-Wesley. ISBN 0-201-41667-0.
- J. Roger Hindley, Basic Simple Type Theory, Cambridge University Press, 2008, ISBN 0-521-05422-2 (also 1995, 1997). A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. Book review
- Stanford Encyclopedia of Philosophy: Type Theory" – by Thierry Coquand.
- Fairouz D. Kamareddine, Twan Laan, Rob P. Nederpelt, A modern perspective on type theory: from its origins until today, Springer, 2004, ISBN 1-4020-2334-0
- José Ferreirós, José Ferreirós Domínguez, Labyrinth of thought: a history of set theory and its role in modern mathematics, Edition 2, Springer, 2007, ISBN 3-7643-8349-6, chapter X "Logic and Type Theory in the Interwar Period"
- Bertrand Russell (1903) The Principles of Mathematics: Vol. 1, Cambridge at the University Press, Cambridge, UK, republished as a googlebook.
- Bertrand Russell (1920) Introduction to Mathematical Philosophy (second edition), Dover Publishing Inc., New York NY, ISBN 0-486-27724-0 (pbk).
- Alfred Tarski (1946) Introduction to Logic and to the Methodology of Deductive Sciences, republished 1995 by Dover Publications, Inc., New York, NY ISBN 0-486-28462-X
- Jean van Heijenoort (1967, 3rd printing 1976), From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, Cambridge, MA, ISBN 0-674-32449-8 (pbk)
- Bertrand Russell (1902) Letter to Frege with commentary by van Heijenoort, pages 124-125. Wherein Russell announces his discovery of a "paradox" in Frege's work.
- Gottlob Frege (1902) Letter to Russell with commentary by van Heijenoort, pages 126-128.
- Bertrand Russell (1908a) Mathematical logic as based on the theory of types, with commentary by Willard Quine, pages 150-182.
- Emil Post (1921) Introduction to a general theory of elementary propositions, with commentary by van Heijenoort, pages 264-283.
- Alfred North Whitehead and Bertrand Russell(1910–1913, 1927 2nd edition reprinted 1962), Principia Mathematica to *56, Cambridge at the University Press, London UK, no ISBN or US card catalog number.
- Ludwig Wittgenstein (republished 2009) Major Works: Selected Philosophical Writings", HarperCollins, New York. ISBN 978-0-06-155024-9. Wittgenstein's (1921 in English) Tractatus Logico-Philosophicus pages 1–82.
|
|
|
|
Overview
|
|
Academic
areas |
|
|
Foundational
concepts |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
![OC ReMix #2730: Pokémon X 'WHAT TYPE ARE YOU' [Title] by Theory of N](http://web.archive.org./web/20130901060558im_/http://i1.ytimg.com/vi/Kr0X8ltkU60/default.jpg "OC ReMix #2730: Pokémon X 'WHAT TYPE ARE YOU' [Title] by Theory of N")
![Sylveon's Type [THEORY] - AstronomicalFilmz](http://web.archive.org./web/20130901060558im_/http://i.ytimg.com/vi/cDzIrPu3Upg/default.jpg "Sylveon's Type [THEORY] - AstronomicalFilmz")
![[icon]](http://web.archive.org./web/20130901060558/http://en.wikipedia.org/wiki/File:Wiki_letter_w_cropped.svg){kind=small}
![[1]](http://web.archive.org./web/20130901060558/http://photos-g.ak.fbcdn.net/photos-ak-sf2p/v323/79/46/1393560204/n1393560204_30411518_520.jpg){kind=link}