Chapter 76Optional

Universe Paradoxes and Hurkens's Construction

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Suppose a small predicate code may quantify over every code in an enclosing large universe. Its classifier must then contain a product of the form $\forall_{01} X : U_{1} . P (X) : U_{0},$ not merely a product over one decoded small code. This mixed product is the point at which the familiar failed self-membership calculation becomes dangerous. Hurkens’s construction shows that four carefully separated product operations already suffice for collapse; literal self-membership is not required.

The axiom card

This chapter uses its own Tarski-style signature $U^{-}$ . It is not an extension of the predicative hierarchy of chapter 29.

Definition 76.1 — Hurkens's U^- interface ¶

The large universe consists of a type $U_{1}$ and, for each $A : U_{1}$ , a type ${El}_{1} (A)$ . It has codes for products over a decoded large code and over all large codes: $\begin{aligned} Π_{1} (A, B) & : U_{1} & (A : U_{1}, B : {El}_{1} (A) \to U_{1}), \\ Π_{2} (F) & : U_{1} & (F : U_{1} \to U_{1}) . \end{aligned}$ For each product there are abstraction and application operations $λ_{1}, \cdot_{1}$ and $λ_{2}, \cdot_{2}$ , with signatures $\begin{aligned} λ_{1} & : (\prod_{x : {El}_{1} (A)} {El}_{1} (B x)) \to {El}_{1} (Π_{1} (A, B)), \\ \cdot_{1} & : {El}_{1} (Π_{1} (A, B)) \to \prod_{x : {El}_{1} (A)} {El}_{1} (B x), \\ λ_{2} & : (\prod_{A : U_{1}} {El}_{1} (F A)) \to {El}_{1} (Π_{2} (F)), \\ \cdot_{2} & : {El}_{1} (Π_{2} (F)) \to \prod_{A : U_{1}} {El}_{1} (F A) . \end{aligned}$ We take the two large beta laws as judgmental computation equations: $\begin{aligned} (λ_{1} x . t) \cdot_{1} a & \equiv t [a / x], \\ (λ_{2} A . t) \cdot_{2} B & \equiv t [B / A] . \end{aligned}$ Spiwack presents corresponding equality axioms and rewrites along them. The judgmental presentation used here exposes the same conversion sites without printing the transports; it is therefore a strengthened presentation of the source interface, not a claim that its equalities were judgmental.

There is a code $u_{0} : U_{1}$ . Put $U_{0} : = {El}_{1} (u_{0})$ and assume a type ${El}_{0} (a)$ for each $a : U_{0}$ . The small codes are closed under $\begin{aligned} Π_{0} (a, b) & : U_{0} & (a : U_{0}, b : {El}_{0} (a) \to U_{0}), \\ Π_{01} (A, b) & : U_{0} & (A : U_{1}, b : {El}_{1} (A) \to U_{0}), \end{aligned}$ with abstraction and application $λ_{0}, \cdot_{0}$ and $λ_{01}, \cdot_{01}$ , typed by $\begin{aligned} λ_{0} & : (\prod_{x : {El}_{0} (a)} {El}_{0} (b x)) \to {El}_{0} (Π_{0} (a, b)), \\ \cdot_{0} & : {El}_{0} (Π_{0} (a, b)) \to \prod_{x : {El}_{0} (a)} {El}_{0} (b x), \\ λ_{01} & : (\prod_{x : {El}_{1} (A)} {El}_{0} (b x)) \to {El}_{0} (Π_{01} (A, b)), \\ \cdot_{01} & : {El}_{0} (Π_{01} (A, b)) \to \prod_{x : {El}_{1} (A)} {El}_{0} (b x) . \end{aligned}$ No beta law for either small product is assumed. Finally fix an arbitrary code $F : U_{0}$ .

Referenced from 6 locations

