The topic of type theory is fundamental both in logic and computerscience. We limit ourselves here to sketch some aspects that areimportant in logic. For the importance of types in computer science, werefer the reader for instance to Reynolds 1983 and 1985.

• 1. Paradoxes and Russell’s Type Theories
• 2. Simple Type Theory and the \(\lambda\)-Calculus
• 3. Ramified Hierarchy and Impredicative Principles
• 4. Type Theory/Set Theory
• 5. Type Theory/Category Theory
• 6. Extensions of Type System, Polymorphism, Paradoxes
• 7. Univalent Foundations
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Paradoxes and Russell’s Type Theories

The theory of types was introduced by Russell in order to cope withsome contradictions he found in his account of set theory and wasintroduced in “Appendix B: The Doctrine of Types”of Russell 1903. This contradiction was obtained by analysing atheorem of Cantor that no mapping

(where \(\Pow(X)\) is the class of subclasses of a class\(X)\) can be surjective; that is, \(F\) cannot be such thatevery member \(b\) of \(\Pow(X)\) is equal to\(F(a)\) for some element \(a\) of \(X\). Thiscan be phrased “intuitively” as the fact that there aremore subsets of \(X\) than elements of \(X\). The proof ofthis fact is so simple and basic that it is worthwhile giving ithere. Consider the following subset of \(X\):

This subset cannot be in the range of \(F\). For if \(A = F(a)\), forsome \(a\), then

which is a contradiction.

Some remarks are in order. First, the proofdoes not use the law of excluded middle and is thus validintuitionistically. Second, the method that is used, calleddiagonalisation was already present in the work of duBois-Reymond for building real functions growing faster than anyfunction in a given sequence of functions.

Russell analysed what happens if we apply this theorem to the casewhere A is the class of all classes, admitting that there is such aclass. He was then lead to consider the special class of classes thatdo not belong to themselves

We then have

It seems indeed that Cantor was already aware of the fact that theclass of all sets cannot be considered itself to be a set.

Russell communicated this problem to Frege, and his letter, togetherwith Frege’s answer appear in van Heijenoort 1967. It is importantto realise that the formulation (*) does not apply as it is to Frege’ssystem. As Frege himself wrote in his reply to Russell, the expression“a predicate is predicated of itself” is not exact. Fregehad a distinction betweenpredicates (concepts) andobjects. A (first-order) predicate applies to an object butit cannot have a predicate as argument. The exact formulation of theparadox in Frege’s system uses the notion of theextension ofa predicate \(P\), which we designate as \(\varepsilon P\).The extension of a predicate is itself an object. The important axiomV is:

This axiom asserts that the extension of \(P\) is identical to theextension of \(Q\) if and only if \(P\) and \(Q\) are materiallyequivalent. We can then translate Russell’s paradox (*) inFrege’s system by defining the predicate

It can then been checked, using Axiom V in a crucial way, that

