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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

1 Citaat (Scopus)
91 Downloads (Pure)

Samenvatting

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
UitgeverijSpringer
Pagina's140-159
ISBN van geprinte versie978-3-540-74463-4
DOI's
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
Volume4502
ISSN van geprinte versie0302-9743

Congres

Congresconference; TYPES 2006, Nottingham, United Kingdom; 2007-04-18; 2007-04-21
Periode18/04/0721/04/07
AnderTYPES 2006, Nottingham, United Kingdom

Vingerafdruk

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