We use the following local notation, always at the code level: $\begin{aligned} \forall_{1} x : A . B & : = Π_{1} (A, λ x . B), & A \to_{1} B & : = \forall_{1}_: A . B, \\ \forall_{2} A . B & : = Π_{2} (λ A . B), \\ \forall_{0} x : a . b & : = Π_{0} (a, λ x . b), & a \to_{0} b & : = \forall_{0}_: a . b, \\ \forall_{01} x : A . b & : = Π_{01} (A, λ x . b) . \end{aligned}$ Thus ${El}_{1} (A \to_{1} u_{0})$ carries application into ${El}_{1} (A) \to U_{0}$ and abstraction back, with the displayed one-sided beta equation. We do not identify it with that function type. The code $a \to_{0} b : U_{0}$ has the corresponding small introduction and elimination operations but no assumed beta equation. The subscripts distinguish a code in $U_{1}$ from one in $U_{0}$ .

The diagonal terms

The following definitions are Spiwack’s axiomatisation with names expanded and types kept beside the terms [Spi15].

Definition 76.2 — The Hurkens spine ¶

Define the large codes $\begin{aligned} V & : = \forall_{2} A . ((A \to_{1} u_{0}) \to_{1} A \to_{1} u_{0}) \to_{1} A \to_{1} u_{0} : U_{1}, \\ U & : = V \to_{1} u_{0} : U_{1} . \end{aligned}$ Here $U$ is a code in the universe $U_{1}$ , not a third universe; $U_{0}$ is the small universe decoded from $u_{0}$ . For $z : {El}_{1} (V)$ define $sb (z) : = λ_{2} A . λ_{1} r . λ_{1} a . r \cdot_{1} (z \cdot_{2} A \cdot_{1} r) \cdot_{1} a : {El}_{1} (V) .$ For $i : {El}_{1} (U \to_{1} u_{0})$ and $x : {El}_{1} (U)$ put $le (i, x) : = x \cdot_{1} (λ_{2} A . λ_{1} r . λ_{1} a . i \cdot_{1} (λ_{1} v . sb (v) \cdot_{2} A \cdot_{1} r \cdot_{1} a)) : U_{0} .$ Its curried large representative is ${le}^{'} : = λ_{1} i . λ_{1} x . le (i, x) : {El}_{1} ((U \to_{1} u_{0}) \to_{1} U \to_{1} u_{0}) .$ Now define the small code $Ind (i) : = \forall_{01} x : U . le (i, x) \to_{0} (i \cdot_{1} x) : U_{0},$ the large term $WF : = λ_{1} z . Ind (z \cdot_{2} U \cdot_{1} {le}^{'}) : {El}_{1} (U),$ and, for $x : {El}_{1} (U)$ , the large term $D (x) : = λ_{1} v . sb (v) \cdot_{2} U \cdot_{1} {le}^{'} \cdot_{1} x : {El}_{1} (U) .$ For $i : {El}_{1} (U \to_{1} u_{0})$ put $J (i) : = λ_{1} y . i \cdot_{1} D (y) : {El}_{1} (U \to_{1} u_{0}) .$ Finally, for $x : {El}_{1} (U)$ define the small code $I (x) : = (\forall_{01} i : (U \to_{1} u_{0}) . le (i, x) \to_{0} (i \cdot_{1} D (x))) \to_{0} F : U_{0} .$

Referenced from 3 locations

Universe Paradoxes and Hurkens's Construction

Every displayed application is now checkable from the adjacent type. The critical one is $z \cdot_{2} U \cdot_{1} {le}^{'} : {El}_{1} (U \to_{1} u_{0})$ : since $z : {El}_{1} (V)$ , instantiating its outer $\forall_{2}$ at $U$ expects exactly the large representative ${le}^{'}$ . The result is precisely the domain of $Ind$ , so $WF$ is well formed.

The diagonal proof uses four conversions, all generated by the two large beta equations: $\begin{aligned} (β_{1}) & J (i) \cdot_{1} x & \equiv i \cdot_{1} D (x), \\ (β_{1}, β_{2}) & le (J (i), x) & \equiv le (i, D (x)), \\ (β_{1}, β_{2}) & le (i, WF) & \equiv Ind (J (i)), \\ (β_{1}) & (λ_{1} u . I (u)) \cdot_{1} x & \equiv I (x) . \end{aligned}$ For the second equation, unfold $le$ and contract the outer $λ_{1}$ in $J (i)$ and the $λ_{2}$ and $λ_{1}$ redexes in $sb$ . The third unfolds $WF$ and $Ind$ before the same contractions. No small beta equation is used.

Lemma 76.3 — The three inhabitants ¶

Under definition 76.1, definition 76.2, there are terms $\begin{aligned} Ω & : {El}_{0} (\forall_{01} i : (U \to_{1} u_{0}) . Ind (i) \to_{0} (i \cdot_{1} WF)), \\ L_{1} & : {El}_{0} (Ind (λ_{1} u . I (u))), \\ L_{2} & : {El}_{0} ((\forall_{01} i : (U \to_{1} u_{0}) . Ind (i) \to_{0} (i \cdot_{1} WF)) \to_{0} F) . \end{aligned}$ Their construction uses only the two large beta laws.

Referenced from 6 locations

Proof of Lemma 76.3 — The three inhabitants

Proof. Write $Q : = \forall_{01} i : (U \to_{1} u_{0}) . Ind (i) \to_{0} (i \cdot_{1} WF) and k : = λ_{1} u . I (u) .$ The three inhabitants are the following terms: $\begin{aligned} Ω : = & λ_{01} i . λ_{0} y . y \cdot_{01} WF \cdot_{0} (λ_{01} x . λ_{0} h . y \cdot_{01} D (x) \cdot_{0} h), \\ L_{1} : = & λ_{01} x . λ_{0} p . λ_{0} q . (q \cdot_{01} k \cdot_{0} p) \cdot_{0} (λ_{01} i . λ_{0} h . q \cdot_{01} J (i) \cdot_{0} h), \\ L_{2} : = & λ_{0} q . (q \cdot_{01} k \cdot_{0} L_{1}) \cdot_{0} (λ_{01} i . λ_{0} h . q \cdot_{01} J (i) \cdot_{0} h) . \end{aligned}$

We check the terms from the outside inward. For $Ω$ , let $i : {El}_{1} (U \to_{1} u_{0})$ and $y : {El}_{0} (Ind (i))$ . Application at $WF$ asks for ${El}_{0} (le (i, WF))$ . By (β _1,β _2), this is ${El}_{0} (Ind (J (i)))$ . Its displayed inhabitant sends $x$ and $h : {El}_{0} (le (J (i), x))$ to $y \cdot_{01} D (x) \cdot_{0} h$ : equation (β _1,β _2) converts the premise, and (β _1) converts the result. Thus $Ω : Q$ .

For $L_{1}$ , the outer two abstractions construct $Ind (k)$ . By (β _1), their result must inhabit $I (x)$ . After introducing $p : {El}_{0} (le (k, x)) and q : {El}_{0} (\forall_{01} i . le (i, x) \to_{0} i \cdot_{1} D (x)),$ the term $q \cdot_{01} k \cdot_{0} p$ inhabits $I (D (x))$ by (β _1). Its remaining argument is constructed by sending $i, h$ to $q \cdot_{01} J (i) \cdot_{0} h$ ; equations (β _1,β _2) and (β _1) give exactly the required premise and conclusion. This establishes $L_{1}$ .

Finally let $q : {El}_{0} (Q)$ . The term $q \cdot_{01} k \cdot_{0} L_{1}$ inhabits $I (WF)$ by (β _1). Its displayed final argument sends $i$ and $h : {El}_{0} (le (i, WF))$ to $q \cdot_{01} J (i) \cdot_{0} h$ ; equation (β _1,β _2) converts $h$ to the required induction premise, and (β _1) converts the result. Hence $L_{2} : Q \to_{0} F$ .

These terms are the transport-free, judgmental-beta presentation of Spiwack’s Omega, lemma1, and lemma2 [Spi15]. The four code formers correspond to the source’s Forall1, ForallU1, Forall0, and ForallU0, respectively. Every conversion above is one of the four displayed $β_{1} / β_{2}$ equations; no small beta law occurs. ◻

Theorem 76.4 — Hurkens collapse ¶

For every $F : U_{0}$ , the interface of definition 76.1 yields a term of ${El}_{0} (F)$ .

Referenced from 8 locations

Proof of Theorem 76.4 — Hurkens collapse

Proof. By lemma 76.3, application $L_{2} \cdot_{0} Ω$ has type ${El}_{0} (F)$ . Application is an operation supplied by the interface; no small beta equation is used. ◻

Corollary 76.5 — The exact inconsistency boundary ¶

If some $F : U_{0}$ decodes to an empty type, the interface is inconsistent. Removing either large product closure, either small product closure, the embedding $u_{0}$ , or the relevant introduction/elimination operation blocks the displayed derivation. The derivation does not require beta for either small product.

Referenced from 3 locations

Universe Paradoxes and Hurkens's Construction

Proof of Corollary 76.5 — The exact inconsistency boundary

Proof. If ${El}_{0} (F)$ is empty, theorem 76.4 supplies an inhabitant of an empty type. The dependency boundary is read from the written terms:

$Π_{1}$ .: It first forms $U = V \to_{1} u_{0}$ and is then used by $sb$ , $le$ , ${le}^{'}$ , $D$ , and $J$ .
$Π_{2}$ .: It forms the head of $V$ and permits each $z \cdot_{2} A$ and $sb (v) \cdot_{2} U$ application.
$Π_{0}$ .: It forms the small implications in $Ind$ and $I$ , including the final implication to $F$ .
$Π_{01}$ .: It forms the quantifiers over $x : U$ and over $i : U \to_{1} u_{0}$ in $Ind$ , $I$ , $Q$ , and the three proof terms.
$u_{0}$ .: It supplies the small-universe code used in every $A \to_{1} u_{0}$ classifier and in the definition of $U_{0}$ .

The displayed proof terms also use the corresponding abstraction and application operations. Their only reductions are the four large-beta conversions in (β _1), (β _1,β _2), (β _1,β _2), and (β _1); neither small beta law is present. Removing one listed operation makes the first named construction that uses it ill formed. This proves a dependency claim about this derivation, not consistency of any weakened interface. ◻

It does not follow that every weakening of one assumption is consistent. In particular, ordinary predicative hierarchies avoid the interface because a small impredicative product may not quantify over the enclosing large universe.

A Reynolds–Hurkens variation

Coquand’s variation is a separate higher-order-logic calculation, not a renaming of theorem 76.4. Its $λ HOL$ card has sorts $*, ◻, △$ , axioms $* : ◻$ , $◻ : △$ , and product rules $(*, *)$ , $(◻, ◻)$ , and $(◻, *)$ . Fix $A : ◻$ , put $⊥ : = \forall p : * . p$ and $\neg p : = p \to ⊥$ , and let $Pow (X) = X \to *$ and $T (X) = Pow (Pow (X))$ . The rule $(◻, *)$ is spent when a proposition quantifies over $p : Pow (A)$ . For $f : X \to Y$ , $Q : T (X)$ , and $p : Pow (Y)$ , functorial action is $T (f) (Q) : = λ p . Q (λ x . p (f x)) .$

Theorem 76.6 — Reynolds–Hurkens retraction boundary ¶

In minimal higher-order logic, suppose $A$ is a type with maps $intro : T (A) \to A, match : A \to T (A),$ and the judgmental equality $\begin{matrix} (R H) & match \circ intro \equiv T (intro \circ match) . \end{matrix}$ Then falsity is inhabited.

Referenced from 2 locations

Universe Paradoxes and Hurkens's Construction

Proof of Theorem 76.6 — Reynolds–Hurkens retraction boundary

Proof. Put $δ = intro \circ match$ and define $\begin{aligned} p_{0} (x) & : = \forall p : Pow (A) . p (δ x) \to \neg match (x) (p), \\ X_{0} (p) & : = \forall x : A . p (x) \to \neg match (x) (p), \\ x_{0} & : = intro (X_{0}) . \end{aligned}$ Equation (RH) gives $match (δ x) (p) \equiv match (x) (p \circ δ)$ . Let $x : A$ , $p : Pow (A)$ , $h_{1} : p_{0} (x)$ , and $h_{0} : X_{0} (p)$ . The auxiliary terms are $\begin{aligned} s_{1} (x, h_{1}) & : = λ p . h_{1} (p \circ δ) & : p_{0} (δ x), \\ s_{2} (p, h_{0}) & : = λ x . h_{0} (δ x) & : X_{0} (p \circ δ), \\ l_{0} & : = λ p . λ h . λ h_{0} . h_{0} (x_{0}) (h) (s_{2} (p, h_{0})), \\ l_{1} & : = λ x . λ h_{1} . h_{1} (p_{0}) (s_{1} (x, h_{1})) & : X_{0} (p_{0}) . \end{aligned}$ Here $l_{0} : \prod_{p : Pow (A)} p (x_{0}) \to \neg X_{0} (p) .$ Its typing uses (RH) to convert $match (x_{0}) (p)$ to $X_{0} (p \circ δ)$ . For arbitrary $p : Pow (A)$ and $h : p (δ x_{0})$ , put $l_{2} (p, h) : = l_{0} (p \circ δ, h) : \neg match (x_{0}) (p) .$ The classifier is converted using (RH), since $match (x_{0}) (p) \equiv X_{0} (p \circ δ)$ . Thus $l_{2} : p_{0} (x_{0})$ . The final term $l_{0} (p_{0}, l_{2}, l_{1})$ has type $⊥$ . This is the calculation of Coquand’s Theorem 1.2 [Coq23]; its only conversion beyond beta is (RH), used in the typings of $s_{1}$ , $s_{2}$ , $l_{0}$ , and $l_{2}$ . The source prints $l_{0} (x_{0}, l_{2}, l_{1})$ at the final step; its declared type requires the first argument $p_{0}$ , as displayed here. ◻

The weak impredicative encoding $A : = Π_{X : ◻} (T X \to X) \to X$ supplies such maps and equation in $λ U^{-}$ , which extends the displayed $λ HOL$ card by the product rule $(△, ◻)$ [Coq23]. That observation is scoped to the stated sort and product rules. It neither adds those rules to the book’s predicative hierarchy nor turns Reynolds’s semantic non-definability theorem into this syntactic contradiction.

Exercise 76.1 ¶

★★☆ Starting from $z : {El}_{1} (V)$ , type every application in $sb (z)$ . Record which occurrence uses $Π_{2}$ rather than $Π_{1}$ .

Referenced from 3 locations

Exercise 29.17 ¶

★☆☆ Work in the inductive theory of chapter 28 extended by the $U^{-}$ interface, and assume $F : U_{0}$ with ${El}_{0} (F) \equiv 0$ type. Use theorem 76.4 and empty elimination to inhabit any given closed type.

Referenced from 3 locations

Suggested first pass.

Begin with exercise 76.3, exercise 76.4; then run exercise 76.5 and compare each rejected certificate with the mathematical dependency ledger in corollary 76.5.

Exercise 76.3 ¶

★★★ For each conversion in (β _1), (β _1,β _2), (β _1,β _2), and (β _1), mark the contracted $β_{1}$ and $β_{2}$ redexes. Then check each use of those equations in the proof of lemma 76.3. Verify that no line appeals to $β_{0}$ or $β_{01}$ .

Referenced from 4 locations

Exercise 76.4 ¶

★★☆ Derive $match (δ x) (p) \equiv match (x) (p \circ δ)$ from (RH) by expanding $T$ . Identify the exact type of $s_{2} (p, h)$ and the four points at which the proof uses (RH).

Referenced from 4 locations

Exercise 76.5 ¶

★★★ Practical project.hurkens-assumption-ledger Run this chapter’s Kappa assumption ledger. Remove $Π_{1}$ , $Π_{2}$ , $Π_{0}$ , $Π_{01}$ , and $u_{0}$ in turn and require the corresponding named rejection. Then enable the two small-beta flags: the accepted certificate must remain accepted. Explain why this finite Boolean dependency check is not a term checker and does not mechanize theorem 76.4.

Referenced from 5 locations

Bibliographic notes

Hurkens gave the compact paradox in 1995 [Hur95]. Spiwack’s axiomatisation records exactly which beta laws the proof uses [Spi15]; those pages were the primary rule and proof source for definition 76.1, lemma 76.3. Coquand’s Reynolds–Hurkens variation states the separate retraction equation and its $λ U^{-}$ encoding [Coq23]. The Rocq library and an Agda file compiled with --type-in-type are useful replays of stronger inconsistent settings. Neither is evidence that the predicative hierarchy of chapter 29 admits the displayed interface.