## Stream: Coq users

### Topic: The logic behind existential quantification

#### walker (Feb 18 2022 at 08:22):

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.

#### Paolo Giarrusso (Feb 18 2022 at 09:15):

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.

#### walker (Feb 18 2022 at 09:24):

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

#### walker (Feb 18 2022 at 09:25):

(deleted)

Last updated: Jun 16 2024 at 01:42 UTC