(In)consistency of extensions of higher order logic and type theory

It is well-known, due to the work of Girard and Coquand, that adding polymorphic domains to higher order logic, HOL, or its type theoretic variant ¿HOL, renders the logic inconsistent. This is known as Girard’s paradox, see [4]. But there is also another presentation of higher order logic, in its type theoretic variant called ¿PRED¿, to which polymorphic domains can be added safely, Both ¿HOL and ¿PRED¿ are well-known type systems and in this paper we study why ¿HOL with polymorphic domains is inconsistent and why nd ¿PRED¿ with polymorphic domains remains consistent. We do this by describing a simple model for the latter and we show why this can not be a model of the first