I need to understand how is this the definition of exists

```
Inductive ex {A : Type} (P : A -> Prop) : Prop :=
| ex_intro : forall x : A, P x -> ex P.
Notation "'exists' x , p" :=
(ex (fun x => p))
(at level 200, right associativity) : type_scope.
```

The way I understand it is that this definition of exists is almost identical to the definition of forall, because forall implies exists directly.

That code means that to prove `ex P`

, you must provide an arbitrary witness `x`

and a proof `P x`

.

The way I understand it is that this definition of exists is almost identical to the definition of forall, because forall implies exists directly.

Intuitively, "forall implies exists" is not true, because `forall x : A, P x`

holds even if `A`

is empty.

I'm not sure why you think it is, but it might be a matter of parentheses. Formally, "forall implies exists" would usually mean `(forall x : A, P x) -> (exists x : A, P x)`

or `(forall x : A, P x) -> ex P`

, but the type of `ex_intro`

above is instead `forall x : A, (P x -> ex P)`

which is very different.

I see, now It kinda makes sense, thanks a lot!

(deleted)

Last updated: Oct 05 2023 at 02:01 UTC