Girard's paradox

Counterexample

System U is the pure type system with sorts $*$, $\square$ and $\triangle$, axioms $* : \square$ and $\square : \triangle$, and rules $(*, *)$, $(\square, *)$, $(\square, \square)$, $(\triangle, *)$ and $(\triangle, \square)$. It extends the higher-order form of System F by allowing quantification over all kinds, such as $\forall \kappa{:}\square.\, \dots$. Girard's paradox is the construction, in System U, of a closed term of type $\bot = \forall \alpha{:}{*}.\, \alpha$. Applying this term to any type $\tau$ of sort $*$ gives a closed term of $\tau$. So every proposition has a proof, and System U is inconsistent as a logic. It follows that System U does not have the normalization property. Indeed, a closed normal term of type $\forall \alpha{:}{*}.\, \alpha$ would have the form $\lambda \alpha{:}{*}.\, t$. Here $t$ would be a normal term of type $\alpha$ whose only free variable is $\alpha$, and no such $t$ exists.