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

Bernardo Alonso

arxiv: 2605.27633 · v1 · pith:IEQD5MKOnew · submitted 2026-05-26 · 💻 cs.LO

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

Bernardo Alonso This is my paper

Pith reviewed 2026-06-29 14:19 UTC · model grok-4.3

classification 💻 cs.LO

keywords Burali-Forti paradoxDiaconescu paradoxReynolds paradoxHurkens paradoxCalculus of Inductive ConstructionsRocq kernelimpredicativityproof assistant

0 comments

The pith

Four mechanized paradoxes mark the exact refusal points that keep Rocq's kernel consistent.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper examines four paradoxes formalized in the coq-paradoxes library to show how they expose the necessary restrictions in the Calculus of Inductive Constructions used by Rocq. It walks through Burali-Forti, Diaconescu, Reynolds, and Hurkens paradoxes, each deriving falsehood in a system close to CIC but blocked by the kernel. This collection serves as a negative specification, indicating what the kernel must refuse: impredicativity in certain places, large elimination, and universe constraints. A sympathetic reader would care because it explains the design choices that prevent inconsistency in proof assistants.

Core claim

The four mechanizations 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 package is a negative specification of what the kernel must refuse.

What carries the argument

The coq-paradoxes library files that encode the paradoxes and identify the CIC kernel's refusal points.

If this is right

The kernel must place impredicativity to block the Hurkens paradox in Set.
Large elimination must be restricted to avoid derivations of falsehood.
Universe constraints must be enforced to stop constructions like Burali-Forti.
The Diaconescu formalization shows why choice implies excluded middle only under specific logic rules.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar negative specifications could be built for other proof assistants to test their type theory boundaries.
New kernel features in Rocq could be validated by attempting to encode these paradoxes.
The approach suggests that consistency proofs for type theories benefit from explicit mechanized counterexamples.

Load-bearing premise

The mechanizations in the coq-paradoxes files are faithful to the original paradoxes and correctly identify the refusal points without artifacts from the encoding.

What would settle it

A demonstration that the kernel accepts one of the four constructions without deriving inconsistency, or that a new paradox evades the current refusal points.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper packages four known paradoxes into Coq files to mark Rocq kernel boundaries, but the main value is the exposition rather than any new result.

read the letter

The paper's core contribution is a library and accompanying write-up that turns four classic paradoxes into runnable Coq derivations. It shows where each one fails to type-check in systems close to CIC, using the Burali-Forti, Diaconescu, Reynolds, and Hurkens examples. Nothing here derives a new paradox or changes the underlying mathematics; the paradoxes themselves come from the cited prior work by Coquand, Geuvers, and others.

What the paper does well is walk through the actual code. It explains the shared well-foundedness machinery in Logics.v, then steps through each file against the original analyses. The Reynolds reconstruction via the preinitial PHI-algebra and the Hurkens adaptation are laid out clearly enough that a reader can see the connection to the source papers. That kind of concrete mapping is useful when people want to understand why certain features are blocked.

The soft spot is the claim that these four files establish three precise boundary conditions on the kernel. That rests on the mechanizations being faithful reproductions without artifacts from the encoding or the shared library. If the well-foundedness setup or universe handling shifts the exact refusal point, the identified conditions on impredicativity, large elimination, and universe discipline become less diagnostic. The paper treats the files as direct enough, but that assumption is not checked against the originals in the text provided.

This is for people who work on Rocq kernel design or teach the limits of type theory. A reader already familiar with the paradoxes will mostly see a convenient collection rather than fresh insight. It deserves peer review because the formalizations exist and the topic matters for anyone maintaining or extending the system, even if the novelty is incremental.

Referee Report

1 major / 2 minor

Summary. This paper analyzes four paradoxes mechanized in the coq-paradoxes library for Coq/Rocq: the Burali-Forti paradox in BuraliForti.v, Diaconescu's paradox in diaconescu.v, Reynolds' paradox in Reynolds.v, and Hurkens' paradox in Hurkens_Set.v. It claims that these formalizations, using shared machinery in Logics.v, collectively establish three boundary conditions on the CIC kernel: placement of impredicativity, restriction of large elimination, and discipline of universe constraints. The package is presented as a negative specification of what the Rocq kernel refuses to compile, based on derivations of False in systems close to CIC.

