Difference between P -> Q and P /\ Q

Using Rocq
4

P → Q and P /\ Q in general make very different statements. P → Q means “if P, then Q” while P /\ Q means “P and Q”. It just happens that (P /\ Q) → R and P → (Q → R) are equivalent.

You usually use “forall” with → and “exists” with /\. If you think about what those statements would actually mean, it might make it clearer:

  • forall x:T, P x -> Q x reads as “For all x, if P x is true, then so is Q x.”
  • exists x:T, P x /\ Q x reads as “There is some x for which P x is true, and Q x is also true.”