Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

Abstract

This article reads the four paradoxes mechanised in the coq-paradoxes package, namely the Burali-Forti paradox in system U, the Diaconescu paradox that the axiom of choice entails excluded middle, the Reynolds paradox that System F has no set-theoretic model, and the Hurkens paradox for impredicative Set. The package collects four pieces of mechanised mathematics that, taken together, draw the boundary of the Calculus of Inductive Constructions from the outside: each file formalises a derivation of False in a system close to CIC, and each shows where the kernel of Rocq has been designed to refuse to compile the construction. The article walks through the shared machinery of well-foundedness in Logics.v, reads the Burali-Forti construction in BuraliForti.v against Coquand's analysis of Girard's paradox, sets out the Diaconescu argument in diaconescu.v, reconstructs the Reynolds argument in Reynolds.v via the preinitial PHI-algebra and Lawvere's fixed-point theorem, and follows Geuvers's adaptation of Hurkens in Hurkens_Set.v. The four together establish three boundary conditions on the kernel of Rocq: the placement of impredicativity, the restriction of large elimination, and the discipline of universe constraints. The article argues that the package is best read not as a collection of curiosities but as a negative specification of what Rocq's kernel had to be designed to refuse, and as evidence that the refusal is being made for the right reasons.