Significance. If the mechanizations faithfully reproduce the original paradoxes without artifacts from the encoding or Logics.v, this work provides a valuable contribution by offering machine-checked evidence for the design rationale behind Rocq's kernel. The use of formal proofs to delineate consistency boundaries is a strength, potentially useful for researchers in type theory and proof assistant development.

major comments (1)

[Discussion of Logics.v and the paradox files (BuraliForti.v, diaconescu.v, Reynolds.v, Hurkens_Set.v)] The claim that these establish the three kernel boundary conditions requires that the mechanizations are faithful to the cited sources (Coquand on Girard's paradox, Diaconescu, Reynolds via Lawvere, Geuvers) and that the well-foundedness machinery in Logics.v does not introduce or remove universe constraints or alter large-elimination usage. An explicit argument or check that the refusal points match the originals without encoding shifts is needed, as this is load-bearing for the negative specification interpretation.

minor comments (2)

[Abstract] The abstract could explicitly list the three boundary conditions for clarity.
[References] Ensure all cited works on the original paradoxes (e.g., full citations for Coquand, Geuvers) are included.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful review and for emphasizing the importance of faithfulness in the mechanizations. We address the major comment below.

read point-by-point responses

Referee: The claim that these establish the three kernel boundary conditions requires that the mechanizations are faithful to the cited sources (Coquand on Girard's paradox, Diaconescu, Reynolds via Lawvere, Geuvers) and that the well-foundedness machinery in Logics.v does not introduce or remove universe constraints or alter large-elimination usage. An explicit argument or check that the refusal points match the originals without encoding shifts is needed, as this is load-bearing for the negative specification interpretation.

Authors: The manuscript already supplies detailed source comparisons: BuraliForti.v is read directly against Coquand's analysis of Girard's paradox; diaconescu.v follows the standard Diaconescu derivation; Reynolds.v reconstructs the argument via Lawvere's fixed-point theorem on the preinitial PHI-algebra; and Hurkens_Set.v follows Geuvers's adaptation. The well-foundedness definitions in Logics.v are auxiliary and do not participate in the impredicativity, large-elimination, or universe-level steps that trigger the kernel refusals. Nevertheless, we agree that a standalone, explicit verification of these refusal points would make the negative-specification claim more robust. We will therefore insert a concise new subsection that tabulates the precise universe annotations and elimination rules appearing in each file and confirms they align with the cited sources without encoding-induced shifts. This is a partial revision. revision: partial

Circularity Check

0 steps flagged

No circularity: claims rest on explicit Coq mechanizations and external citations

full rationale

The paper's central claim—that the four mechanized paradoxes delineate Rocq kernel boundaries on impredicativity, large elimination, and universe constraints—is supported by direct reference to the contents of BuraliForti.v, diaconescu.v, Reynolds.v, Hurkens_Set.v and the shared Logics.v well-foundedness definitions. These are presented as faithful reproductions of cited external sources (Coquand on Girard, Diaconescu, Reynolds/Lawvere, Geuvers) rather than derived from any fitted parameter, self-defined quantity, or load-bearing self-citation chain. No step equates a 'prediction' or 'result' to its own input by construction; the refusal points are exhibited by the failure of the encoded derivations to type-check, which is independently checkable against the CIC rules. The analysis therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard properties of the Calculus of Inductive Constructions and prior analyses of the paradoxes; no new free parameters, axioms beyond standard math, or invented entities are introduced.

axioms (1)

standard math Properties of the Calculus of Inductive Constructions as implemented in Rocq
Invoked throughout to explain where the kernel refuses the constructions.

pith-pipeline@v0.9.1-grok · 5821 in / 1168 out tokens · 38322 ms · 2026-06-29T14:19:08.531271+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

9 extracted references · 7 canonical work pages

[1]

Coq library, Rocq Prover Package Index

URLhttps://rocq-prover.org/p/coq-paradoxes/latest. Coq library, Rocq Prover Package Index. Thierry Coquand. An analysis of Girard’s paradox. InProceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pages 227–236, Washington, DC,

1986
[2]

Thierry Coquand and Christine Paulin-Mohring

doi: 10.1016/0890-5401(88)90005-3. Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors,COLOG-88, volume 417 ofLecture Notes in Computer Science, pages 50–66. Springer, Berlin,

work page doi:10.1016/0890-5401(88)90005-3
[3]

Inductively defined types

doi: 10.1007/3-540-52335-9_47. Radu Diaconescu. Axiom of choice and complementation.Proceedings of the American Mathe- matical Society, 51(1):176–178,

work page doi:10.1007/3-540-52335-9_47
[4]

Herman Geuvers

doi: 10.2307/2040105. Herman Geuvers. Inconsistency of classical logic in type theory,

work page doi:10.2307/2040105
[5]

19780242514

doi: 10.1002/malq. 19780242514. Antonius J. C. Hurkens. A simplification of Girard’s paradox. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors,Typed Lambda Calculi and Applications (TLCA 1995), volume 902 ofLecture Notes in Computer Science, pages 266–278, Berlin,

work page doi:10.1002/malq 1995
[6]

doi: 10.1007/BF01110627. F. William Lawvere. Diagonal arguments and Cartesian closed categories. InCategory Theory, Homology Theory and their Applications II, volume 92 ofLecture Notes in Mathematics, pages 134–145. Springer, Berlin,

work page doi:10.1007/bf01110627
[7]

doi: 10.1007/BFb0080769. John C. Reynolds. Polymorphism is not set-theoretic. Research Report RR-0296, INRIA,

work page doi:10.1007/bfb0080769
[8]

URLhttps: //rocq-prover.org. INRIA. Benjamin Werner. Sets in types, types in sets. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software (TACS 1997), volume 1281 ofLecture Notes in Computer Science, pages 530–546, Berlin,

1997
[9]

doi: 10.1007/BFb0014566

Springer. doi: 10.1007/BFb0014566. 13

work page doi:10.1007/bfb0014566

[1] [1]

Coq library, Rocq Prover Package Index

URLhttps://rocq-prover.org/p/coq-paradoxes/latest. Coq library, Rocq Prover Package Index. Thierry Coquand. An analysis of Girard’s paradox. InProceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pages 227–236, Washington, DC,

1986

[2] [2]

Thierry Coquand and Christine Paulin-Mohring

doi: 10.1016/0890-5401(88)90005-3. Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors,COLOG-88, volume 417 ofLecture Notes in Computer Science, pages 50–66. Springer, Berlin,

work page doi:10.1016/0890-5401(88)90005-3

[3] [3]

Inductively defined types

doi: 10.1007/3-540-52335-9_47. Radu Diaconescu. Axiom of choice and complementation.Proceedings of the American Mathe- matical Society, 51(1):176–178,

work page doi:10.1007/3-540-52335-9_47

[4] [4]

Herman Geuvers

doi: 10.2307/2040105. Herman Geuvers. Inconsistency of classical logic in type theory,

work page doi:10.2307/2040105

[5] [5]

19780242514

doi: 10.1002/malq. 19780242514. Antonius J. C. Hurkens. A simplification of Girard’s paradox. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors,Typed Lambda Calculi and Applications (TLCA 1995), volume 902 ofLecture Notes in Computer Science, pages 266–278, Berlin,

work page doi:10.1002/malq 1995

[6] [6]

doi: 10.1007/BF01110627. F. William Lawvere. Diagonal arguments and Cartesian closed categories. InCategory Theory, Homology Theory and their Applications II, volume 92 ofLecture Notes in Mathematics, pages 134–145. Springer, Berlin,

work page doi:10.1007/bf01110627

[7] [7]

doi: 10.1007/BFb0080769. John C. Reynolds. Polymorphism is not set-theoretic. Research Report RR-0296, INRIA,

work page doi:10.1007/bfb0080769

[8] [8]

URLhttps: //rocq-prover.org. INRIA. Benjamin Werner. Sets in types, types in sets. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software (TACS 1997), volume 1281 ofLecture Notes in Computer Science, pages 530–546, Berlin,

1997

[9] [9]

doi: 10.1007/BFb0014566

Springer. doi: 10.1007/BFb0014566. 13

work page doi:10.1007/bfb0014566