Existential quantifier and first projection

Stream: new members

[Martin C. Martin]

Exists isn't built in, but defined in core. The definition is equivalent to:

inductive Exists {α : Sort u} (q : α → Prop) : Prop
| intro : ∀ (a : α), q a → Exists

This is the same as the definition of sigma (or psigma), except for the extra : Prop at the end.

Because Exists lives in Prop ... this causes it to have some weird definition, where it's not a dependent product type like the sigmas, and you can't extract the witness (first argument to constructor) or second argument to the constructor, whose type might include the value of the witness.

How does that work under the covers? Are there special rules for inductive types that live in Prop to enforce the "there's only zero or one object of this type"? Something about an eliminator? Do inductive types in Prop essentially not have any internal structure?

Also, I thought the type hierarchy had to be strictly increasing, in the sense that any type that depends on Sort u must live in a Sort bigger than u, to avoid Russel's paradox? Do the restrictions on inductive types living in Prop avoid this?

[Jireh Loreaux]

I'm not the person to answer this question for you, but there are two pieces of information that might be useful:

1. Lean has subsingleton elimination which is how certain specific things (like equality) can eliminate from Prop into higher universes.
2. Universe levels for Π-types use imax not max, which basically means a Π-type over a Prop is still a Prop, whereas a Π-type over something in universe Type u ends up in Type (u + 1).
3. This I think doesn't give rise to Girard's paradox (type theory equivalent of Russell's paradox) because in general (except for subsingleton types) you can't eliminate from Prop into higher universes.

Note: like I said, I'm not the right person to answer this question, so it's possible I've got something wrong in what I said above.

[Junyan Xu]

Nice explanations! Some addenda:

The two paragraphs above prior to Section 7.9, TPIL talks about subsingleton elimination (called "singleton elimination" there):

There is an exception to this last rule: we are allowed to eliminate from an inductively defined Prop to an arbitrary Sort when there is only one constructor and each constructor argument is either in Prop or an index. The intuition is that in this case the elimination does not make use of any information that is not already given by the mere fact that the type of argument is inhabited. This special case is known as singleton elimination.

Another prominent example of Prop that allows large elimination is docs#acc, which allows well-founded recursive definitions. Exists on the other hand doesn't admit large elimination and that's why you can't define the first projection. docs#classical.some is sort of a right inverse to Exists.mk, but it's not an eliminator and doesn't satisfy the computation rule.

The universe level of an inductive type is explained in Section 7.8 just above this, and for Pi types also in Section 4.1 (search for imax). This behavior of Pi type for Props is what makes Prop impredicative.

See also Some notes that covers the same topics and also mentions Girard's paradox.

[Mario Carneiro]

Martin C. Martin said:

Also, I thought the type hierarchy had to be strictly increasing, in the sense that any type that depends on Sort u must live in a Sort bigger than u, to avoid Russel's paradox? Do the restrictions on inductive types living in Prop avoid this?

This is called predicativity, and Prop is an impredicative universe. This is a very strong axiomatic assumption (it pumps the consistency strength from primitive recursive arithmetic all the way up to ZFC + some inaccessible cardinals), but conversely it is necessary for doing "real math" in lean. It is not inconsistent, at least as long as Prop is also proof irrelevant and understood to have no internal structure like you say, just "true" and "false"