and we have a contradiction as well. (Notice that for defining thepredicate \(R\), we have used animpredicativeexistential quantification on predicates. It can be shown that thepredicative version of Frege’s system is consistent (seeHeck 1996 and for further refinements Ferreira 2002).

It is clear from this account that an idea of types was alreadypresent in Frege’s work: there we find a distinction between objects,predicates (or concepts), predicates of predicates, etc. (This pointis stressed in Quine 1940.) This hierarchy is called the“extensional hierarchy” by Russell (1959), and itsnecessity was recognised by Russell as a consequence of hisparadox.

2. Simple Type Theory and the \(\lambda\)-Calculus

As we saw above, the distinction: objects, predicates, predicate ofpredicates, etc., seems enough to block Russell’s paradox (and thiswas recognised by Chwistek and Ramsey). We first describe the typestructure as it is inPrincipia and later in this section wepresent the elegant formulation due to Church 1940 based on\(\lambda\)-calculus. The types can be defined as

1. \(i\) is the type of individuals
2. \((\,)\) is the type of propositions
3. if \(A_1 ,\ldots ,A_n\) are types then \((A_1 ,\ldots ,A_n)\) isthe type of \(n\)-ary relations over objects of respective types \(A_1,\ldots ,A_n\)

For instance, the type of binary relations over individuals is\((i, i)\), the type of binary connectives is\(((\,),(\,))\), the type of quantifiers over individuals is\(((i))\).

For forming propositions we use this type structure: thus \(R(a_1,\ldots ,a_n)\) is a proposition if \(R\) is of type \((A_1 ,\ldots,A_n)\) and \(a_i\) is of type \(A_i\) for \(i = 1,\ldots ,n\). Thisrestriction makes it impossible to form a proposition of the form\(P(P)\): the type of \(P\) should be of the form \((A)\), and \(P\)can only be applied to arguments of type \(A\), and thus cannot beapplied to itself since \(A\) is not the same as \((A)\).

However simple type theory is not predicative: we can define an object\(Q(x, y)\) of type \((i, i)\)by

Assume that we have two individuals \(a\) and \(b\) such that \(Q(a,b)\) holds. We can define \(P(x)\) to be \(Q(x, a)\). It is then clearthat \(P(a)\) holds, since it is \(Q(a, a)\). Hence \(P(b)\) holds aswell. We have proved, in an impredicative way, that \(Q(a, b)\)implies \(Q(b, a)\).

Alternative simpler formulations, which retain only the notion ofclasses, classes of classes, etc., were formulated by Gödel andTarski. Actually this simpler version was used by Gödel in his1931 paper on formally undecidable propositions. The discovery of theundecidable propositions may have been motivated by a heuristicargument that it is unlikely that one can extend the completenesstheorem of first-order logic to type theory (see the end of hisLecture at Königsberg 1930 in Gödel Collected Work, VolumeIII, Awodey and Carus 2001 and Goldfarb 2005). Tarski had a versionof the definability theorem expressed in type theory (see Hodges2008). See Schiemer and Reck 2013.

We have objects of type 0, for individuals, objects of type 1, forclasses of individuals, objects of type 2, for classes of classes ofindividuals, and so on. Functions of two or more arguments, likerelations, need not be included among primitive objects since one candefine relations to be classes of ordered pairs, and ordered pairs tobe classes of classes. For example, the ordered pair of individualsa, b can be defined to be \(\{\{a\},\{a,b\}\}\) where\(\{x,y\}\) denotes the class whose sole elements are \(x\) and\(y\). (Wiener 1914 had suggested a similar reduction of relations toclasses.) In this system, all propositions have the form \(a(b)\),where \(a\) is a sign of type \(n+1\) and \(b\) a sign of type\(n\). Thus this system is built on the concept of an arbitrary classor subset of objects of a given domain and on the fact that thecollection ofall subsets of the given domain can form a newdomain of the next type. Starting from a given domain of individuals,this process is then iterated. As emphasised for instance in Scott1993, in set theory this process of forming subsets is iterated intothetransfinite.

In these versions of type theory, as in set theory, functions are notprimitive objects, but are represented as functional relation. Theaddition function for instance is represented as a ternary relation byan object of type \((i,i,i)\). An elegantformulation of the simple type theory which extends it by introducingfunctions as primitive objects was given by Church in 1940. It usesthe \(\lambda\)-calculus notation (Barendregt 1997). Since such aformulation is important in computer science, for the connection withcategory theory, and for Martin-Löf type theory, we describe itin some detail. In this formulation, predicates are seen as a specialkind of functions (propositional functions), an idea that goes back toFrege (see for instance Quine 1940). Furthermore, the notion offunction is seen as more primitive than the notion of predicates andrelations, and a function is not defined anymore as a special kind ofrelation. (Oppenheimer and Zalta 2011 presents some arguments againstsuch a primitive representation of functions.) The types of thissystem are defined inductively as follows

1. there are two basic types \(i\) (the type of individuals)and \(o\) (the type of propositions)
2. if \(A, B\) are types then \(A \rightarrow B\), the type offunctions from \(A\) to \(B\), is a type

We can form in this way the types:

which correspond to the types \((i)\) and \(((i))\) but alsothe new types

It is convenient to write

for

In this way

corresponds to the type \((A_1 ,\ldots ,A_n)\).

First-order logic considers only types of the form

Notice that

stands for

(association to the right).

For the terms of this logic, we shall not follow Church’s account buta slight variation of it, due to Curry (who had similar ideas beforeChurch’s paper appeared) and which is presented in detail inR. Hindley’s book on type theory. Like Church, we use\(\lambda\)-calculus, which provides a general notation for functions

Here we have used the so-called BNF notation, very convenient incomputing science. This gives a syntactic specification of the\(\lambda\)-terms which, when expanded, means:

• every variable is a function symbol;
• every juxtaposition of two function symbols is a function symbol;
• every \(\lambda x.M\) is a function symbol;
• there are no other function symbols.

The notation for function application \(M N\) is alittle different than the mathematical notation, which would be\(M(N)\). In general,

stands for

(association to the left). The term \(\lambda x.M\) represents thefunction which to \(N\) associates \(M[x:=N\)]. This notation is soconvenient that one wonders why it is not widely used inmathematics. The main equation of \(\lambda\)-calculus is then\((\beta\)-conversion)

which expresses the meaning of \(\lambda x.M\)as a function. We have used \(M[x:=N\)] as anotation for the value of the expression that results when \(N\)is substituted for the variable \(x\) in the matrix \(M\).One usually sees this equation as a rewrite rule\((\beta\)-reduction)

Inuntyped lambda calculus, it may be that such rewritingdoes not terminate. The canonical example is given by the term\(\Delta = \lambda x.x x\) and the application

(Notice the similarity with Russell’s paradox.) The idea ofCurry is then to look at types as predicates over lambda terms,writing \(M:A\) to express that \(M\) satisfies the predicate/type\(A\). The meaning of

is then

which justifies the following rules

In general one works with judgements of the form

where \(x_1,..., x_n\) are distinctvariables, and \(M\) is a term having all free variables among\(x_1,..., x_n\). In order to beable to get Church’s system, one adds some constants in order to formpropositions. Typically

The term

represents the predicate of predicates that do not apply to themselves.This term does not have a type however, that is, it is not possible tofind \(A\) such that

which is the formal expression of the fact that Russell’s paradoxcannot be expressed. Leibniz equality

will be defined as

One usually writes \(\forall x[M\)] instead of \(\forall(\lambdax.M)\), and the definition of \(Q\) can then be rewritten as

This example again illustrates that we can formulate impredicative definitionsin simple type theory.

The use of \(\lambda\)-terms and \(\beta\)-reduction is mostconvenient for representing the complex substitution rules that areneeded in simple type theory. For instance, if we want to substitutethe predicate \(\lambda x.Q a x\) for \(P\) in the proposition

we get

and, using \(\beta\)-reduction,

In summary, simple type theory forbids self-application but not thecircularity present in impredicative definitions.

The \(\lambda\)-calculus formalism also allows for a clearer analysisof Russell’s paradox. We can see it as the definition of thepredicate

If we think of \(\beta\)-reduction as the process of unfolding adefinition, we see that there is a problem already with understandingthe definition of R R

In some sense, we have a non-wellfounded definition, which is asproblematic as a contradiction (a proposition equivalent to itsnegation). One important theorem, the normalisation theorem, says thatthis cannot happen with simple types: if we have\(M:A\) then \(M\) is normalisable in astrong way (any sequence of reductions starting from \(M\)terminates).

For more information on this topic, we refer to the entry onChurch’s simple type theory.

3. Ramified Hierarchy and Impredicative Principles

Russell introduced another hierarchy, that was not motivated by anyformal paradoxes expressed in a formal system, but rather by the fearof “circularity” and by informal paradoxes similar to theparadox of the liar. If a man says “I am lying”, then wehave a situation reminiscent of Russell’s paradox: a proposition whichis equivalent to its own negation. Another informal such paradoxicalsituation is obtained if we define an integer to be the “leastinteger not definable in less than 100 words”. In order toavoid such informal paradoxes, Russell thought it necessary tointroduce another kind of hierarchy, the so-called “ramifiedhierarchy”. The need for such a hierarchy is hinted in AppendixB of Russell 1903. Interestingly this is connected there to thequestion of the identity of equivalent propositions and of the logicalproduct of a class of propositions. A thorough discussion can be foundin Chapter 10 of Russell 1959. Since this notion of ramifiedhierarchy has been extremely influential in logic and especially prooftheory, we describe it in some details.

In order to further motivate this hierarchy, here is one example dueto Russell. If we say

Napoleon was Corsican.

we do not refer in this sentence to any assemblage of properties. Theproperty “to be Corsican” is said to bepredicative. If we say on the other hand

Napoleon had all the qualities of a great general

we are referring to a totality of qualities. The property “tohave all qualities of a great general” is said to beimpredicative.

Another example, also coming from Russell, shows how impredicative properties can potentially lead to problems reminiscent of the liar paradox. Suppose that we suggest the definition

A typical Englishman is one who possesses all the properties possessedby a majority of Englishmen.

It is clear that most Englishmen do not possessall theproperties that most Englishmen possess. Therefore, a typicalEnglishman, according to this definition, should be untypical. Theproblem, according to Russell, is that the word “typical”has been defined by a reference to all properties and has been treatedas itself a property. (It is remarkable that similar problems arisewhen defining the notion ofrandom numbers, cf.Martin-Löf “Notes on constructive mathematics”(1970).) Russell introduced theramified hierarchy in orderto deal with the apparent circularity of such impredicativedefinitions. One should make a distinction between thefirst-order properties, like being Corsican, that do notrefer to the totality of properties, and consider that thesecond-order properties refer only to the totality offirst-order properties. One can then introduce third-orderproperties, that can refer to the totality of second-order property,and so on. This clearly eliminates all circularities connected toimpredicative definitions.

At about the same time, Poincaré carried out a similaranalysis. He stressed the importance of “predicative”classifications, and of not defining elements of a class using aquantification over this class (Poincaré1909). Poincaré used the following example. Assume that we havea collection with elements 0, 1 and an operation + satisfying

Let us say that a property isinductive if it holds of 0 and holds for \(x+1\) if it holds for \(x\).

An impredicative, and potentially “dangerous”, definitionwould be to define an element to be anumber if it satisfiesall inductive properties. It is then easy to show that thisproperty “to be a number” is itself inductive. Indeed, 0is a number since it satisfies all inductive properties, and if \(x\)satisfies all inductive properties then so does \(x+1\). Similarly itis easy to show that \(x+y\) is a number if \(x,y\) arenumbers. Indeed the property \(Q(z)\) that \(x+z\) is a number isinductive: \(Q\)(0) holds since \(x+0=x\) and if \(x+z\) is a numberthen so is \(x+(z+1) = (x+z)+1\). This whole argument however iscircular since the property “to be a number” is notpredicative and should be treated with suspicion.

Instead, one should introduce a ramified hierarchy of properties andnumbers. At the beginning, one has onlyfirst-order inductiveproperties, which do not refer in their definitions to a totality ofproperties, and one defines the numbers of order 1 to be the elementssatisfying all first-order inductive properties. One can next considerthe second-order inductive properties, that can refer to thecollection of first-order properties, and the numbers of order 2, thatare the elements satisfying the inductive properties of order 2. Onecan then similarly consider numbers of order 3, and soon. Poincaré emphasizes the fact that a number of order 2 isa fortiori a number of order 1, and more generally, a numberof order \(n+1\) isa fortiori a number of order \(n\). Wehave thus a sequence of more and more restricted properties: inductiveproperties of order 1, 2, … and a sequence of more and morerestricted collections of objects: numbers of order 1, 2, …Also, the property “to be a number of order \(n\)” isitself an inductive property of order \(n+1\).

It does not seem possible to prove that \(x+y\) is a number of order\(n\) if \(x,y\) are numbers of order \(n\). On the other hand, it ispossible to show that if \(x\) is a number of order \(n+1\), and \(y\)a number of order \(n+1\) then \(x+y\) is a number of order\(n\). Indeed, the property \(P(z)\) that “\(x+z\) is a numberof order \(n\)” is an inductive property of order \(n+1: P\)(0)holds since \(x+0 = x\) is a number of order \(n+1\), and hence oforder \(n\), and if \(P(z)\) holds, that is if \(x+z\) is a number oforder \(n\), then so is \(x+(z+1) = (x+z)+1\), and so \(P(z+1)\)holds. Since \(y\) is a number of order \(n+1\), and \(P(z)\) is aninductive property of order \(n+1, P(y)\) holds and so \(x+y\) isa number of order \(n\). This example illustrates well thecomplexities introduced by the ramified hierarchy.

The complexities are further amplified if one, like Russell as forFrege, defines even basic objects like natural numbers as classes ofclasses. For instance the number 2 is defined as the class of allclasses of individuals having exactly two elements. We again obtainnatural numbers of different orders in the ramified hierarchy.Besides Russell himself, and despite all these complications, Chwistektried to develop arithmetic in a ramified way, and the interest ofsuch an analysis was stressed by Skolem. See Burgess and Hazen 1998for a recent development.

Another mathematical example, often given, of an impredicativedefinition is the definition of least upper bound of a bounded classof real numbers. If we identify a real with the set of rationals thatare less than this real, we see that this least upper bound can bedefined as the union of all elements in this class. Let us identifysubsets of the rationals as predicates. For example, for rationalnumbers \(q, P(q)\) holds iff \(q\) is amember of the subset identified as \(P\). Now, we define thepredicate \(L_C\) (a subset of the rationals)to be the least upper bound of class \(C\) as:

which is impredicative: we have defined a predicate \(L\) by anexistential quantification over all predicates. In the ramifiedhierarchy, if \(C\) is a class of first-order classes ofrationals, then \(L\) will be a second-order class ofrationals. One obtains then notone notion or real numbers,but real numbers of different orders 1, 2, … The least upperbound of a collection of reals of order 1 will then be at least oforder 2 in general.

As we saw earlier, yet another example of an impredicative definitionis given by Leibniz’ definition of equality. For Leibniz, thepredicate “is equal to \(a\)” is true for \(b\)iff \(b\) satisfies all the predicates satisfied by \(a\).

How should one deal with the complications introduced by the ramifiedhierarchy? Russell showed, in the introduction to the second editiontoPrincipia Mathematica, that these complications can be avoided in somecases. He even thought, in Appendix B of the second edition ofPrincipia Mathematica, that the ramified hierarchy of naturalnumbers of order 1,2,… collapses at order 5 for defining the reflexive transitive closure of a relation. However,Gödel later found a problem in his argument, and indeed, it wasshown by Myhill 1974 that this hierarchy actuallydoes notcollapse at any finite level. A similar problem, discussed by Russellin the introduction to the second edition toPrincipia Mathematica arises in the proof of Cantor’s theorem thatthere cannot be any injective functions from the collection of allpredicates to the collection of all objects (the version of Russell’sparadox in Frege’s system that we presented in the introduction). Canthis be done in a ramified hierarchy? Russell doubted that this couldbe done within a ramified hierarchy of predicates and this was indeedconfirmed indeed later (see Chwistek 1926, Fitch 1939 and Heck 1996).

Because of these problems, Russell and Whitehead introduced in thefirst edition ofPrincipia Mathematica the followingreducibility axiom: the hierarchy of predicates, first-order,second-order, etc., collapses at level 1. This means that for anypredicate of any order, there is a predicate of the first-order levelwhich is equivalent to it. In the case of equality for instance, wepostulate a first-order relation “\(a=b\)”which is equivalent to “\(a\) satisfies all properties that\(b\) satisfies”. The motivation for this axiom was purelypragmatic. Without it, all basic mathematical notions, like real ornatural numbers are stratified into different orders. Also, despitethe apparent circularity of impredicative definitions, the axiom ofreducibility does not seem to lead to inconsistencies.

As noticed however first by Chwistek, and later by Ramsey, in thepresence of the axiom of reducibility, there is actually no point inintroducing the ramified hierarchy at all! It is much simpler toaccept impredicative definitions from the start. The simple“extensional” hierarchy of individuals, classes, classesof classes, … is then enough. We get in this way the simplersystems formalised in Gödel 1931 or Church 1940 that werepresented above.

The axiom of reducibility draws attention to the problematic status ofimpredicative definitions. To quote Weyl 1946, the axiom ofreducibility “is a bold, an almost fantastic axiom; there islittle justification for it in the real world in which we live, andnone at all in the evidence on which our mind bases itsconstructions”! So far, no contradictions have been found usingthe reducibility axiom. However, as we shall see below,proof-theoretic investigations confirm the extreme strength of such aprinciple.

The idea of the ramified hierarchy has been extremely important inmathematical logic. Russell considered only the finite iteration ofthe hierarchy: first-order, second-order, etc., but from thebeginning, the possibility of extending the ramification transfinitelywas considered. Poincaré (1909) mentions the work of Koenig inthis direction. For the example above of numbers of different order,he also defines a number to be inductive of order \(\omega\) if it isinductive of all finite orders. He then points out thatx+yis inductive of order \(\omega\) if both \(x\) and \(y\)are. This shows that the introduction of transfinite orders can insome case play the role of the axiom of reducibility. Such transfiniteextension of the ramified hierarchy was analysed further by Gödelwho noticed the key fact that the following form of the reducibilityaxiom is actuallyprovable: when one extends the ramifiedhierarchy of properties over the natural numbers into the transfinitethis hierarchy collapses at level \(\omega_1\), the leastuncountable ordinal (Gödel 1995, and Prawitz1970). Furthermore, while at all levels \(\lt \omega_1\), thecollection of predicates is countable, the collection of predicates atlevel \(\omega_1\) is of cardinality \(\omega_1\). Thisfact was a strong motivation behind Gödel’s model ofconstructible sets. In this model the collection of all subsets of theset of natural numbers (represented by predicates) is of cardinality\(\omega_1\) and is similar to the ramified hierarchy. Thismodel satisfies in this way the Continuum Hypothesis, and gives arelative consistency proof of this axiom. (The motivation ofGödel was originally only to build a model where the collectionof all subsets of natural numbers is well-ordered.)

The ramified hierarchy has been also the source of much work in prooftheory. After the discovery by Gentzen that the consistency ofArithmetic could be proved by transfinite induction (over decidablepredicates) along the ordinal \(\varepsilon_0\), the natural questionwas to find the corresponding ordinal for the different levels of theramified hierarchy. Schütte (1960) found that for the first levelof the ramified hierarchy, that is if we extend arithmetic byquantifying only over first-order properties, we get a system ofordinal strength \(\varepsilon_{\varepsilon_0}\). For the second levelwe get the ordinal strength \(\varepsilon_{\varepsilon_{\varepsilon_0}}\), etc. We recall that \(\varepsilon_{\alpha}\)denotes the \(\alpha\)-th \(\varepsilon\)-ordinal number, an\(\varepsilon\)-ordinal number being an ordinal \(\beta\) such that\(\omega^{\beta} = \beta\), see Schütte (1960).

Gödel stressed the fact that his approach to the problem of thecontinuum hypothesis was not constructive, since it needs theuncountable ordinal \(\omega_1\), and it was natural to studythe ramified hierarchy along constructive ordinals. After preliminaryworks of Lorenzen and Wang, Schütte analysed what happens if weproceed in the following more constructive way. Since arithmetic hasfor ordinal strength \(\varepsilon_0\) we consider first theiteration of the ramified hierarchy up to \(\varepsilon_0\).Schütte computed the ordinal strength of the resulting system andfound an ordinal strength \(u(1)\gt \varepsilon_0\). Weiterate then ramified hierarchy up to this ordinal \(u(1)\) andget a system of ordinal strength \(u(2)\gt u(1)\),etc. Each \(u(k)\) can be computed in terms of theso-called Veblen hierarchy: \(u(k+1)\) is\(\phi_{u(k)}(0)\). The limit of this processgives an ordinal called \(\Gamma_0\): if we iterate theramified hierarchy up to the ordinal \(\Gamma_0\) we get asystem of ordinal strength \(\Gamma_0\). Such an ordinal wasobtained independently about the same time by S. Feferman. It has beenclaimed that \(\Gamma_0\) plays for predicative systems a rolesimilar to \(\varepsilon_0\) for Arithmetic. Recentproof-theoretical works however are concerned with systems havingbigger proof-theoretical ordinals that can be considered predicative(see for instance Palmgren 1995).

Besides these proof theoretic investigations related to the ramifiedhierarchy, much work has been devoted in proof theory to analysing theconsistency of the axiom of reducibility, or, equivalently, theconsistency of impredicative definitions. Following Gentzen’sanalysis of the cut-elimination property in the sequent calculus,Takeuti found an elegant sequent formulation of simple type theory(without ramification) and made the bold conjecture thatcut-elimination should hold for this system. This conjecture seemed atfirst extremely dubious given the circularity of impredicativequantification, which is well reflected in this formalism. The rulefor quantifications is indeed

where \(T\) isany term predicate, which may itselfinvolve a quantification over all predicates. Thus the formula\(A[X:=T]\) may be itself much more complexthan the formula \(A(X)\).

One early result is that cut-elimination for Takeuti’simpredicative system implies in a finitary way the consistency ofsecond-order Arithmetic. (One shows that this implies the consistencyof a suitable form of infinity axiom, see Andrews 2002.) Followingwork by Schütte (1960b), it was later shown by W. Tait andD. Prawitz that indeed the cut-elimination property holds (the proofof this has to use a stronger proof theoretic principle, as it shouldbe according to the incompleteness theorem.)

What is important here is that these studies have revealed the extremepower of impredicative quantification or, equivalently, the extremepower of the axiom of reducibility. This confirms in some way theintuitions of Poincaré and Russell. The proof-theoreticstrength of second-order Arithmetic is way above all ramifiedextensions of Arithmetic considered by Schütte. On the otherhand, despite the circularity of impredicative definitions, which ismade so explicit in Takeuti’s calculus, no paradoxes have been foundyet in second-order Arithmetic.

Another research direction in proof theory has been to understand howmuch of impredicative quantification can be explained from principlesthat are available in intuitionistic mathematics. The strongest suchprinciples are strong forms of inductive definitions. With suchprinciples, one can explain a limited form of an impredicativequantification, called \(\Pi_{1}^1\)-comprehension,where one uses only one level of impredicative quantification overpredicates. Interestingly, almost all known uses of impredicativequantifications: Leibniz equality, least upper bound, etc., can bedone with \(\Pi_{1}^1\)-comprehension. This reductionof \(\Pi_{1}^1\)-comprehension was first achieved byTakeuti in a quite indirect way, and was later simplified by Buchholzand Schütte using the so-called \(\Omega\)-rule. It can be seen asa constructive explanation of some restricted, but nontrivial, uses ofimpredicative definitions.

4. Type Theory/Set Theory

Type theory can be used as a foundation for mathematics, and indeed,it was presented as such by Russell in his 1908 paper, which appearedthe same year as Zermelo’s paper, presenting set theory as a foundationfor mathematics.

It is clear intuitively how we can explain type theory in set theory:a type is simply interpreted as a set, and function types \(A\rightarrow B\) can be explained using the set theoretic notion offunction (as a functional relation, i.e. a set of pairs ofelements). The type \(A \rightarrow o\) corresponds to the powersetoperation.

The other direction is more interesting. How can we explain the notionof sets in terms of types? There is an elegant solution, due toA. Miquel, which complements previous works by P. Aczel (1978) andwhich has also the advantage of explaining non necessarilywell-founded sets a la Finsler. One simply interprets asetas apointed graph (where the arrow in the graph representsthe membership relation). This is very conveniently represented intype theory, a pointed graph being simply given by a type A and a pairof elements

We can then define in type theory when two such sets \(A, a, R\) and\(B, b, S\) are equal: this is the case iff there is a bisimulation\(T\) between \(A\) and \(B\) such that \(Tab\) holds. A bisimulationis a relation

such that whenever \(Txy\) and \(Rxu\) hold, there exists \(v\) suchthat \(Tuv\) and \(Syv\) hold, and whenever \(Txy\) and \(Ryv\) hold,there exists \(u\) such that \(Tuv\) and \(Rxu\) hold. We can thendefine the membership relation: the set represented \(B, b, S\) is amember of the set represented by \(A, a, R\) iff there exists \(a_1\)such that \(Ra_1a\) and \(A, a_1, R\) and \(B, b, S\) arebisimilar.

It can then be checked that all the usual axioms of set theoryextensionality, power set, union, comprehension over bounded formulae(and even antifoundation, so that the membership relation does notneed to be well-founded) hold in this simple model. (A bounded formulais a formula where all quantifications are of the form \(\forall x \ina\ldots\) or \(\exists x \in a\ldots\)). In this way it can been shownthat Church’s simple type theory is equiconsistent with thebounded version of Zermelo’s set theory.

5. Type Theory/Category Theory

There are deep connections between type theory and category theory.We limit ourselves to presenting two applications of type theory tocategory theory: the constructions of the free cartesian closedcategory and of the free topos (see the entry on category theory for anexplanation of “cartesian closed” and “topos”).

For building the free cartesian closed category, we extend simple typetheory with the type 1 (unit type) and the product type \(A \timesB\), for \(A, B\) types. The terms are extended by adding pairingoperations and projections and a special element of type 1. As inLambek and Scott 1986, one can then define a notion oftypedconversions between terms, and show that this relation isdecidable. One can then show (Lambek and Scott 1986) that the categorywith types as objects and as morphisms from \(A\) to \(B\) the set ofclosed terms of type \(A \rightarrow B\) (with conversion as equality)is the free cartesian closed category. This can be used to show thatequality between arrows in this category is decidable.

The theory of types of Church can also be used to build the freetopos. For this we take as objects pairs \(A,E\) with \(A\) type and\(E\) a partial equivalence relation, that is a closed term \(E:A\rightarrow A \rightarrow o\) which is symmetric and transitive. Wetake as morphisms between \(A, E\) and \(B, F\) the relations\(R:A\rightarrow B\rightarrow o\) that arefunctional that is such that for any \(a:A\) satisfying \(E aa\) there exists one, and only one (modulo \(F)\) element \(b\) of\(B\) such that \(F b b\) and \(R a b\). For the subobject classifierwe take the pair \(o, E\) with \(E:o\rightarrow o\rightarrow o\)defined as

One can then show that this category forms a topos, indeed the freetopos.

It should be noted that the type theory in Lambek and Scott 1986uses a variation of type theory, introduced by Henkin and refined byP. Andrews (2002) which is to have an extensional equality as theonly logical connective, i.e. a polymorphic constant

and to define all logical connectives from this connective andconstants \(T, F : o\). For instance, one defines

The equality at type \(o\) is logical equivalence.

One advantage of the intensional formulation is that it allows for adirect notation of proofs based on \(\lambda\)-calculus (Martin-Löf1971 and Coquand 1986).

6. Extensions of Type System, Polymorphism, Paradoxes

We have seen the analogy between the operation A \(\rightarrow\) A \(\rightarrow\) o ontypes and the powerset operation on sets. In set theory, the powersetoperation can be iterated transfinitely along the cumulativehierarchy. It is then natural to look for analogous transfiniteversions of type theory.

One such extension of Church’s simple type theory is obtained byadding universes (Martin-Löf 1970). Adding a universe is areflection process: we add a type \(U\) whose objectsare the types considered so far. For Church’s simple type theory wewill have

and, furthermore, \(A\) is a type if \(A:U\). We can then considertypes such as

and functions such as

The function id takes as argument a “small” type \(A:U\)and an element \(x\) of type \(A\), and outputs an element of type\(A\). More generally if \(T(A)\) is a type under the assumption\(A:U\), one can form the dependent type

That \(M\) is of this type means that \(M A:T(A)\) whenever\(A:U\). We get in this way extensions of type theory whose strengthis similar to the one of Zermelo’s set theory (Miquel2001). More powerful form of universes are considered in (Palmgren1998). Miquel (2003) presents a version of type theory of strengthequivalent to the one of Zermelo-Fraenkel.

One very strong form of universe is obtained by adding the axiom\(U:U\). This was suggested by P. Martin-Löf in1970. J.Y. Girard showed that the resulting type theory isinconsistent as a logical system (Girard 1972). Though it seems at firstthat one could directly reproduce Russell’s paradox using a set of allsets, such a direct paradox is actually not possible due to thedifference between sets and types. Indeed the derivation of acontradiction in such a system is subtle and has been rather indirect(though, as noticed in Miquel 2001, it can now be reduced toRussell’s paradox by representing sets as pointed graphs). J.Y. Girardfirst obtained his paradox for a weaker system. This paradox wasrefined later (Coquand 1994 and Hurkens 1995). (The notion of puretype system, introduced in Barendregt 1992, is convenient forgetting a sharp formulation of these paradoxes.) Instead of the axiom\(U:U\) one assumes only

if \(T(A) : U [A:U]\). Notice the circularity, indeed of the same kindas the one that is rejected by the ramified hierarchy: we define anelement of type \(U\) by quantifying over all elements of \(U\). Forinstance the type

will be the type of the polymorphic identity function. Despite thiscircularity, J.Y. Girard was able to show normalisation for typesystems with this form of polymorphism. However, the extension ofChurch’s simple type theory with polymorphism is inconsistent as alogical system, i.e. all propositions (terms of type o) areprovable.

J.Y. Girard’s motivation for considering a type system withpolymorphism was to extend Gödel’s Dialectica (Gödel 1958)interpretation to second-order arithmetic. He proved normalisationusing the reducibility method, that had been introduced by Tait (1967)while analysing Gödel 1958. It is quite remarkable that thecircularity inherent in impredicativity does not result innon-normalisable terms. (Girard’s argument was then used to show thatcut-elimination terminates in Takeuti’s sequent calculus presentedabove.) A similar system was introduced independently by J. Reynolds(1974) while analysing the notion of polymorphism in computerscience.

Martin-Löf’s introduction of a type of all types comes from theidentification of the concept of propositions and types, suggested bythe work of Curry and Howard. It is worth recalling here his threemotivating points:

1. Russell’s definition of types as ranges of significance ofpropositional functions
2. the fact that one needs to quantify over all propositions(impredicativity of simple type theory)
3. identification of proposition and types

Given (1) and (2) we should have a type of propositions (as in simpletype theory), and given (3) this should also be the type of alltypes. Girard’s paradox shows that one cannot have (1),(2) and (3)simultaneously. Martin-Löf’s choice was to take away (2),restricting type theory to be predicative (and, indeed, the notion ofuniverse appeared first in type theory as a predicative version of thetype of all types). The alternative choice of taking away (3) isdiscussed in Coquand 1986.

7. Univalent Foundations

The connections between type theory, set theory and category theorygets a new light through the work on Univalent Foundations (Voevodsky2015) and theAxiom ofUnivalence. This involves in an essential way the extension oftype theory described in the previous section, in particular dependenttypes, the view of propositions as types, and the notion of universeof types. These development are also relevant for discussing thenotion of structure, the importance of which was for instanceemphasized in Russell 1959.

Martin-Löf 1975 [1973] introduced a new basic type\(\mathbf{Id}_A (a,b)\), if \(a\) and \(b\) are in the type \(A\),which can be thought as the type of equality proofs of the element\(a\) and \(b\). An important feature of this new type is that it canbe iterated, so that we can consider the type\(\mathbf{Id}_{\mathbf{Id}_A (a,b)}(p,q)\) if \(p\) and \(q\) are oftype \(\mathbf{Id}_A (a,b)\). If we think of a type as a special kindof set, it is natural to conjecture that such a type of equalityproofs is always inhabited for any two equality proofs \(p\) and\(q\). Indeed, intuitively, there seems to be at most an equalityproof between two elements \(a\) and \(b\). Surprisingly, Hofmann andStreicher 1996 designed a model of dependent type theory where this isnot valid, that is a model where they can be different proofs that twoelements are equal. In this model, a type is interpreted byagroupoid and the type \(\mathbf{Id}_A (a,b)\) by the set ofisomorphisms between \(a\) and \(b\), set which may have more than oneelement. The existence of this model has the consequence that itcannot be proved in general in type theory that an equality type hasat most one element. This groupoid interpretation has been generalizedin the following way, which gives an intuitive interpretation of theidentity type. Atype is interpreted by atopologicalspace, up to homotopy, and a type \(\mathbf{Id}_A (a,b)\) isinterpreted by the type ofpaths connecting \(a\) and\(b\). (See Awodey et al. 2013 and [HoTT 2013, Other InternetResources].)

Voevodsky 2015 introduced the following stratification of types. (Thisstratification was motivated in part by this interpretation of a typeas a topological space, but can be understood directly withoutreference to this interpretation.) We say that a type \(A\) isaproposition if we have \(\mathbf{Id}_A (a,b)\) for anyelement \(a\) and \(b\) of \(A\) (this means that the type \(A\) hasat most one element). We say that a type \(A\) is aset ifthe type \(\mathbf{Id}_A (a,b)\) is a proposition for any element\(a\) and \(b\) of \(A\). We say that a type \(A\) isagroupoid if the type \(\mathbf{Id}_A (a,b)\) is a set forany element \(a\) and \(b\) of \(A\). The justification of thisterminology is that it can be shown, only using the rules of typetheory, that any such type can indeed be seen as a groupoid in theusual categorical sense, where the objects are the elements of thistype, the set of morphisms between \(a\) and \(b\) being representedby theset \(\mathbf{Id}_A (a,b)\). The composition is theproof of transitivity of equality, and the identity morphism is theproof of reflexivity of equality. The fact that each morphism has aninverse corresponds to the fact that identity is a symmetricrelation. This stratification can then be extended and we can definewhen a type is a 2-groupoid, 3-groupoid and so on. In this view,type theory appears as a vast generalization ofsettheory, since a set is a particular kind of type.

Voevodsky 2015 introduces also a notion ofequivalence between types, notion which generalizes in anuniform way the notions oflogical equivalence betweenpropositions,bijection between sets,categoricalequivalence between groupoids, and so on. We say that a map\(f:A\rightarrow B\) is an equivalence if, for any element \(b\) in\(B\) the type of pairs \(a,p\) where \(p\) is of type \(\mathbf{Id}_B(f a,b)\), is a proposition and is inhabited. This expresses in astrong way that an element in \(B\) is the image of exactly oneelement in \(A\), and if \(A\) and \(B\) are sets, we recover theusual notion of bijection between sets. (In general if\(f:A\rightarrow B\) is an equivalence, then we have a map\(B\rightarrow A\), which can be thought of as the inverse of \(f\).)It can be shown for instance that the identity map is always anequivalence. Let \(\text{Equiv}(A,B)\) be the type of pairs \(f,p\) where\(f:A\rightarrow B\) and \(p\) is a proof that \(f\) is anequivalence. Using the fact that the identity map is an equivalence wehave an element of \(\text{Equiv}(A,A)\) for any type \(A\). This impliesthat we have a map

and theAxiom of Univalence states that this map is anequivalence. In particular, we have the implication

and so if there is an equivalence between two small types thenthese types are equal.

This Axiom can be seen as a strong form of the extensionalityprinciple. It indeed generalizes the Axiom ofpropositionalextensionality mentioned by Church 1940, which states that twologically equivalent propositions are equal. Surprisingly, it alsoimplies the Axiom offunction extensionality, Axiom 10 inChurch 1940, which states that two pointwise equal functions are equal(Voevodsky 2015). It also directly impliesthat two isomorphic sets are equal, that two categorically equivalentgroupoids are equal, and so one.

This can be used to give a formulation of the notionoftransport of structures (Bourbaki 1957) alongequivalences. For instance, let \(M A\) be the type of monoidstructures on the set \(A\): this is the type of tuples \(m, e, p\)where \(m\) is a binary operation on \(A\) and \(e\) an element of\(A\) and \(p\) a proof that these elements satisfy the usual monoidlaws. The rule of substitution of equal by equal takes the form

If there is a bijection between \(A\) and \(B\) they areequal by the Axiom of Univalence, and we can use this implication totransport any monoid structure of \(A\) in a monoid structureof \(B\).

Both Russell 1919 and Russell 1959 stress the importance of thenotion of structure. For instance, in Chapter VI of Russell 1919, itis noticed that two similar relations essentially have the sameproperties, and hence have the same “structure”. (Thenotion of “similarity” of relations was introduced inRussell 1901.) We can also use this framework to refineRussell’s discussions on the notion of structure. For instance,letMonoid be the type of pairs \(A,p\) where \(p\)is an element of \(M A\). Two such pairs \(A,p\) and \(B,q\) areisomorphic if there exists a bijection \(f\) from \(A\) to \(B\) suchthat \(q\) is equal to the transport of structure of \(p\) along\(f\). A consequence of the Axiom of Univalence is that two isomorphicelements of the typeMonoid are equal, and henceshares the same properties. Notice that such a general transport ofproperties isnot possible when structures are formulated ina set theoretic framework. Indeed, in a set theoretic framework, it ispossible to formulate properties using the membership relations, forinstance the property that the carrier set of the structure containsthe natural number \(0\), property that is not preserved in general byisomorphisms. Intuitively, the set theoretical description of astructure is not abstract enough since we can talk about the way thisstructure is built up. This difference between set theory and typetheory is yet another illustration of the characterization byJ.Reynolds 1983 of a type structure as a “syntactical disciplinefor enforcing level of abstraction”.

Bibliography

• Aczel, P., 1978, “The type theoretic interpretation ofconstructive set theory”,Logic Colloquium ’77,Amsterdam: North-Holland, 55–66.
• Andrews, P., 2002,An introduction to mathematical logic andtype theory: to truth through proof (Applied Logic Series: Volume27), Dordrecht: Kluwer Academic Publishers, second edition.
• Awodey, S. and Carus, A.W., 2001, “Carnap, completeness andcategoricity: the Gabelbarkeitssatz of 1928”,Erkenntnis, 54: 145–171.
• ––– and Pelayo, A., Warren, M. 2013, “TheAxiom of Univalence in Homotopy Type Theory”,Notices of theAmerican Mathematical Society, 60(9): 1157–1164.
• Barendregt, H., 1997, “The impact of the lambda calculus inlogic and computer science”,Bulletin of SymbolicLogic, 3(2): 181–215.
• –––, 1992,Lambda calculi withtypes. Handbook of logic in computer science, Volume 2, Oxford,New York: Oxford University Press, 117–309.
• Bell, J.L., 2012, “Types, Sets and Categories”, inAkihiro KanamoryHandbook of the History of Logic. Volume 6: Setsand Extensions in the Twentieth Century, Amsterdam: North Holland.
• Bourbaki, N., 1958,Théorie des Ensembles, 3rdedition, Paris: Hermann.
• de Bruijn, N. G., 1980, “A survey of the projectAUTOMATH”, inTo H. B. Curry: essays on combinatory logic,lambda calculus and formalism, London-New York: Academic Press, 579–606.
• Burgess J. P. and Hazen A. P., 1998, “Predicative Logic andFormal Arithmetic Source,”Notre Dame J. Formal Logic,39(1): 1–17.
• Buchholz, W. and K. Schütte, 1988,Proof theory ofimpredicative subsystems of analysis (Studies in Proof Theory:Monograph 2), Naples: Bibliopolis.
• Church, A., 1940, “A formulation of the simple theory oftypes,”Journal of Symbolic Logic, 5: 56–68
• –––, 1984, “Russell’s theory of identityof propositions,”Philosophia Naturalis, 21:513–522
• Chwistek, L., 1926, “Ueber die Hypothesen derMengelehre,”Mathematische Zeitschrift, 25:439–473
• –––, 1948,The Limits of Science: Outline of Logicand of the Methodology of the Exact Sciences, London: Routledgeand Kegan Paul.
• Coquand, T., 1986, “An analysis of Girard’s paradox,”Proceedings of the IEEE Symposium on Logic in ComputerScience, 227–236.
• –––, 1994, “A new paradox in type theory,”Stud. Logic Found. Math. (Volume 134), Amsterdam:North-Holland, 555–570.
• du Bois-Reymond, P., 1875, “Ueber asymptotische Werthe,infintaere Appproximationen und infitaere Aufloesung vonGleichungen,”Mathematische Annalen, 8:363–414.
• Feferman, S., 1964, “Systems of predicative analysis,”Journal of Symbolic Logic, 29: 1–30.
• Ferreira, F. and Wehmeier, K., 2002, “On the consistency ofthe Delta-1-1-CA fragment of Frege’s Grundgesetze,”Journalof Philosophic Logic, 31: 301–311.
• Fitch, F. B., 1964, “The hypothesis that infinite classesare similar,”Journal of Symbolic Logic, 4:159–162.
• Girard, J.Y., 1972,Interpretation fonctionelle eteleimination des coupures dans l’arithmetique d’ordre superieure,These d’Etat, Université Paris 7.
• Goldfarb, Warren, 2005. “On Godel’s way in: The influence ofRudolf Carnap.”Bulletin of Symbolic Logic 11(2):185–193.
• Gödel, K., 1995,Collected Works Volume III, UnpublishedEssays and Lectures, Oxford: Oxford University Press, 1995.
• –––, 1931, “Über formaluntentscheidbare Sätze der Principia Mathematica und verwandterSysteme I,”Monatshefte fü Mathematik und Physik,38: 173–198.
• –––, 1944, “Russell’s mathematicallogic,” inThe philosophy of Bertrand Russell,P. A. Schilpp (ed.), Evanston: Northwestern University Press,123–153.
• –––, 1958, “Über eine bisher noch nichtbenützte Erweiterung des finiten Standpunktes,”,Dialectica, 12: 280–287.
• Heck, R., Jr., 1996, “The consistency of predicativefragments of Frege’s Grundgesetze der Arithmetik,”Historyand Philosophy of Logic, 17(4): 209–220.
• van Heijenoort, 1967,From Frege to Gödel. A source bookin mathematical logic 1879–1931, Cambridge, MA: HarvardUniversity Press.
• Hindley, R., 1997,Basic Simple Type Theory, Cambridge:Cambridge University Press.
• Hodges, W., 2008, “Tarski on Padoa’s Method: a test case forunderstanding logicians of other traditions”, inLogic,Navya-Nyāya and Applications: Homage to Bimal Krishna Matilal,Mihir K. Chakraborti et al. (eds.), London: College Publications,pp. 155–169
• Hofmann, M. and Streicher, Th. 1996, “The Groupoidinterpretation of Type Theory,” inTwenty-five years ofconstructive type theory (Oxford Logic Guides: Volume 36),Oxford, New York: Oxford University Press, 83–111.
• Howard, W. A., 1980, “The formulae-as-types notion ofconstruction,” inTo H. B. Curry: essays on combinatorylogic, lambda calculus and formalism, London, New York: AcademicPress, 480–490.
• Hurkens, A. J. C., 1995, “A simplification of Girard’sparadox. Typed lambda calculi and applications,” inLectureNotes in Computer Science (Volume 902), Berlin: Springer:266–278.
• Lambek, J., 1980. “From \(\lambda\)-calculus to CartesianClosed Categories” inTo H.B. Curry: Essays on CombinatoryLogic, \(\lambda\)-calculus and Formalism, J. Seldin and J. Hindley(eds.), London, New York: Academic Press. pp. 375–402.
• Lambek, J. and Scott, P. J., 1986,Introduction to higherorder categorical logic (Cambridge Studies in AdvancedMathematics: Volume 7), Cambridge: Cambridge University Press;reprinted 1988.
• Lawvere, F. W. and Rosebrugh, R., 2003,Sets formathematics, Cambridge: Cambridge University Press.
• Martin-Löf, P., 1970,Notes on constructivemathematics, Stockholm: Almqvist & Wiksell.
• –––, 1971,A Theory of Types, Technical Report 71–3, Stockholm: Stockholm University.
• –––, 1998, “An intuitionistic theory oftypes,” inTwenty-five years of constructive typetheory (Oxford Logic Guides: Volume 36), Oxford, New York: OxfordUniversity Press, 127–172.
• –––, 1975 [1973], “An intuitionistictheory of types: Predicative Part,” inLogic Colloquium’73 (Proceedings of the Logic Colloquium, Bristol 1973) (Studiesin Logic and the Foundations of Mathematics: Volume 80), H.E. Rose andJ.C. Shepherdson (eds.), Amsterdam: North-Holland, 73–118.
• Myhill, J., 1974, “The Undefinability of the Set of NaturalNumbers in the Ramified Principia”, inBertrand Russell’sPhilosophy, G. Nakhnikian (ed.), London: Duckworth,19–27.
• Miquel, A., 2001,Le Calcul des Constructions implicite:syntaxe et sémantique, Thèse dedoctorat, Université Paris 7.
• –––, 2003, “A strongly normalising Curry-Howardcorrespondence for IZF set theory,” inComputer scienceLogic (Lecture Notes in Computer Science, 2803), Berlin: Springer:441–454.
• Oppenheimer, P. and E. Zalta, 2011, “Relations Versus Functionsat the Foundations of Logic: Type-Theoretic Considerations”,Journal of Logic and Computation, 21: 351–374.
• Palmgren, Erik, 1998, “On universes in type theory,”inTwenty-five years of Constructive Type Theory (OxfordLogic Guides: Volume 36), Oxford, New York: Oxford University Press,191–204.
• Poincaré, 1909, “H. La logique de l’infini”Revue de metaphysique et de morale, 17: 461–482.
• Prawitz, D., 1967, “Completeness and Hauptsatz for secondorder logic”,Theoria, 33: 246–258.
• –––, 1970, “On the proof theory ofmathematical analysis,” inLogic and value (Essaysdedicated to Thorild Dahlquist on his fiftieth birthday), FilosofiskaStudier (Filosof. Föreningen och Filosof. Inst.), No. 9, Uppsala:Uppsala University, 169–180.
• Quine, W., 1940, “Review of Church ‘A formulation ofthe simple theory of types’,”Journal of Symbolic Logic,5: 114.
• Ramsey, F.P., 1926, “The foundations of mathematics,”Proceedings of the London Mathematical Society, s2–25 (1),338–384.
• Russell, B., 1901, “Sur la logique des relations avec desapplications a la théorie des séries”,Revue deMathématique, 7: 115–136, 137–148.
• –––, 1903,The Principles of Mathematics, Cambridge: Cambridge University Press.
• –––, 1908, “Mathematical logic as based onthe theory of types,”American Journal of Mathematics,30: 222–262.
• –––, 1919,Introduction to MathematicalPhilosophy, London: George Allen and Unwin.
• –––, 1959,My philosophicaldevelopment, London, New York: Routledge.
• Russell, B. and Whitehead, A., 1910, 1912, 1913,PrincipiaMathematica (3 volumes), Cambridge: Cambidge UniversityPress.
• Reynolds, J., 1974, “Towards a theory of typestructure,” inProgramming Symposium (Lecture Notes inComputer Science: Volume 19), Berlin: Springer, 408–425.
• –––, 1983, “Types, Abstraction andParametric Polymorphism,”Proceedings of the IFIP 9th WorldComputer Congress, Paris, 513–523.
• –––, 1984, “Polymorphism is notset-theoretic. Semantics of data types,”Lecture Notes inComputer Science (Volume 173), Berlin: Springer,145–156.
• –––, 1985, “Three approaches to typestructure. Mathematical foundations of software development,”inLecture Notes in Computer Science (Volume 185), Berlin:Springer, 97–138.
• Schiemer, G. and Reck, E.H., 2013, “Logic in the 1930s: TypeTheory and Model Theory,”The Bulletin of SymbolicLogic, 19(4): 433–472.
• Schütte, K., 1960,Beweistheorie, Berlin:Springer-Verlag.
• –––, 1960b, “Syntactical and SemanticalProperties of Simple Type Theory,”Journal of SymbolicLogic, 25: 305–326.
• Scott, D., 1993 “A type-theoretic alternative to ISWIM,CUCH, OWHY,”Theoretical Computer Science, 121:411–440.
• Skolem, T., 1970,Selected works in logic, Jens ErikFenstad (ed.), Oslo: Universitetsforlaget.
• Tait, W. W., 1967, “Intensional interpretations offunctionals of finite type,”Journal of Symbolic Logic,32 (2): 198–212.
• Takeuti, G., 1955 “On the fundamental conjecture of GLC:I”,Journal of the Mathematical Society of Japan, 7:249–275.
• –––, 1967, “Consistency proofs ofsubsystems of classical analysis,”The Annals ofMathematics (Second Series), 86 (2): 299–348.
• Tarski, A., 1931, “Sur les ensembles definissables denombres reels I,”Fundamenta Mathematicae, 17:210–239.
• Urquhart, A., 2003, “The Theory of Types,” inThe Cambridge Companion to Bertrand Russell, NicholasGriffin (ed.), Cambridge: Cambridge University Press.
• Voevodsky, V., 2015, “An experimental library of formalizedmathematics based on univalent foundations,”Mathematical Structures in Computer Science, 25: 1278–1294,available online.
• Wiener, N., 1914, “A simplification of the logic ofrelations,”Proceedings of the Cambridge PhilosophicalSociety, 17: 387–390.
• Weyl, H., 1946, “Mathematics and Logic,”AmericanMathematical Monthly, 53: 2–13.
• Zermelo, E., 1908, “Untersuchungen über die Grundlagender Mengenlehre I,”Mathematische Annalen, 65:261–281.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

• Kubota, K., 2018, “Foundations of Mathematics. Genealogy and Overview,” manuscript, draft of March 27, 2018.
• [HoTT 2013],Homotopy TypeTheory: Univalent Foundations of Mathematics, Institute for Advanced Study.

Related Entries

Russell, Bertrand |category theory |Frege, Gottlob |Frege, Gottlob: theorem and foundations for arithmetic |logic: paraconsistent |mathematics: inconsistent | peano |Principia Mathematica |type theory: Church’s type theory |type theory: intuitionistic