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 : Typeis 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