TY - GEN
T1 - (In)consistency of extensions of higher order logic and type theory
AU - Geuvers, J.H.
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-540-74464-1_10
DO - 10.1007/978-3-540-74464-1_10
M3 - Conference contribution
SN - 978-3-540-74463-4
T3 - Lecture Notes in Computer Science
SP - 140
EP - 159
BT - Revised Selected Papers of the International Workshop on Types for Proofs and Programs (TYPES 2006) 18-21 April 2006, Nottingham, United Kingdom
A2 - Altenkirsch, T.
A2 - McBride, C.
PB - Springer
CY - Berlin
T2 - conference; TYPES 2006, Nottingham, United Kingdom; 2007-04-18; 2007-04-21
Y2 - 18 April 2007 through 21 April 2007
ER -