(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.