----- Original Message -----
From: Jan Brosius <[EMAIL PROTECTED]>
To: Carl R. Witty <[EMAIL PROTECTED]>
Sent: Thursday, May 18, 2000 12:06 PM
Subject: Re: Fw: more detailed explanation about forall in Haskell
> Thanks Carl for letting me see an ugly error that I made . SHAME on me.
>
> the equivalence [forall x. alpha(x)] <=> alpha(x) is ONLY TRUE if
> alpha(x) is a TRUE formula.
>
> [forall x. alpha(x)] => alpha(x) is TRUE
>
>
>
> Let's see what happens when alpha(x) is FALSE for not all x and if one
would
> accept that:alpha(x) => [forall x. alpha(x)] is TRUE.
>
> Since alpha(x) is FALSE there might still be a constant c such that
alpha(c)
> is TRUE
>
> Then (Modus Ponens)
>
> alpha(c) => [forall x. alpha(x)]
>
> alpha(c)
>
> *************************************
>
> forall x . alpha(x) is TRUE
>
> which is of course false
>
> this shows that the implication alpha(x) => [forall x. alpha(x)] is in
> general false (it is only true if alpha(x) is a true formula.
>
> Very friendly
> Jan Brosius
>
>
> >.From: Carl R. Witty <[EMAIL PROTECTED]>
> >To: Jan Brosius <[EMAIL PROTECTED]>
> >Cc: <[EMAIL PROTECTED]>
> >Sent: Wednesday, May 17, 2000 4:24 AM
> >Subject: Re: Fw: more detailed explanation about forall in Haskell
>
>
> > "Jan Brosius" <[EMAIL PROTECTED]> writes:
> >
> > > > 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.
> > > >
> > > > (Is there something wrong with the education of a computer
scientist?)
> >
> > Jan, could you tell us whether you think the following statements are
> > true or false?
> >
> > Let prime(x) mean "x is a prime number".
> >
> > 1. [forall x. prime(x)] <=> prime(x)
> > 2. forall x.([forall x. prime(x)] <=> prime(x))
> > 3. forall y.([forall x. prime(x)] <=> prime(y))
> > 4. [forall x. prime(x)] <=> prime(y)
> > 5. [forall x. prime(x)] <=> prime(2)
> > 6. [forall x. prime(x)] => prime(2)
> > 7. prime(2) => [forall x. prime(x)]
> > 8. prime(2)
> > 9. [forall x. prime(x)] <=> prime(4)
> > 10. [forall x. prime(x)] => prime(4)
> > 11. prime(4) => [forall x. prime(x)]
> > 12. prime(4)
> > 13. forall x. prime(x)
> > 14. prime(x)
> > 15. Statement 1 above means the same thing as statement 2 above.
> > 16. Statement 2 above means the same thing as statement 3 above.
> > 17. Statement 3 above means the same thing as statement 4 above.
> > 18. Statement 5 above is a substitution instance of statement 3;
> > thus, if statement 3 were true, statement 5 would be true.
> > 19. Statement 13 above means the same thing as statement 14 above.
> >
> > If we follow the convention that free variables are to be considered
> > implicitly universally quantified, my vote is that statements 6, 8, 9,
> > 10, 11, 15, 16, 17, 18, and 19 are true; the rest are false.
> >
> > Carl Witty
> >
>
