While itβs rather difficult to accidentally prove an inconsistency in a well-meaning 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 type-theoretical formulation of the set-theoretical 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 well-known inconsistent features.

### Type in Type

The most common mechanization of Hurkensβ paradox you can find online is using type-in-type,
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 type-in-type 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 `-impredicative-set`

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 type-in-type 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 type-in-type, despite never actually exploiting it.
If we really want to make sure we really never make use of type-in-type,
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 fully-applied 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 proof-irrelevant `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 non-forced, potentially non-`Set`

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 Church-encode 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 set-theoretical 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 partially-applied 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 type-in-type,
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 type-theoretic 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 well-founded with respect to some reasonable order on them,
then prove a falsehood by providing an ordinal that is obviously *not* well-founded.
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 pattern-matching 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:

- Type-in-type:
`Β· β’ Set : Set`

- Impredicative
`Set`

and`Setβ`

where`Β· β’ Set : Setβ`

- Strong impredicative pairs
- Impredicative inductive types + unrestricted large elimination
- Negative inductive types
- Non-strictly-positive 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 type-in-type: 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

## References

[1] Hurkens, Antonius J. C. (TLCA 1995). *A Simplification of Girardβs Paradox*. α΄
α΄Ιͺ:10.1007/BFb0014058.

[2] Coquand, Thierry. (INRIA 1986). *An Analysis of Girardβs Paradox*. https://hal.inria.fr/inria-00076023.

[3] BuraliβForti, Cesare. (RCMP 1897). *Una questione sui numeri transfini*. α΄
α΄Ιͺ:10.1007/BF03015911.

[4] Gilbert, GaΓ«tan; Cockx, Jesper; Sozeau, Matthieu; Tabareau, Nicolas. (POPL 2019). *Definitional Proof-Irrelevance without K*. α΄
α΄Ιͺ:10.1145/3290316.

[5] Coquand, Theirry; Paulin, Christine. (COLOG 1988). *Inductively defined types*. α΄
α΄Ιͺ:10.1007/3-540-52335-9_47.

[6] Barbanera, Franco; Berardi, Stefano. (JFP 1996). *Proof-irrelevance out of excluded middle and choice in the calculus of constructions*. α΄
α΄Ιͺ:10.1017/S0956796800001829.

[7] Pfenning, Frank; Christine, Paulin-Mohring. (MFPS 1989). *Inductively defined types in the Calculus of Constructions*. α΄
α΄Ιͺ:10.1007/BFb0040259.

[8] GimΓ©nez, Eduardo. (TYPES 1994). *Codifying guarded definitions with recursive schemes*. α΄
α΄Ιͺ:10.1007/3-540-60579-7_3.