[Prev][Next][Index][Thread]

HOL and ML-Polymorphism

Coquand's 1986 paper `An analysis of Girard's paradox' contains the 
claim that the combination of Church-style higher order logic and 
ML-polymorphism is inconsistent because one can express the Burali-Forti 
paradox. Now, e.g., Isabelle/HOL does explicitly feature ML-polymorphism 
(and, of course, higher order logic), and its type checker eats terms
like "twice twice", where twice:: ('a => 'a) => ('a => 'a). This 
prompted us to risk a closer peek:

-- The derivation of the Burali-Forti paradox in the cited paper appears 
to be based on a type error in the sense that the two formulae that, due 
to the omission of explicit types, seem to contradict each other are in 
fact differently typed and hence not contradictory at all.

-- It seems that ML-polymorphism (in a *logic*) could be coded away by 
just replacing each polymorphic operator or axiom by infinitely many 
instances, one for each (proper) type, so that it's consistency would 
follow from that of the surrounding logic.


Are we missing something here? If not -- can anybody point us to related 
references?

Greetings,


Lutz Schröder and Till Mossakowski



-- 
-----------------------------------------------------------------------------
Lutz Schroeder                  Phone +49-421-218-4683
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            lschrode@informatik.uni-bremen.de
P.O.Box 330440, D-28334 Bremen 
http://www.informatik.uni-bremen.de/~lschrode
-----------------------------------------------------------------------------