Prop := Sort 0 Motivation

Stream: new members

[Lucas Teixeira]

What's the motivation for having Prop be at the bottom of the universe hierarchy??

[Lucas Teixeira]

Is it that so we cannot create a type who's type is Prop?? Would a type who's type is Prop undermine the proposition as type idea??

[Martin Dvořák]

Are you talking about creating a term x such that x : Prop or something else?

[Martin Dvořák]

As for Prop, it is a type and thus a term — it must have a type. It is Prop : Type in fact.

[Martin Dvořák]

Afaik the last thing can be translated as Sort 0 : Type 0 but I never worked with Lean on such an abstract level, so please, wait for others' response.

[Lucas Teixeira]

It would seem to me that since Prop is at the bottom of the hiearchy, any x : Prop cannot themselves be a type to something

[Martin Dvořák]

I can do def a := false and the Lean Infoview shows me a : Prop so it seems legit.

[Martin Dvořák]

I think there is no paradox. We have false : Prop and Prop : Type as well as we have e.g. 3 : int and int : Type which seems perfectly natural.

[Kyle Miller]

I think the motivation is to have Prop be in the universe hierarchy at all (and of course Prop needs a type as well -- may as well be Type). Long ago, it used to be that Type 0 = Prop to make it convenient to have universe-polymorphic definitions, but that had the wrinkle that inductive data types used the universe max 1 u. There was a proposal to split off Prop from the universe hierarchy because this was apparently annoying (all of this happened before I started learning Lean), but then Floris suggested introducing Sort (u + 1) = Type u with Sort 0 = Prop. That way we can still have universe-polymorphic definitions that allow things to be either a Type u or a Prop. https://github.com/leanprover/lean/issues/1341

[Kyle Miller]

I'm not fully understanding your question, though. Prop is a universe of types, each type is called a proposition, and the terms of those types are called proofs.

[Lucas Teixeira]

Martin Dvořák
But given a: Prop can you have a y s.t. y: a??

It would seem to me that if x : Prop there does not exist a y : x
since that would imply that there exists u that Sort(u + 1) = Sort 0

[Johan Commelin]

You can have h : P and P : Prop. Then h is a witness that P is a true proposition.

[Johan Commelin]

There is a u such that Type 0 = Sort (u+1).

[Johan Commelin]

Prop = Sort 0, and Type = Type 0 = Sort 1.

[Johan Commelin]

Not all types have the same type. Does that observation help?

[Lucas Teixeira]

Johan Commelin It's helping, but I'm not quite there yet.
So my understanding is that

Prop : (Type = Sort 0)
Type : (Type 0 = Sort 1)

Let's assume there's a proof called P of type Prop (or in other words, that P inhabits Prop)
Now let's say that P was itself a proposition (or in other words an inhabitable type), and for the sake of demonstration there was an x which inhabited that type, it seems like that would imply that

P : (Prop = Sort 0)
 x : (P  = Sort -1)

which to my (limited) understanding isn't a thing

[Martin Dvořák]

My intuition struggles with that concept that we have false : Prop and also P : Prop however they feel fundamentally different.

[Kevin Buzzard]

Does this help? https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/

[Martin Dvořák]

Of course, both false and P are terms; however, only P is a type, and so, we can have h : P but f : false would be a nonsense.

[Reid Barton]

It should be Type : Type 1 not Type : Type 0. But the error is that just because Prop : Type, it doesn't mean there aren't other things of type Type, like nat : Type. Likewise, Sort (-1) : (Sort 0 = Prop) doesn't exist but there are still other things of type Prop, like true : Prop.

[Martin Dvořák]

What if we go higher? Is there any x : Type 2 apart from x = Type 1 of course?

[Johan Commelin]

Lucas Teixeira said:

So my understanding is that

Prop : (Type = Sort 0)

which to my (limited) understanding isn't a thing

Nope, Type = Sort 1

[Johan Commelin]

@Martin Dvořák sure, stuff like x = {T : Type | nonempty T}

[Johan Commelin]

and many other constructions that quantify over Type

