Type : Type

Stream: new members

[Mateusz Zugaj]

What would happen if Type was of the type Type? I tried to make some sort of Russell's paradox out of this, but I cannot define a type T made of things that are not their own type.

[Mateusz Zugaj]

Sorry for a noob question

[Jalex Stark]

Which type are you talking about when you say Type? I think you mean Type u for some universe u

[Jalex Stark]

Type u has type Type (u +1)

[Jalex Stark]

When I type #check Type into VSCode it decides that I'm talking about Type 1

[Reid Barton]

If you use a recent enough Lean 3, I think the universe checks are disabled for meta inductive definitions, and then you can try to write your paradox.

[Mateusz Zugaj]

Yes, and I want to understand the need for "+1" in Type u : Type (u+1)

[Mateusz Zugaj]

Why there cannot be a type of all types?

[Jalex Stark]

are you asking a question about Lean's type theory or a question about type theories in general?

[Reid Barton]

meta inductive T : Type
| mk : Type → T

With a recent enough version, Lean will accept this and then you can implement the usual paradoxes.

[Kevin Buzzard]

What's the shortest meta proof of false?

[Reid Barton]

meta def a : false := a, but this isn't very exciting

[Mateusz Zugaj]

@Jalex Stark The question is about Lean's type theory, but I suppose the answer to the general question should be the same.

[Jalex Stark]

well, the answer for Lean's type theory is going to be something like "Lean requires the judgement relation : to be well-founded"
(with the caveat that I don't know whether the thing I'm saying is literally true. one can do real maths in Lean without understanding its type theory on a deep level)

[Jalex Stark]

whereas for general type theory it's going to be "well-founded judgement relations enjoy nice properties that ill-founded ones in general do not"

[Reid Barton]

I thought we had a proof in mathlib that Type (u+1) is bigger than Type u, but it's not easy to search for.

[Mateusz Zugaj]

@Jalex Stark "ill-founded ones in general do not" - so it's not like we have a paradox instantly, just some bad behaviour?

[Reid Barton]

No, there really is a paradox.

[Jalex Stark]

I was speaking mildly to avoid saying false things. Reid knows more than me and can speak more decisively.

[Reid Barton]

Although it's not super easy to see, it follows from https://github.com/leanprover-community/mathlib/blob/e397b4c/src/set_theory/ordinal.lean#L1855-L1868 that each universe has more ordinals than the previous one

[Reid Barton]

So, in Lean, you can prove not (Type u = Type (u+1)), and that should be pretty convincing that Type : Type would lead to inconsistency

[Mateusz Zugaj]

@Reid Barton Yes, that is convincing. The one more bit I'm missing is what exactly universes are, and why not u+1 = u. But that (I hope) I will learn from tutorials

[Jalex Stark]

i don't think the tutorials try to teach you that, since it's not very necessary for typical lean use cases

[Reid Barton]

I'm not sure what your background is, but for most people it's probably better to start out by taking on faith that Type : Type would lead to inconsistencies which are avoided by introducing universe levels.

[Mateusz Zugaj]

So one of my takeaways is that in ZFC it is really easy to say why the set of all sets doesn't exists, but it turns out that in type theory that it isn't so easy to say why there is not a type of all types, right?

[Reid Barton]

Yeah, somehow the global membership concept gives you easier access to these paradoxes. I guess another way to prove it in Lean should be to use its model of ZFC, and then run a proof that there is no set of all sets there.

[Reid Barton]

If you like ZFC then you may also want to think of the "intended model" of Lean as fixing a sequence $\mathcal{U}_0 \in \mathcal{U}_1 \in \cdots$ of Grothendieck universes, thinking of universe levels as external natural numbers $\{0, 1, \ldots\}$, and interpreting a type of type Type u as a set belonging to $\mathcal{U}_u$.

[David Wärn]

You should be able to derive a quick contradiction from Type : Type using Cantor?
Let K := Σ α : Type, α. Any α : Type injects into K. So assuming Type : Type, we get that set K embeds into K.

[Kenny Lau]

well Cantor's Theorem (or Russell's paradox) is that there is no surjection from A to P(A) right

[Kenny Lau]

but I guess you can noncomputably construct a surjection from an injection the other way

[Chris Hughes]

You can constructively prove there's no injection from the powerset.

[Kenny Lau]

how?

[Jalex Stark]

i think this is constructive:

given f : set \a \to \a,
make g (x : set \a) : \set \a := {a | \ex y \sub x, f y = a}

g has a least fixpoint x := \bigcup_n g^n \emptyset

f (g x) = f x \in x

since f x \in x, we must have f x \in g^n \emptyset for some finite n, contradicting injectivity

[David Wärn]

A formal proof:

import tactic

def K : Type 1 := Σ α : Type, α

def embed_sum (α : Type) : α → K := λ a, ⟨α, a⟩

lemma embed_inj (α : Type) : function.injective (embed_sum α) := by tidy

theorem cantor (α : Type) (f : set α → α)
  (inj : function.injective f) : false :=
begin
  let s := { x | ∃ t, f t = x ∧ ¬ x ∈ t },
  have not_mem : ¬ f s ∈ s,
  { intro h,
    suffices : ¬ f s ∈ s,
    { exact this h },
    rcases h with ⟨t, ht, hn⟩,
    rwa inj ht at hn, },
  have is_mem : f s ∈ s := ⟨s, rfl, not_mem⟩,
  exact not_mem is_mem,
end

-- fails due to some issue with universes...
-- theorem falso : false :=
-- cantor (set K) (embed_sum K) (embed_inj K)

[Patrick Stevens]

FWIW if you're interested in the general question of Type in Type, rather than how it applies to Lean, I found http://liamoc.net/posts/2015-09-10-girards-paradox.html very clear

[Patrick Stevens]

Although I can read Agda, so I can't promise it's readable to people who haven't spent ages learning the syntax of Agda :P