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