[Martin Dvořák]

Oh I see. We can also have f := Type → Type and then f : Type 2 which is the same level as in your example.

[Lucas Teixeira]

Johan Commelin

Okay so

(Prop = Sort  0) : (Type = Sort 1)

Doesn't that leave the whole inhabitants of Sort 0 being of type Sort -1 conundrum unresolved??

P : (Prop = Sort 0)
 x : (P  = Sort -1)

[Kevin Buzzard]

Why don't you check your work before posting Martin?

def f := Type → Type

#check f

[Kevin Buzzard]

@Lucas there is no such thng as Sort -1. Does this help?

[Martin Dvořák]

Kevin Buzzard said:

Why don't you check your work before posting Martin?

def f := Type → Type

#check f

I did. Exactly this. I just wanted to post for clarification if others read it after us.

[Kevin Buzzard]

So it's Type 1 not Type 2, right?

[Martin Dvořák]

[this comment is no longer relevant]

[Kyle Miller]

@Lucas Teixeira In type theory, everything has a single type. For example, 5 has the type ℕ, and ℕ has the type Type 0. There are two synonyms for Type 0: Type and Sort 1. (In general, the type of a type is Sort 0, or Sort 1, or Sort 2, or ...)

We don't say that 5 : Type -1 -- the type of 5 is ℕ. Similarly, if x : P and P : Sort 0, we don't say x : Sort -1, since x : P and that's that.

[Kyle Miller]

Lucas Teixeira said:

Let's assume there's a proof called P of type Prop (or in other words, that P inhabits Prop)
Now let's say that P was itself a proposition (or in other words an inhabitable type)

"a proof called P of type Prop" doesn't make sense. If P has type Prop, it's called a proposition, not a proof.

"or in other words an inhabitable type": all propositions are inhabitable (they are types). If a proposition is inhabited, a term that inhabits it is called a proof of that proposition.

Here's what characterizes these Sort u universes: they are the type of the type of something. A proposition is not the type of the type of something -- at most it's the type of something (a proof).

[Johan Commelin]

@Lucas Teixeira With types it is turtles all the way up. So 3 : int and int : Type and Type : Type 1 and Type n : Type (n+1).
Similarly trivial : true and true : Prop and Prop : Type and Type : Type 1 etc...

But it is not turtles all the way down! Just because Type : Type 1 and Prop : Type and P : Prop and possibly h : P (which is a proof witness of the proposition P), this doesn't mean that you can sensibly treat h as a type, and ask for x : h.

[Lucas Teixeira]

Kevin Buzzard said:

@Lucas there is no such thng as Sort -1. Does this help?

Yes, that was my intuition. If I were to reformulate my original question I would ask: Is the reason Prop := Sort 0 rather then Prop := Sort 1 is because Prop:= Sort 1 would lead to a situation where the inhabitants of Prop would themselves have inhabitants and that suggest a non-sensical heuristic of proofs (inhabitants of Prop) are themselves propositions (types) which can be proved (inhabited)

It was more of a questions regarding the design motivations behind the Prop syntactic sugaring than type theory itself

[Johan Commelin]

To continue with the turtles. If you have some random X : Type 5, then you can talk about x : X. But you cannot talk about y : x.
Except in the very special case where X = Type 4. Because then x would be a type, and so you can talk about its terms.

[Johan Commelin]

So even if you start with X : Type 5, this does not mean that you can go 5 turtles down. Almost always, you can only go 2 turtles down: from Type 5 to X, and from X to x.

[Kyle Miller]

Lucas Teixeira said:

Prop:= Sort 1 would lead to a situation where the inhabitants of Prop would themselves have inhabitants

A reason you're getting answers about type theory is because statements like this suggest a misunderstanding -- true is an inhabitant of Prop that itself has an inhabitant (trivial), so this is already the case.

[Reid Barton]

a situation where the inhabitants of Prop would themselves have inhabitants and that suggest a non-sensical heuristic of proofs (inhabitants of Prop) are themselves propositions (types) which can be proved (inhabited)

