Stream: Coq users

Topic: The logic behind existential quantification


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip walker (Feb 18 2022 at 09:24):

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

view this post on Zulip walker (Feb 18 2022 at 09:25):

(deleted)


Last updated: Feb 04 2023 at 21:02 UTC