# Zulip Chat Archive

## Stream: new members

### Topic: Predicativity

#### Horatiu Cheval (May 18 2021 at 13:14):

Probably a very basic type theory question, but what is the purpose of the predicativity of `Type`

? What would break if

`Π α : Type, α`

were of type `Type`

instead of `Type 1`

? And what among the features distinguishing `Prop`

from `Type`

make `Prop`

admissible as an impredicative sort?

#### Kevin Buzzard (May 18 2021 at 13:19):

If Pi a : Type, a were of type Type then you will get the same kind of contradiction as Russell's paradox, where you allow the collection of all sets to be a set. I think it's called Girard's paradox in type theory. Prop is impredicative because Leo designed it that way, I'm not sure I really understand the second question.

#### Kevin Buzzard (May 18 2021 at 13:21):

Oh I see -- you're asking "how come forall a : Prop, a is allowed to be a Prop"?

#### Horatiu Cheval (May 18 2021 at 13:21):

Yes, that's right

#### Kevin Buzzard (May 18 2021 at 13:22):

You could look at https://leanprover-community.github.io/mathlib_docs/logic/girard.html and then change all the `Type u`

to Prop and see what breaks.

#### Horatiu Cheval (May 18 2021 at 13:22):

And why is it not contradictory if with `Type`

it is. It seems like the same situation

#### Kevin Buzzard (May 18 2021 at 13:29):

OK so with the set theoretic version you construct a problematic set -- the set of all sets which don't contain themselves -- and then you make a contradiction from that. The key thing is that the contradiction involves constructing data, which doesn't live in the Prop universe.

If you just stick to `Type`

then the Girard contradiction involves

```
F: Type → Type := λ (X : Type), (set (set X) → X) → set (set X)
U: Type := pi F
```

If you try this with `X : Prop`

then Lean chokes at `set X`

.

#### David Wärn (May 18 2021 at 13:30):

As I understand it, `Type : Type`

is contradictory because `Type`

is too big, e.g. it should have strictly more elements than any `A : Type`

. Similarly whenever you construct some type by referring to all `A : Type`

, there is a risk that the result is too big, so can't be in `Type`

. (Actually `Π α : Type, α`

is not too big, since it's empty.) This is *not* true when you construct a `Prop`

by referring to all `A : Type`

: the resulting prop can only have one element, so classically it's `true`

or `false`

. So you shouldn't expect an impredicative `Prop`

to be contradictory.

#### Kevin Buzzard (May 18 2021 at 13:33):

```
#check λ (X : Prop), (((X → Prop) → Prop) → X) → ((X → Prop) → Prop) -- Prop → Type
#check λ (X : Type), (((X → Prop) → Prop) → X) → ((X → Prop) → Prop) -- Type → Type
#check λ (X : Type u), (((X → Prop) → Prop) → X) → ((X → Prop) → Prop) -- Type u → Type u
```

So here explicitly is where the Girard proof breaks. I've replaced `set X`

with `X -> Prop`

. The trick doesn't work with Prop as the target is data.

#### Kevin Buzzard (May 18 2021 at 13:34):

Of course the _proof_ that an impredicative Prop isn't contradictory is that Lean's type theory is equiconsistent with ZFC + universes!

#### Horatiu Cheval (May 18 2021 at 13:57):

Thank you both for the great clarifications!

Last updated: Dec 20 2023 at 11:08 UTC