The inhabitants of Prop are propositions, and they do have inhabitants (proofs).

[Reid Barton]

That's the reason to consider Prop as belonging to the same family as Type (and Type 1, etc.) at all.

[Kyle Miller]

(I do wonder how propext and proof irrelevance would work if there were a "Sort -1". Maybe trivial would have to be a type?)

[Kevin Buzzard]

One could imagine a different (and much easier to understand for beginners) set-up where there were three classes of things: terms (which are not types), types (which are not universes) and Universes (which have no type). Then Sort 0 = Prop, Sort 1 = Type, Sort 2, Sort 3 ... are your universes, types have type a Sort, and terms have type a type. The only reason that it is not like this is because that everything has to have a type in type theory, so we arbitrarily let Sort n have type Sort (n+1) just to satisfy this condition. The fact that it is true does not make it useful or helpful, indeed it can make it confusing as we're seeing.

[Kevin Buzzard]

The blog post I linked to above tries to stress this point of view, term : type and type : universe, without going into this irrelevant universe : (another universe) issue.

[Kyle Miller]

@Kevin Buzzard I believe this is how (at least one version of) Automath is set up, but it only has Prop and Type.

(It has some support for higher-order theorems, but the theorems don't have types themselves. They're too big. It's like axiom schema not being axioms themselves.)

[Kevin Buzzard]

Isn't Isabelle/HOL like this?

[Lucas Teixeira]

Kyle Miller said:

Lucas Teixeira said:

Prop:= Sort 1 would lead to a situation where the inhabitants of Prop would themselves have inhabitants

A reason you're getting answers about type theory is because statements like this suggest a misunderstanding -- true is an inhabitant of Prop that itself has an inhabitant (trivial), so this is already the case.

You're right actually, I do have a misunderstanding.

trivial : true and true: (Prop = Sort 0) but it is not the case that true = Sort -1 even though it has an inhabitant.

I think my confusion comes from the difference between universes and types. Is true then a type without being a universe???

[Martin Dvořák]

Kevin Buzzard said:

The blog post I linked to above tries to stress this point of view, term : type and type : universe, without going into this irrelevant universe : (another universe) issue.

I really like how it is written. If I understand it correctly, your simplified view contains only two universes Type and Prop neither of which can stand on the left side of the colon, right?

[Kevin Buzzard]

Right -- to do a lot of mathematics (note that I am speaking to mathematicians) one only needs these two universes.

[Kyle Miller]

Lucas Teixeira said:

I think my confusion comes from the difference between universes and types. Is true then a type without being a universe???

Yes

[Kevin Buzzard]

@Lucas Teixeira true is a true-false statement, so it's a proposition (a true one, like 2+2=4 is a true proposition). In particular it is at the "type" level of the three-level heirarchy (term/type/universe) which I'm urging you to take on board, so it is a type but not a universe, yes. Its type is Prop, which is a universe. It has a term trivial, which is its proof.

[Reid Barton]

Lucas Teixeira said:

You're right actually, I do have a misunderstanding.

trivial : true and true: (Prop = Sort 0) but it is not the case that true = Sort -1 even though it has an inhabitant.

I think my confusion comes from the difference between universes and types. Is true then a type without being a universe???

0 : nat and nat : Type but it isn't the case that nat = Prop either.

[Martin Dvořák]

Lucas Teixeira said:

You're right actually, I do have a misunderstanding.

trivial : true and true: (Prop = Sort 0) but it is not the case that true = Sort -1 even though it has an inhabitant.

Well, you see, we have trivial : true and true : Prop where Prop = Sort 0 without having true = Sort -1. In a similar manner, we have 3 : int and int : Type where Type = Sort 1 without having int = Sort 0.

[Kevin Buzzard]

(noting again that Sort -1 doesn't exist)

[Lucas Teixeira]

Kevin Buzzard said:

The blog post I linked to above tries to stress this point of view, term : type and type : universe, without going into this irrelevant universe : (another universe) issue.

Noted, I'll check it out. Thanks everyone for being so helpful!

Here's my understanding so far

1. All terms have a type
2. Not all types are universes
3. Universes are expressed in Sort u (or some syntactic sugaring of it, such as Prop or Type u)

And what I feel to be true but still not 100% on

4. All types have a universe
5. All Universes are types

[Kyle Miller]

If "all types have a universe" means "the type of a type is a universe", then looks good to me.

[Martin Dvořák]

Lucas Teixeira said:

4. All types have a universe
5. All Universes are types

I read (4) as "all types belong to a universe".

[Kyle Miller]

Kevin Buzzard said:

In particular it is at the "type" level of the three-level hierarchy (term/type/universe) which I'm urging you to take on board

I just dug up the terminology for this from an automath paper, to support this viewpoint (and if it worked for de Bruijn and the automath project, it's probably good pedagogically!).

Every expression has a degree, which is 1, 2, or 3. Their meanings (translated to Lean):

1. Type and Prop (universes)
2. types and propositions
3. terms and proofs

The type of something of degree 3 is something of degree 2, and the type of something of degree 2 is something of degree 1.

[Kyle Miller]

(@Lucas Teixeira Maybe a way to say what's going on (using this terminology) is that you were thinking the u in Sort u had to do with the degree of an expression, but degree and universe level end up being orthogonal concepts. Each Sort u is of degree 1.)

[Martin Dvořák]

(deleted)

[Kevin Buzzard]

"all types belong to a universe"

This is not set theory, so there is no "belong" or "element of" here. The type of each type is a universe.

[Martin Dvořák]

Kevin Buzzard said:

"all types belong to a universe"

This is not set theory, so there is no "belong" or "element of" here. The type of each type is a universe.

Oh yes. However, reading "type of each type" brings a risk of developing a headache, and so, I decided to overload the word "belongs" for : in addiction to the standard meaning of expressing ∈ in plain English. Can we agree on that? Or is my word use misleading?

[Kyle Miller]

Unfortunately Lean has ∈, too, so it can be confusing.

[Martin Dvořák]

The concept of degrees (1, 2, 3) is pretty neat. Thank you @Kyle Miller ! We can also observe that bool and Prop occupy different degrees in your hierarchy (2 and 1, respectively).

So informally, we have tt : bool : Type and trivial : true : Prop. Specifically, note that tt and true are on different degrees (3 and 2, respectively). This explains why we can speak of true being inhabited (by the term trivial as a matter of fact), whereäs speaking of tt being inhabited would be a nonsense. Also, apart from true and false many other terms can be of the type Prop which also confirms the well-known rule of thumb that we cannot do by_cases on P : Prop while we could happily do by_cases on b : bool as it can have only the two expected values (tt : bool or ff : bool).

This is in contrast to Lean's typesystem, where both tt and true are outside of the Sort u hierarchy, and moreover, both the grandfather of tt and the grandfather of true are precisely Sort 1. From this point of view, they might seem to be equivalent, which they aren't.

So, for these purposes (and for thinking inside my head, generally), your concept of degrees is more useful than the concept of levels. Did I put everything right?

[Kyle Miller]

To be clear, this is not my hierarchy in any way -- it's what Kevin was talking about and I just pulled out de Bruijn's terminology of "degree." It seems to make it easier to help keep the degree hierarchy and the universe level hierarchy straight.

Here's a diagram that's come to mind due to this discussion, illustrating the types you mention and also a type up in Type 1:

image.png

[Kyle Miller]

Degree does seem to be the fundamental notion. Universe levels are, as I understand it, a particular solution to some technical problems (making sure everything, including universes, has a type, doing so without introducing paradoxes, being able to give universe-polymorphic definitions, and having a practical universe inference system).

[Martin Dvořák]

Very nice, thanks!

[Lucas Teixeira]

Kyle Miller said:

(Lucas Teixeira Maybe a way to say what's going on (using this terminology) is that you were thinking the u in Sort u had to do with the degree of an expression, but degree and universe level end up being orthogonal concepts. Each Sort u is of degree 1.)

Yes! That sums up my confusion pretty well