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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)
90 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationRevised Selected Papers of the International Workshop on Types for Proofs and Programs (TYPES 2006) 18-21 April 2006, Nottingham, United Kingdom
EditorsT. Altenkirsch, C. McBride
Place of PublicationBerlin
PublisherSpringer
Pages140-159
ISBN (Print)978-3-540-74463-4
DOIs
Publication statusPublished - 2007
Eventconference; TYPES 2006, Nottingham, United Kingdom; 2007-04-18; 2007-04-21 -
Duration: 18 Apr 200721 Apr 2007

Publication series

NameLecture Notes in Computer Science
Volume4502
ISSN (Print)0302-9743

Conference

Conferenceconference; TYPES 2006, Nottingham, United Kingdom; 2007-04-18; 2007-04-21
Period18/04/0721/04/07
OtherTYPES 2006, Nottingham, United Kingdom

Fingerprint

Dive into the research topics of '(In)consistency of extensions of higher order logic and type theory'. Together they form a unique fingerprint.

Cite this