Jan Brosius writes:
> > Why do some computer scientists have such problems with the good logical
> > forall
> > and exist. Remember that good old logic came first.
> > On it was build SET theory.
> > On it was built topological space
> >
> > To prove some theorem in lambda calculus one used a topological model.
> >
> > You see : good old logic came FIRST afterwards came theorems of typed
> > lambda calculus .
> > This is not the sophistic question : what came first : the egg or the
> > chicken.
> >
> > NO good old logic came first .
Your argument is absurd and irrelevant.
> SORRY, this is quite TRUE , in fact [forall x. alpha(x)] <=> alpha(x)
>
> the above true equivalence seems to be easily considered as wrong . Why?
> Because alpha(x) is TRUE can be read as alpha(x) is TRUE for ANY x.
I think this is one of the roots of your misconceptions. These two
propositions are certainly not equivalent. Maybe it is because you have been
told that, in Haskell, syntax we typically elide the "forall" quantifier.
The sentence "alpha(x)" asserts that there is a _distinguished_ element named
"x" in the domain of your model, and that that element, at least, satisfies
"alpha". The sentence "forall x. alpha(x)", OTOH, asserts that _any_ element
in your domain satisifies "alpha". So if your domain is a set D, then a model
of "alpha(x)" needs a subset C of D to interpret "alpha", along with a member
X of C to interpret "x", and the sentence is true iff X is in C. OTOH, a model
of "forall x. alpha(x)" needs only the subset C, and is true iff C=D, since it
asserts that for any element Y of D, Y is in C.
In Haskell the situation is complicated by the fact that there are no
"set-theoretic" models (are you even aware that Haskell's type system is
unsound?), and the fact that the domain is multi-sorted. But those facts do
not bear on the distinction between the two terms on either side of the
equivalence above.
--
Frank Atanassow, Dept. of Computer Science, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
