Inductive Predicate for Exists looks confusing

Stream: general

[Bernardo Borges]

On learning about inductive predicates I stopped at the Exists definition:

inductive Exists (α : Type u) (p : α → Prop) : Prop
| intro : ∀ x : α, p x → Exists α p

It might be a "loaded" notation, but I found it most unusual that the forall is used to define the exists. Is this sound or is there another piece missing? Forgive the cluelessness...

[David Renshaw]

If you find the forall quantifier distracting, you can also write it like this:

inductive Exists (α : Type u) (p : α → Prop) : Prop
| intro : (x : α) → p x → Exists α p

[David Renshaw]

It says that Exists.intro takes two arguments: an α -- call it x -- and a proof of p x.

[David Renshaw]

I am reminded of existential types in Haskell, which use the forall keyword: https://wiki.haskell.org/Existential_type

[Edward van de Meent]

personally, it reminds me of the paradox given by the close-to converse ∃ (x :α), (p x → ∀ (y:α), p y), which can be described as saying "there exists a person in the bar who drinks only when everyone in the bar is does", aka the drinker paradox

[Mario Carneiro]

Bernardo Borges said:

On learning about inductive predicates I stopped at the Exists definition:

inductive Exists (α : Type u) (p : α → Prop) : Prop
| intro : ∀ x : α, p x → Exists α p

It might be a "loaded" notation, but I found it most unusual that the forall is used to define the exists. Is this sound or is there another piece missing? Forgive the cluelessness...

This is not a mistake. In dependent type theory there is an asymmetry in the logical connectives: forall is the dependent Pi type and this is primitive, while exists is an inductive type which is defined using forall. This also relates to the fact that docs#not_exists is provable with no axioms while docs#Classical.not_forall requires classical logic

[Kevin Buzzard]

"for every y such that p(y), you can give a proof that there exists an x such that p(x)".

[Kevin Buzzard]

I remember sitting in a rented apartment in Berkeley in 2017 also being super-confused about this (reading #tpil). The above is my explanation of what's going on

[Max Nowak 🐉]

I think if you understand it from a programming perspective it makes a lot more sense: try writing Exists using “structure” instead. You’ll find that it’s just a tuple of a witness x, such that a certain predicate holds. Nothing else really.

[Max Nowak 🐉]

Similar constructs are also Sigma, Subtype, Prod, etc

[Max Nowak 🐉]

Just with different combinations of which of the two parts are in Prop vs in Type, and whether it’s a non-dependent or dependent pair.

[Kevin Buzzard]

Sure it makes sense from a CS point of view. But if you're a mathematician who doesn't know the first thing about type theory (eg me in 2017) then it's really disconcerting that the definition of "exists x, p x" seems to be "forall x, p x".

[Mario Carneiro]

Oh, but also the parentheses are really important here!

| intro : (∀ x : α, p x) → Exists α p -- wrong

| intro : ∀ x : α, (p x → Exists α p) -- right

[Mario Carneiro]

Using the former in the definition of exists would indeed make it equivalent to forall

[Patrick Massot]

Kevin is well aware of this, that’s why he wrote “seems to be”.