Existentials

[Albert Lai]

Reminds me of the very intimate relationship between forall and exist
in predicate logic.  For example,

  (forall x. P=>Q) = (exist x.  P)=>Q
  (exist  x. P=>Q) = (forall x. P)=>Q

provided Q mentions no x and the logic is classical enough.  But the
two quantifiers are closer than being duals to each other as in the
above.  I think they are re-incarnations of each other at times.  How
do you formalize "if an even prime number exists, it has to be 2"?
You don't normally use the existential quantifier, no no.  You write:

  forall x. even x /\ prime x ==> x=2