# No Naive Set Theoretic Models of Polymorphic Lambda Calculus?

there are no naive set-theoretic models of polymorphic lambda calculus

In the naive set-theoretic model types are sets and functions are set-theoretic functions which seems reasonable. So why does he say there are no naive set-theoretic models of polymorphic lambda calculus?

• OK, I just stumbled on this paper: hal.inria.fr/inria-00076261/document. I'm gonna have to plough through it.
– M.K.
Jan 7 '16 at 21:57
• That paper by Reynolds is indeed the right paper to read! Omitting a lot of details it sums up to: consider data T = K ((T -> Bool) -> Bool). Then, T and ((T->Bool)->Bool) are isomorphic. If they have a set model where -> denotes the function space (as a set), the latter has a higher cardinality, so it can't be isomorphic to T. So, in a model, we need to interpret -> differently -- e.g. as the space of continuous functions.
– chi
Jan 7 '16 at 23:59
• I answered too quickly and answered the wrong question. Sorry about that. The reason for polymorphic lambda calculus not having a model in naive set theory is apparently rather different than the one for untyped lambda calculus.
– Levi Pearson
Jan 8 '16 at 9:54

The standard reference you are looking for is indeed Reynold's Polymorphism is not Set Theoretic. While it is quite obvious that you cannot form, e.g. the product $\Pi_{S\in\mathrm{Set}}S$ over all sets using the usual set theoretic product, it's a legitimate, and non-trivial question whether there is some weaker notion of product that would work, while preserving the usual binary product $\times$ and function space $\rightarrow$.
This turns out to not be possible either, since on one hand, it is rather easy to build a type $\bf 2$ such that the interpretation has at least 2 elements, and show that the interpretation of $T=\Pi_X(X\rightarrow {\bf 2})\rightarrow{\bf 2}$ is isomorphic to $(T\rightarrow {\bf 2})\rightarrow {\bf 2}$, which is not possible for the usual interpretation of $\rightarrow$ by the usual cantor paradox. In this sense it is somewhat similar to the proof for the untyped calculus.