>>>From: Frank Atanassow <[EMAIL PROTECTED]>
>To: Jan Brosius <[EMAIL PROTECTED]>
>Cc: <[EMAIL PROTECTED]>>
>Sent: Wednesday, May 17, 2000 1:35 PM
>Subject: Fw: more detailed explanation about forall in Haskell
> 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)
Here, I have to say that the above equivalence is false . SHAME on me.
I must put this in the good way;
[forall x . alpha(x)] => alpha(x) is True
If alpha(x) is TRUE then the following is true : alpha(x) => [forall x.
alpha(x)]
So if alpha(x) is TRUE then [forall x. alpha(x) ]<=> alpha(x)
Sorry for the error
> >
> > 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
NO , saying that there is a distinguished element T that satisfies alpha
implies
that exists x. alpha(x) is true
So the following implication is true
(T | x) alpha(x) => exists x. alpha(x)
that is , if alpha(T) is true then [exists x. alpha(x)] is true
more precisely , let c be a constant , and if alpha(c) is true then
you can say that exists x. alpha(x) is true.
> "x" in the domain of your model, and that that element, at least,
satisfies
x is a variable ; no domain ; no model
> "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.
Very friendly
Jan Brosius
>
> --
> 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
>
>
>
