Paradoxes and Type Universes

Stream: Type theory

[Jonathan Lacombe]

I am learning about type theory and I keep reading that it's necessary to add a universe hierarchy to type systems to avoid paradoxes that come from allowing (Type: Type). However, I've never seen a clear and simple example of such a paradox.

I don't know how one would make a proposition of Russell's paradox in type theory. I'm assuming that's because Set theory and Type theory are fundamentally different.

I also hear a lot about the Burali-Forti's paradox, but I don't know what an Ordinal is and how to even define that type or what would be the proposition for the paradox.

Is there a clear and simple example of proving False/Null from a type theory that does not have a universe hiearchy, where the type of Type is Type?

And would such an example require recursion / induction? That is, do all of these paradoxes have to do with recursively defined things? The nlab article on Burali-Forti's paradox says that (Type: Type) is inconsistent because it contains non-normalizing proofs of False. In that case, does that mean a proof of False is always through infinite recursion?

Really, I expect that there exist some type in lean that's something like

Example.{u, v = u + 1} (A: Type u) (B: Type v) ....

that doesn't lead to any inconsistencies, but if it was

Example.{u} (A: Type u) (B: Type u) ...

or without universes

Example (A: Type) (B: Type) ...

then it would clearly lead to proving False in an inconsistent type theory, and fail type checking in lean.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

One type-theoretic analogue of Russell's paradox is Girard's paradox. It is here in mathlib.

[Jonathan Lacombe]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

One type-theoretic analogue of Russell's paradox is Girard's paradox. It is here in mathlib.

Well, this just looks like gibberish to me. But I'll try to go through it anyway.

[Paul Reichert]

The following Russell-like argument should also work assuming LEM and Sigma types (one kind of inductive types):

• Define σ : Type := (α : Type) × α.
• There's an injective function k : (σ → Prop) → σ := fun P => ⟨σ, P⟩ k : (σ → Prop) → σ := fun P => ⟨σ → Prop, P⟩. (Looks already bad!)
• Define Q : σ → Prop := fun b => ∃ P, k P = b ∧ ¬ P b(Think of this as the set of sets that don't contain themselves.)
• If Q (k Q), then there's P with k P = k Q and ¬ P (k Q). But k is injective, so ¬ Q (k Q). Contradiction.
• If ¬ Q (k Q), then choose P := Q and then k P = k Q and ¬ P (k Q), so that Q (k Q) holds by definition. Contradiction.

[Chris Hughes]

see docs#Function.not_surjective_Type for a proof that there is no surjection from α : Type into Type, which also shows why Type : Type would be inconsistent (because the identity function is surjective).

[suhr]

Jonathan Lacombe said:

Well, this just looks like gibberish to me. But I'll try to go through it anyway.

Here are some papers to read:

• https://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf
• https://www.cse.chalmers.se/~coquand/geuvers.pdf

See also https://ionathan.ch/2021/11/24/inconsistencies.html

[Jonathan Lacombe]

Paul Reichert said:

The following Russell-like argument should also work assuming LEM and Sigma types (one kind of inductive types):

• Define σ : Type := (α : Type) × α.
• There's an injective function k : (σ → Prop) → σ := fun P => ⟨σ, P⟩. (Looks already bad!)

I am actually getting stuck on this definition of k. If σ is defined as Sigma Type (λ (α : Type) => α) and k : (σ → Prop) → σ := fun (P: σ → Prop) => ⟨σ, P⟩ then wouldn't ⟨σ, P⟩ need to have type σ so that (fst: Type) = σ and (snd: B σ) where B := λ (α : Type) => α and so wouldn't (snd: σ) = Pfail the type check, since P has type σ → Prop and not σ?
For k to type check, wouldn't it need to be something like k : σ → σ := fun (P: σ) => ⟨σ, P⟩?

[Jonathan Lacombe]

suhr said:

Here are some papers to read:

Thanks

[Robin Arnez]

I think they meant k : (σ → Prop) → σ := fun P => ⟨σ → Prop, P⟩

[Paul Reichert]

Oops, sorry for the confusion. Yes, that is what I meant. Fixed it. Hopefully, it's possible to see how the argument more or less follows Russel's paradoxon. Q is meant to correspond to the set that contains all sets that do not contain themselves.

[Jonathan Lacombe]

Paul Reichert said:

Hopefully, it's possible to see how the argument more or less follows Russel's paradoxon. Q is meant to correspond to the set that contains all sets that do not contain themselves.

Yeah, this mostly makes sense to me now. I think this is exactly what I was looking for. I am getting stuck on the last two bullet points because I don't know how k being injective results in the contradiction and I also don't know what you mean by choose P := Q.

But, I did go on further and write some type theory pseudocode to see if I can get what I'm looking for.

define forward :: Q (k Q) → (Q (k Q) → Null):
    λ (p: Q (k Q)) .
        ?

define backward :: (Q (k Q) → Null) → Q (k Q):
    λ (p: Q (k Q) → Null) .
        ?

define contradiction: λ (A: Type) (a: A → Null) (b: (A → Null) → A) :: Null:
    a (b a)

define proof_of_null :: Null:
    contradiction (Q (k Q)) forward backward

I just don't know how to formulate the definitions from your last two bullet points. But also, I don't see any need to assume LEM here. Does it have to do with something in the last two bullet points that I am missing?

[Aaron Liu]

import Mathlib

axiom Bad : Type

axiom bad : (α : Type) × α ↪ Bad

noncomputable section

def k (P : Bad → Prop) : Bad :=
  bad ⟨Bad → Prop, P⟩

def Q (b : Bad) : Prop :=
  ∃ P, k P = b ∧ ¬P b

theorem k_injective : k.Injective :=
  fun _ _ hab => eq_of_heq
    (Sigma.mk.inj (bad.injective hab)).2

theorem down (h : Q (k Q)) : ¬Q (k Q) :=
  h.elim fun _ hP =>
    (congrArg Not (congrFun (k_injective hP.1) (k Q))).mp hP.2

theorem up (h : ¬Q (k Q)) : Q (k Q) :=
  ⟨Q, rfl, h⟩

theorem false : False :=
  down (up fun h => down h h) (up fun h => down h h)

-- 'false' depends on axioms: [Bad, bad]
#print axioms _root_.false

[Aaron Liu]

you indeed don't need any LEM

[Aaron Liu]

this is just the diagonal argument

[Aaron Liu]

interestingly, this is also one of those infinitely reducing proofs

-- times out
#reduce (proofs := true) _root_.false

[Aaron Liu]

by the way, this exact same proof can be used to show there can be no injective function (α → Prop) → α, which is docs#Function.cantor_injective

[Jonathan Lacombe]

Aaron Liu Yeah this is exactly what I was looking for. Thanks