[Prev][Next][Index][Thread]
HOL and MLPolymorphism

To: types@cis.upenn.edu

Subject: HOL and MLPolymorphism

From: Lutz Schroeder <lschrode@tzi.de>

Date: Mon, 04 Feb 2002 15:06:31 +0100

UserAgent: Mozilla/5.0 (X11; U; Linux i686; enUS; rv:0.9.4) Gecko/20010923
Coquand's 1986 paper `An analysis of Girard's paradox' contains the
claim that the combination of Churchstyle higher order logic and
MLpolymorphism is inconsistent because one can express the BuraliForti
paradox. Now, e.g., Isabelle/HOL does explicitly feature MLpolymorphism
(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 BuraliForti 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 MLpolymorphism (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 +494212184683
Dept. of Computer Science Fax +494212183054
University of Bremen lschrode@informatik.unibremen.de
P.O.Box 330440, D28334 Bremen
http://www.informatik.unibremen.de/~lschrode
