(In)consistency of extensions of higher order logic and type theory

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

1 Citaat (Scopus)
107 Downloads (Pure)


It is well-known, due to the work of Girard and Coquand, that adding polymorphic domains to higher order logic, HOL, or its type theoretic variant ¿HOL, renders the logic inconsistent. This is known as Girard’s paradox, see [4]. But there is also another presentation of higher order logic, in its type theoretic variant called ¿PRED¿, to which polymorphic domains can be added safely, Both ¿HOL and ¿PRED¿ are well-known type systems and in this paper we study why ¿HOL with polymorphic domains is inconsistent and why nd ¿PRED¿ with polymorphic domains remains consistent. We do this by describing a simple model for the latter and we show why this can not be a model of the first.
Originele taal-2Engels
TitelRevised Selected Papers of the International Workshop on Types for Proofs and Programs (TYPES 2006) 18-21 April 2006, Nottingham, United Kingdom
RedacteurenT. Altenkirsch, C. McBride
Plaats van productieBerlin
ISBN van geprinte versie978-3-540-74463-4
StatusGepubliceerd - 2007
Evenementconference; TYPES 2006, Nottingham, United Kingdom; 2007-04-18; 2007-04-21 -
Duur: 18 apr. 200721 apr. 2007

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743


Congresconference; TYPES 2006, Nottingham, United Kingdom; 2007-04-18; 2007-04-21
AnderTYPES 2006, Nottingham, United Kingdom


Duik in de onderzoeksthema's van '(In)consistency of extensions of higher order logic and type theory'. Samen vormen ze een unieke vingerafdruk.

Citeer dit