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.

翻译：本文解读了coq-paradoxes包中形式化的四个悖论，即系统U中的布拉利-福尔蒂悖论、选择公理蕴含排中律的迪亚科内斯库悖论、系统F无集合论模型的雷诺兹悖论，以及针对非谓词Set的赫肯斯悖论。该包汇集了四段形式化数学内容，它们共同从外部勾勒了归纳构造演算的边界：每个文件都在一个接近CIC的系统中形式化了一个假命题推导，每个文件都展示了Rocq内核设计在何处拒绝编译该构造。文章首先讲解了Logics.v中良基性的共享机制，随后对照科康对吉拉德悖论的分析解读了BuraliForti.v中的布拉利-福尔蒂构造，阐述了diaconescu.v中的迪亚科内斯库论证，通过前初始PHI代数与劳维尔不动点定理在Reynolds.v中重构了雷诺兹论证，并遵循Geuvers对赫肯斯论证的改编在Hurkens_Set.v中进行了分析。这四个悖论共同确立了Rocq内核的三项边界条件：非谓词性的位点、大消除的限制以及宇宙约束的纪律。本文认为，该包的最佳解读方式并非将其视为一组奇闻轶事，而是作为Rocq内核不得不设计成拒绝接受哪些内容的否定式规范，以及作为这种拒绝基于正确理由的证据。