Hurkens' paradox

Hurkens' paradox is an argument that a certain combination of features in a dependent type theory is inconsistent, i.e. proves the falsum. Like Girard's paradox, it is not really a paradox per se.

The particular features here are two impredicative universes:

• a "large" universe U_1
• a "small" universe U_0, which is a member of the "larger" one
• both of which are closed under dependent products, even over themselves

Such a system was historically called System U^{-}, especially in the pure type system literature.

As such, it is impossible to have an impredicative universe Prop of propositions be a member Prop : Set of a universe Set which is also impredicative. This is the reason why Coq has made Set predicative in the more recent past.

References

• The paradox was introduced by Antonius Hurkens in a TLCA 1995 paper:

@inproceedings{hurkens_1995,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {A simplification of {Girard}'s paradox},
	volume = {902},
	booktitle = {Typed {Lambda} {Calculi} and {Applications}},
	publisher = {Springer Berlin Heidelberg},
	author = {Hurkens, Antonius J. C.},
	editor = {Dezani-Ciancaglini, Mariangiola and Plotkin, Gordon},
	year = {1995},
	doi = {10.1007/BFb0014058},
	pages = {266--278},
}

• See also

@techreport{coquand_metamathematical_1989,
	title = {Metamathematical investigations of a calculus of constructions},
	url = {https://inria.hal.science/inria-00075471},
	number = {RR-1088},
	institution = {INRIA},
	author = {Coquand, T.},
	year = {1989},
	file = {meta.pdf:C\:\\Users\\Alex\\Zotero\\storage\\V9WNAUTZ\\meta.pdf:application/pdf},
}

• Some notes on formalizing Hurkens' paradox by Arnaud Spiwack.

• A formalisation in the Coq standard library

• A blog post with a version in Agda by Jonathan Chan