While it’s rather difficult to accidentally prove an inconsistency in a wellmeaning type theory that isn’t obviously inconsistent (have you ever unintentionally proven that a type corresponding to an ordinal is strictly larger than itself? I didn’t think so), it feels like it’s comparatively easy to add rather innocent features to your type theory that will suddenly make it inconsistent. And there are so many of them! And sometimes it’s the interaction among the features rather than the features themselves that produce inconsistencies.
Hurken’s Paradox
As it turns out, a lot of the inconsistencies can surface as proofs of what’s known as Hurkens’ paradox^{1}, which is a simplification of Girard’s paradox^{2}, which itself is a typetheoretical formulation of the settheoretical Burali–Forti’s paradox^{3}. I won’t claim to deeply understand how any of these paradoxes work, but I’ll present various formulations of Hurkens’ paradox in the context of the most wellknown inconsistent features.
Type in Type
The most common mechanization of Hurkens’ paradox you can find online is using typeintype,
where the type of the universe Type
has Type
itself as its type,
because most proof assistants have ways of turning this check off.
We begin with what Hurkens calls a powerful paradoxical universe,
which is a type U
along with two functions τ : ℘ (℘ U) → U
and σ : U → ℘ (℘ U)
.
Conceptually, ℘ X
is the powerset of X
, implemented as X → Type
;
τ
and σ
then form an isomorphism between U
and the powerset of its powerset, which is an inconsistency.
Hurkens defines U
, τ
, and σ
as follows, mechanized in Agda below.
U : Set
U = ∀ (X : Set) → (℘ (℘ X) → X) → ℘ (℘ X)
τ : ℘ (℘ U) → U
τ t = λ X f p → t (λ x → p (f (x X f)))
σ : U → ℘ (℘ U)
σ s = s U τ
The complete proof can be found at Hurkens.html, but we’ll focus on just these definitions for the remainder of this post.
Two Impredicative Universe Layers
Hurkens’ original construction of the paradox was done in System U⁻, where there are two impredicative universes,
there named *
and □
.
We’ll call ours Set
and Set₁
, with the following typing rules for function types featuring impredicativity.
Γ ⊢ A : 𝒰
Γ, x: A ⊢ B : Set
────────────────── ΠSet
Γ ⊢ Πx: A. B : Set
Γ ⊢ A : 𝒰
Γ, x: A ⊢ B : Set₁
─────────────────── ΠSet₁
Γ ⊢ Πx: A. B : Set₁
Going back to the typeintype proof, consider now ℘ (℘ X)
.
By definition, this is (X → Set) → Set
; since Set : Set₁
, by ΠSet₁,
the term has type Set₁
, regardless of what the type of X
is.
Then U = ∀ X → (℘ (℘ X) → X) → ℘ (℘ X)
has type Set₁
as well.
Because later when defining σ : U → ℘ (℘ U)
, given a term s : U
, we want to apply it to U
,
the type of X
should have the same type as U
for σ
to type check.
The remainder of the proof of inconsistency is unchanged, as it doesn’t involve any explicit universes,
although we also have the possibility of lowering the return type of ℘
.
An impredicative Set₁
above a predicative Set
may be inconsistent as well,
since we never make use of the impredicativity of Set
itself.
℘ : ∀ {ℓ} → Set ℓ → Set₁
℘ {ℓ} S = S → Set
U : Set₁
U = ∀ (X : Set₁) → (℘ (℘ X) → X) → ℘ (℘ X)
Note well that having two impredicative universe layers is not the same thing as having two parallel impredicative universes.
For example, by turning on impredicativeset
in Coq, we’d have an impredicative Prop
and an impredicative Set
,
but they are in a sense parallel universes: the type of Prop
is Type
, not Set
.
The proof wouldn’t go through in this case, since it relies on the type of the return type of ℘
being impredicative as well.
With cumulativity, Prop
is a subtype of Set
, but this has no influence for our puposes.
Strong Impredicative Pairs
A strong (dependent) pair is a pair from which we can project its components.
An impredicative pair in some impredicative universe 𝒰
is a pair that lives in 𝒰
when either of its components live in 𝒰
,
regardless of the universe of the other component.
It doesn’t matter too much which specific universe is impredicative as long as we can refer to both it and its type,
so we’ll suppose for this section that Set
is impredicative.
The typing rules for the strong impredicative pair are then as follows;
we only need to allow the first component of the pair to live in any universe.
Γ ⊢ A : 𝒰
Γ, x: A ⊢ B : Set
──────────────────
Γ ⊢ Σx: A. B : Set
Γ ⊢ a : A
Γ ⊢ b : B[x ↦ a]
─────────────────────
Γ ⊢ (a, b) : Σx: A. B
Γ ⊢ p : Σx: A. B
────────────────
Γ ⊢ fst p : A
Γ ⊢ p : Σx: A. B
────────────────────────
Γ ⊢ snd p : B[x ↦ fst p]
Γ ⊢ (a, b) : Σx: A. B
──────────────────────
Γ ⊢ fst (a, b) ≡ a : A
Γ ⊢ (a, b) : Σx: A. B
─────────────────────────────
Γ ⊢ snd (a, b) ≡ b : B[x ↦ a]
If we turn typeintype off in the previous example, the first place where type checking fails is for U
,
which with predicative universes we would expect to have type Set₁
.
The idea, then, is to squeeze U
into the lower universe Set
using the impredicativity of the pair,
then to extract the element of U
as needed using the strongness of the pair.
Notice that we don’t actually need the second component of the pair, which we can trivially fill in with ⊤
.
This means we could instead simply use the following record type in Agda.
record Lower (A : Set₁) : Set where
constructor lower
field raise : A
The type Lower A
is equivalent to Σx: A. ⊤
, its constructor lower a
is equivalent to (a, tt)
,
and the projection raise
is equivalent to fst
.
To allow type checking this definition, we need to again turn on typeintype, despite never actually exploiting it.
If we really want to make sure we really never make use of typeintype,
we can postulate Lower
, lower
, and raise
, and use rewrite rules to recover the computational behaviour of the projection.
{# OPTIONS rewriting #}
postulate
Lower : (A : Set₁) → Set
lower : ∀ {A} → A → Lower A
raise : ∀ {A} → Lower A → A
beta : ∀ {A} {a : A} → raise (lower a) ≡ a
{# REWRITE beta #}
Refactoring the existing proof is straightforward:
any time an element of U
is used, it must first be raised back to its original universe,
and any time an element of U
is produced, it must be lowered down to the desired universe.
U : Set
U = Lower (∀ (X : Set) → (℘ (℘ X) → X) → ℘ (℘ X))
τ : ℘ (℘ U) → U
τ t = lower (λ X f p → t (λ x → p (f (raise x X f))))
σ : U → ℘ (℘ U)
σ s = raise s U τ
Again, the complete proof can be found at HurkensLower.html.
One final thing to note is that impredicativity (with respect to function types) of Set
isn’t used either;
all of this code type checks in Agda, whose universe Set
is not impredicative.
This means that impredicativity with respect to strong pair types alone is sufficient for inconsistency.
Unrestricted Large Elimination of Impredicative Universes
In contrast to strong pairs, weak (impredicative) pairs don’t have first and second projections.
Instead, to use a pair, one binds its components in the body of some expression
(continuing our use of an impredicative Set
).
Γ ⊢ p : Σx: A. B
Γ, x: A, y: B ⊢ e : C
Γ ⊢ C : Set
────────────────────────────
Γ ⊢ let (x, y) := p in e : C
The key difference is that the type of the expression must live in Set
, and not in any arbitrary universe.
Therefore, we can’t generally define our own first projection function, since A
might not live in Set
.
Weak impredicative pairs can be generalized to inductive types in an impredicative universe, where the restriction becomes disallowing arbitrary large elimination to retain consistency. This appears in the typing rule for case expressions on inductives.
Γ ⊢ t : I p… a…
Γ ⊢ I p… : (y: u)… → 𝒰
Γ, y: u, …, x: I p… a… ⊢ P : 𝒰'
elim(𝒰, 𝒰') holds
< other premises omitted >
───────────────────────────────────────────────────────────────
Γ ⊢ case t return λy…. λx. P of [c x… ⇒ e]… : P[y… ↦ a…][x ↦ t]
The side condition elim(𝒰, 𝒰')
holds if:
𝒰 = Set₁
or higher; or𝒰 = 𝒰' = Set
; or𝒰 = Set
and Its constructors’ arguments are either forced or have types living in
Set
; and  The fullyapplied constructors have orthogonal types; and
 Recursive appearances of the inductive type in the constructors’ types are syntactically guarded.
 Its constructors’ arguments are either forced or have types living in
The three conditions of the final case come from the rules for definitionally proofirrelevant Prop
^{4};
the conditions that Coq uses are that the case target’s inductive type must be a singleton or empty,
which is a subset of those three conditions.
As the pair constructor contains a nonforced, potentially nonSet
argument in the first component,
impredicative pairs can only be eliminated to terms whose types are in Set
,
which is exactly what characterizes the weak impredicative pair.
On the other hand, allowing unrestricted large elimination lets us define not only strong impredicative pairs,
but also Lower
(and the projection raise
), both as inductive types.
While impredicative functions can Churchencode weak impredicative pairs, they can’t encode strong ones.
Σx: A. B ≝ (P : Set) → ((x : A) → B → P) → P
If Set
is impredicative then the pair type itself lives in Set
,
but if A
lives in a larger universe, then it can’t be projected out of the pair,
which requires setting P
as A
.
Other Paradoxes
There’s a variety of other features that yield inconsistencies in other ways, some of them resembling the settheoretical Russell’s paradox.
Negative Inductive Types
A negative inductive type is one where the inductive type appears to the left of an odd number of arrows in a constructor’s type. For instance, the following definition will allow us to derive an inconsistency.
record Bad : Set where
constructor mkBad
field bad : Bad → ⊥
open Bad
The field of a Bad
essentially contains a negation of Bad
itself (and I believe this is why this is considered a “negative” type).
So when given a Bad
, applying it to its own field, we obtain its negation.
notBad : Bad → ⊥
notBad b = b.bad b
Then from the negation of Bad
we construct a Bad
, which we apply to its negation to obtain an inconsistency.
bottom : ⊥
bottom = notBad (mkBad notBad)
Positive Inductive Types
This section is adapted from Why must inductive types be strictly positive?.
A positive inductive type is one where the inductive type appears to the left of an even number of arrows in a constructor’s type.
(Two negatives cancel out to make a positive, I suppose.)
If it’s restricted to appear to the left of no arrows (0 is an even number), it’s a strictly positive inductive type.
Strict positivity is the usual condition imposed on all inductive types in Coq.
If instead we allow positive inductive types in general, when combined with an impredicative universe (we’ll use Set
again),
we can define an inconsistency corresponding to Russell’s paradox.
{# NO_POSITIVITY_CHECK #}
record Bad : Set₁ where
constructor mkBad
field bad : ℘ (℘ Bad)
From this definition, we can prove an injection from ℘ Bad
to Bad
via an injection from ℘ Bad
to ℘ (℘ Bad)
defined as a partiallyapplied equality type.
f : ℘ Bad → Bad
f p = mkBad (_≡ p)
fInj : ∀ {p q} → f p ≡ f q → p ≡ q
fInj {p} fp≡fq = subst (λ p≡ → p≡ p) (badInj fp≡fq) refl
where
badInj : ∀ {a b} → mkBad a ≡ mkBad b → a ≡ b
badInj refl = refl
Evidently an injection from a powerset of some X
to X
itself should be an inconsistency.
However, it doesn’t appear to be provable without using some sort of impredicativity.
(We’ll see.)
Coquand and Paulin^{5} use the following definitions in their proof, which does not type check without typeintype,
since ℘ Bad
otherwise does not live in Set
.
In this case, weak impredicative pairs would suffice, since the remaining definitions can all live in the same impredicative universe.
P₀ : ℘ Bad
P₀ x = Σ[ P ∈ ℘ Bad ] x ≡ f P × ¬ (P x)
x₀ : Bad
x₀ = f P₀
From here, we can prove P₀ x₀ ↔ ¬ P₀ x₀
. The rest of the proof can be found at Positivity.html.
Impredicativity + Excluded Middle + Large Elimination
Another typetheoretic encoding of Russell’s paradox is Berardi’s paradox^{6}. It begins with a retraction, which looks like half an isomorphism.
record _◁_ {ℓ} (A B : Set ℓ) : Set ℓ where
constructor _,_,_
field
ϕ : A → B
ψ : B → A
retract : ψ ∘ ϕ ≡ id
open _◁_
We can easily prove A ⊲ B → A ⊲ B
by identity.
If we postulate the axiom of choice, then we can push the universal quantification over A ⊲ B
into the existential quantification of A ⊲ B
,
yielding a ϕ
and a ψ
such that ψ ∘ ϕ ≡ id
only when given some proof of A ⊲ B
.
However, a retraction of powersets can be stipulated out of thin air using only the axiom of excluded middle.
record _◁′_ {ℓ} (A B : Set ℓ) : Set ℓ where
constructor _,_,_
field
ϕ : A → B
ψ : B → A
retract : A ◁ B → ψ ∘ ϕ ≡ id
open _◁′_
postulate
EM : ∀ {ℓ} (A : Set ℓ) → A ⊎ (¬ A)
t : ∀ {ℓ} (A B : Set ℓ) → ℘ A ◁′ ℘ B
t A B with EM (℘ A ◁ ℘ B)
...  inj₁ ℘A◁℘B =
let ϕ , ψ , retract = ℘A◁℘B
in ϕ , ψ , λ _ → retract
...  inj₂ ¬℘A◁℘B =
(λ _ _ → ⊥) , (λ _ _ → ⊥) , λ ℘A◁℘B → ⊥elim (¬℘A◁℘B ℘A◁℘B)
This time defining U
to be ∀ X → ℘ X
, we can show that ℘ U
is a retract of U
.
Here, we need an impredicative Set
so that U
can also live in Set
and so that U
quantifies over itself as well.
Note that we project the equality out of the record while the record is impredicative,
so putting _≡_
in Set
as well will help us avoid large eliminations for now.
projᵤ : U → ℘ U
projᵤ u = u U
injᵤ : ℘ U → U
injᵤ f X =
let _ , ψ , _ = t X U
ϕ , _ , _ = t U U
in ψ (ϕ f)
projᵤ∘injᵤ : projᵤ ∘ injᵤ ≡ id
projᵤ∘injᵤ = retract (t U U) (id , id , refl)
Now onto Russell’s paradox.
Defining _∈_
to be projᵤ
and letting r ≝ injᵤ (λ u → ¬ u ∈ u)
,
we can show a curious inconsistent statement.
r∈r≡r∉r : r ∈ r ≡ (¬ r ∈ r)
r∈r≡r∉r = cong (λ f → f (λ u → ¬ u ∈ u) r) projᵤ∘injᵤ
To actually derive an inconsistency, we can derive functions r ∈ r → (¬ r ∈ r)
and (¬ r ∈ r) → r ∈ r
using substitution,
then prove falsehood the same way we did for negative inductive types.
However, the predicate in the substitution is Set → Set
, which itself has type Set₁
,
so these final steps do require unrestricted large elimination.
The complete proof can be found at Berardi.html.
Unrestricted Large Elimination (again)
Having impredicative inductive types that can be eliminated to large types can yield an inconsistency
without having to go through Hurkens’ paradox.
To me, at least, this inconsistency is a lot more comprehensible.
This time, we use an impredicative representation of the ordinals^{7},
prove that they are wellfounded with respect to some reasonable order on them,
then prove a falsehood by providing an ordinal that is obviously not wellfounded.
This representation can be type checked using Agda’s NO_UNIVERSE_CHECK
pragma,
and normally it would live in Set₁
due to one constructor argument type living in Set₁
.
{# NO_UNIVERSE_CHECK #}
data Ord : Set where
↑_ : Ord → Ord
⊔_ : {A : Set} → (A → Ord) → Ord
data _≤_ : Ord → Ord → Set where
↑s≤↑s : ∀ {r s} → r ≤ s → ↑ r ≤ ↑ s
s≤⊔f : ∀ {A} {s} f (a : A) → s ≤ f a → s ≤ ⊔ f
⊔f≤s : ∀ {A} {s} f → (∀ (a : A) → f a ≤ s) → ⊔ f ≤ s
An ordinal is either a successor ordinal, or a limit ordinal.
(The zero ordinal could be defined as a limit ordinal.)
Intuitively, a limit ordinal ⊔ f
is the supremum of all the ordinals returned by f
.
This is demonstrated by the last two constructors of the preorder on ordinals:
s≤⊔f
states that ⊔ f
is an upper bound of all the ordinals of f
,
while ⊔f≤s
states that it is the least upper bound.
Finally, ↑s≤↑s
is simply the monotonicity of taking the successor of an ordinal with respect to the preorder.
It’s possible to show that ≤
is indeed a preorder by proving its reflexivity and transitivity.
s≤s : ∀ {s : Ord} → s ≤ s
s≤s≤s : ∀ {r s t : Ord} → r ≤ s → s ≤ t → r ≤ t
From the preorder we define a corresponding strict order.
_<_ : Ord → Ord → Set
r < s = ↑ r ≤ s
In a moment, we’ll see that <
can be proven to be wellfounded,
which is equivalent to saying that in that there are no infinite descending chains.
Obviously, for there to be no such chains, <
must at minimum be irreflexive — but it’s not!
There is an ordinal that is strictly less than itself,
which we’ll call the “infinite” ordinal,
defined as the limit ordinal of all ordinals,
which is possible due to the impredicativity of Ord
.
∞ : Ord
∞ = ⊔ (λ s → s)
∞<∞ : ∞ < ∞
∞<∞ = s≤⊔f (λ s → s) (↑ ∞) s≤s
To show wellfoundedness, we use an accessibility predicate,
whose construction for some ordinal s
relies on showing that all smaller ordinals are also accessible.
Finally, wellfoundness is defined as a proof that all ordinals are accessible,
using a lemma to extract accessibility of all smaller or equal ordinals.
record Acc (s : Ord) : Set where
inductive
pattern
constructor acc
field
acc< : (∀ r → r < s → Acc r)
accessible : ∀ (s : Ord) → Acc s
accessible (↑ s) = acc (λ { r (↑s≤↑s r≤s) → acc (λ t t<r → (accessible s).acc< t (s≤s≤s t<r r≤s)) })
accessible (⊔ f) = acc (λ { r (s≤⊔f f a r<fa) → (accessible (f a)).acc< r r<fa })
But wait, we needed impredicativity and large elimination. Where is the large elimination?
It turns out that it’s hidden within Agda’s patternmatching mechanism.
Notice that in the limit case of accessible
, we only need to handle the s≤⊔f
case,
since this is the only case that could possibly apply when the left side is a successor and the right is an ordinal.
However, if you were to write this in plain CIC for instance,
you’d need to first explicitly show that the order could not be either of the other two constructors,
requiring showing that the successor and limit ordinals are provably distinct
(which itself needs large elimination, although this is permissible as an axiom),
then due to the proof architecture show that if two limit ordinals are equal, then their components are equal.
This is known as injectivity of constructors.
Expressing this property for ordinals requires large elimination,
since the first (implicit) argument of limit ordinals are in Set
.
You can see how it works explicitly by writing the same proof in Coq,
where the above steps correspond to inversion followed by dependent destruction,
then printing out the full term.
The s≤⊔f
subcase of the ⊔ f
case alone spans 50 lines!
In any case, we proceed to actually deriving the inconsistency, which is easy:
show that ∞
is in fact not accessible using ∞<∞
,
then derive falsehood directly.
¬accessible∞ : Acc ∞ → ⊥
¬accessible∞ (acc p) = ¬accessible∞ (p ∞ ∞<∞)
ng : ⊥
ng = ¬accessible∞ (accessible ∞)
The complete Agda proof can be found at Ordinals.html, while a partial Coq proof of accessibility of ordinals can be found at Ordinals.html.
Relaxed Guardedness
The recursive calls of cofixpoints must be guarded by constructors,
meaning that they only appear as arguments to constructors of the coinductive type of the cofixpoint.
What’s more, the constructor argument type must be syntactically the coinductive type,
not merely a polymorphic type that’s filled in to be the coinductive type later.
If the guardedness condition is relaxed to ignore this second condition,
then we can derive an inconsistency with impredicative coinductives.
Again, we define one using NO_UNIVERSE_CHECK
, with contradictory fields.
Evidently we should never be able to construct such a coinductive.
{# NO_UNIVERSE_CHECK #}
record Contra : Set where
coinductive
constructor contra
field
A : Set
a : A
¬a : A → ⊥
¬c : Contra → ⊥
¬c = λ c → (¬a c) (a c)
However, if the type field in Contra
is Contra
itself,
then we can in fact construct one coinductively.
Here, we use NON_TERMINATING
to circumvent Agda’s perfectly correct guardedness checker,
but notice that the recursive call is inside of contra
and therefore still “guarded”.
This easily leads to an inconsistency.
{# NON_TERMINATING #}
c : Contra
c = contra Contra c ¬c
ng : ⊥
ng = ¬c c
This counterexample is due to Giménez^{8} and the complete proof can be found at Coind.html.
Summary
The combinations of features that yield inconsistencies are:
 Typeintype:
· ⊢ Set : Set
 Impredicative
Set
andSet₁
where· ⊢ Set : Set₁
 Strong impredicative pairs
 Impredicative inductive types + unrestricted large elimination
 Negative inductive types
 Nonstrictlypositive inductive types + impredicativity
 Impredicativity + excluded middle + unrestricted large elimination
 Impredicative inductive types + unrestricted large elimination (again)
 Relaxed guardedness of cofixpoints
Source Files
Hurkens' paradox using typeintype: Hurkens.html
Hurkens' paradox using Lower
: HurkensLower.html
Russell's paradox using a positive inductive type and impredicative pairs: Positivity.html
Berardi's paradox using impredicativity, excluded middle, and large elimination: Berardi.html
Nonwellfoundedness of impredicative ordinals: Ordinals.html
Accessibility of ordinals: Ordinals.html
Relaxed guardedness: Coind.html

Antonius J. C. Hurkens (TLCA 1995). A Simplification of Girard’s Paradox. ᴅᴏɪ: 10.1007/BFb0014058. ↩

Thierry Coquand. (INRIA 1986). An Analysis of Girard’s Paradox. https://hal.inria.fr/inria00076023. ↩

Cesare Burali–Forti. (RCMP 1897). Una questione sui numeri transfini. ᴅᴏɪ: 10.1007/BF03015911. ↩

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau. (POPL 2019). Definitional ProofIrrelevance without K. ᴅᴏɪ: 10.1145/3290316. ↩

Theirry Coquand, Christine PaulinMohring. (COLOG 1988). Inductively defined types. ᴅᴏɪ: 10.1007/3540523359_47. ↩

Franco Barbanera, Stefano Berardi. (JFP 1996). Proofirrelevance out of excluded middle and choice in the calculus of constructions. ᴅᴏɪ: 10.1017/S0956796800001829. ↩

Frank Pfenning, Christine PaulinMohring. (MFPS 1989). Inductively defined types in the Calculus of Constructions. ᴅᴏɪ: 10.1007/BFb0040259. ↩

Eduardo Giménez. (TYPES 1994). Codifying guarded definitions with recursive schemes. ᴅᴏɪ: 10.1007/3540605797_3. ↩