A simplification of Girard's paradox
edited by: Mariangiola Dezani-Ciancaglini, Gordon Plotkin
In 1972 J.-Y. Girard showed that the Burali-Forti paradox can be formalised in the type system U. In 1991 Th. Coquand formalised another paradox in U–. The corresponding proof terms (that have no normal form) are large. We present a shorter term of type in the Pure Type System U– and analyse its reduction behaviour. The idea is to construct a universe U and two functions such that a certain equality holds. Using this equality, we prove and disprove that a certain object in U is well-founded.