The Computational Behaviour of Girard's Paradox

Abstract

In their paper "Type" Is Not a Type, Meyer and Reinhold argued that serious pathologies can result when a type of all types is added to a programing language with dependent types. Central to their argument is the claim that by following the proof of Girard's paradox it is possible to construct in their calculus $\lambda^{\tau \tau}$ a term having a fixed-point property. Because of the tremendous amount of formal detail involved, they were unable to establish this claim. We have made use of the Nuprl proof development system in constructing a formal proof of Girard's paradox and analysing the resulting term. We can show that the term does not have the desired fixed-point property, but does have a weaker form of it that is sufficient to establish some of the results of Meyer and Reinhold. We believe that the method used here is in itself of some interest, representing a new kind of application of a computer to a problem in symbolic logic.