Predicativity

Stream: new members

[Horatiu Cheval]

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]

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]

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

[Horatiu Cheval]

Yes, that's right

[Kevin Buzzard]

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]

And why is it not contradictory if with Type it is. It seems like the same situation

[Kevin Buzzard]

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]

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]

#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]

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

[Horatiu Cheval]

Thank you both for the great clarifications!