Zulip Chat Archive

Stream: new members

Topic: Type : Type


view this post on Zulip Mateusz Zugaj (Jun 04 2020 at 12:48):

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.

view this post on Zulip Mateusz Zugaj (Jun 04 2020 at 12:49):

Sorry for a noob question

view this post on Zulip Jalex Stark (Jun 04 2020 at 12:52):

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

view this post on Zulip Jalex Stark (Jun 04 2020 at 12:53):

Type u has type Type (u +1)

view this post on Zulip Jalex Stark (Jun 04 2020 at 12:54):

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

view this post on Zulip Reid Barton (Jun 04 2020 at 12:56):

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.

view this post on Zulip Mateusz Zugaj (Jun 04 2020 at 12:56):

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

view this post on Zulip Mateusz Zugaj (Jun 04 2020 at 12:57):

Why there cannot be a type of all types?

view this post on Zulip Jalex Stark (Jun 04 2020 at 12:58):

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

view this post on Zulip Reid Barton (Jun 04 2020 at 13:00):

meta inductive T : Type
| mk : Type  T

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

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 13:01):

What's the shortest meta proof of false?

view this post on Zulip Reid Barton (Jun 04 2020 at 13:03):

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

view this post on Zulip Mateusz Zugaj (Jun 04 2020 at 13:33):

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

view this post on Zulip Jalex Stark (Jun 04 2020 at 13:35):

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)

view this post on Zulip Jalex Stark (Jun 04 2020 at 13:36):

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"

view this post on Zulip Reid Barton (Jun 04 2020 at 13:40):

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.

view this post on Zulip Mateusz Zugaj (Jun 04 2020 at 13:41):

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

view this post on Zulip Reid Barton (Jun 04 2020 at 13:41):

No, there really is a paradox.

view this post on Zulip Jalex Stark (Jun 04 2020 at 13:42):

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

view this post on Zulip Reid Barton (Jun 04 2020 at 13:48):

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

view this post on Zulip Reid Barton (Jun 04 2020 at 13:55):

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

view this post on Zulip Mateusz Zugaj (Jun 04 2020 at 14:12):

@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

view this post on Zulip Jalex Stark (Jun 04 2020 at 14:15):

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

view this post on Zulip Reid Barton (Jun 04 2020 at 14:18):

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.

view this post on Zulip Mateusz Zugaj (Jun 04 2020 at 14:23):

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?

view this post on Zulip Reid Barton (Jun 04 2020 at 14:34):

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.

view this post on Zulip Reid Barton (Jun 04 2020 at 14:37):

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

view this post on Zulip David Wärn (Jun 04 2020 at 15:00):

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.

view this post on Zulip Kenny Lau (Jun 04 2020 at 15:09):

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

view this post on Zulip Kenny Lau (Jun 04 2020 at 15:09):

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

view this post on Zulip Chris Hughes (Jun 04 2020 at 15:24):

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

view this post on Zulip Kenny Lau (Jun 04 2020 at 15:28):

how?

view this post on Zulip Jalex Stark (Jun 04 2020 at 15:45):

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

view this post on Zulip David Wärn (Jun 04 2020 at 16:02):

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)

view this post on Zulip Patrick Stevens (Jun 04 2020 at 16:40):

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

view this post on Zulip Patrick Stevens (Jun 04 2020 at 16:41):

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


Last updated: May 14 2021 at 07:19 UTC