Thu, 17 Apr 2003 19:24:28 +0200
You might determine whether it should be "all" or "exist" by means of a
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.