You might determine whether it should be "all" or "exist" by means of a formal analysis: In metamathematics exist x: A is a rewriting of not(all x: not A) Then an example of a set of metamathematical axioms for the "all" quantifier is as follows (written as code in my program): theory Q. -- Quantification axioms, Mendelson, p.57 (called `K' there). { formula A, B, C term t free x. axiom Q1. A => (B => A). axiom Q2. (A => (B => C)) => ((A => B) => (A => C)). axiom Q3. (not B => not A) => ((not B => A) => B). axiom Q4. t free for x in A |- (all x: A) => [x\t]A. axiom Q5. x not free in A |- (all x: A => B) => (A => all x: B). axiom MP `modus ponens'. A, A => B |- B. axiom Gen `generalization'. A |- all x: A. } -- theory Q. Here, the symbol "|-" is the metamathematical implication, i.e., provability. Here, A |- B corresponds to Prolog B :- A. In Haskell, what is the analogue of the generalization axiom Gen? -- If you know that, then you know what should be "all" and "exist" in Haskell. Hans Aberg