Existentials

[Hans Aberg]

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