----- Original Message -----
From: Jan Brosius <[EMAIL PROTECTED]>
To: Richard Uhtenwoldt <[EMAIL PROTECTED]>
Sent: Wednesday, May 17, 2000 1:23 AM
Subject: Re: more detailed explanation about forall in Haskell
>
> ----- Original Message -----
> From: Richard Uhtenwoldt <[EMAIL PROTECTED]>
> To: Jan Brosius <[EMAIL PROTECTED]>
> Cc: <[EMAIL PROTECTED]>
> Sent: Tuesday, May 16, 2000 11:06 PM
> Subject: Re: more detailed explanation about forall in Haskell
>
>
> > although this argument originated from a discussion of rank-2
> > polymorphism in Haskell's type system, the part I am replying to
> > addresses only first-order predicate logic (also called "predicate
> > calculus").
> >
> > Jan Brosius asserts
> >
> > > Now forall s1. ( ST s1 T(s)) IMPLIES forall s . ( ST s T(s) )
> >
> > Marcin replies
> >
> > > It does not. And I have already told why, a few e-mails ago.
> > > I can explain it again.
> > >
> > > For the first term to have any meaning, "s" must have a meaning,
> > > because it is a free variable. So for a counter-example assume that
> > > we sit in real numbers and
> > > ST a b means a^2 > b
> > > T(a) means a+1
> > > s means -2
> > >
> > > The first term means forall s1. s1^2 > -1, which is true.
> > > The second term means forall s. s^2 > s+1, which is false.
> > > So the first does not imply the second.
>
> Now I understand what Marcin meant with this "counterexample".
> I admit I was very puzzled to find out where these formulas came from.
> It's a pity that I didn't saw it in a previous email.
>
> I guess Marcin meant with first term:
>
> forall s1. ST s1 T(s) == forall s1. s1^2 > T(s) == forall s1. s1^2 > s +
1
>
> As everybody can notice the first term is FALSE . Indeed let s1 = 1 and s
=1
> and we get a false assertion.
> (the assertion 1^2 > 20
> However
>
> [forall s1. ST s1 T(s) ] => [ forall s. ST s T(s)] is always TRUE.
>
> Since EX FALSO QUODLIBET ( a false assertion implies everything) if we
> would say
>
> [ forall s1. ST s1 T(s) ] => [ forall s . ST s T(s)] ( remember always )
> TRUE
>
> forall s1. ST s1 T(s) (FALSE)
>
****************************************************************************
> ***********
> forall s . ST s T(s) == forall s . s^2 > s + 1 (TRUE or FALSE) ( here
> FALSE)
>
> The above rule is called a syllogism
>
> Marcin departed in his reasoning allready with a false assertion. The
error
> he committed was to say
> that the first term was true for the case s = -2 . Here it is clear what
> confusion computer scientists
> might experience if they lose the real meaning of a variable. Indeed if I
> would put s =3 then everybody sees
> that one gets a FALSE assertion forall s1. s1^2 > 4 (false for s1 = 1)
>
> So Marcin's statement that he gave a counterexample was FALSE.
>
> (Sometimes one needs to reread something several days later in order to
see
> what was meant
> by somebodyelse)
>
> >
> > Jan's assertion and Marcin's counter-assertion are later repeated two
> > more times in different words. I think Marcin's counterexample
> > completely disproves Jan's assertion.
>
> Well Marcin's counterexample is FALSE ( see above)
>
>
> > I am adding my thoughts to the
> > discussion simply to argue for Marcin's conclusion using different (and
> > more numerous) words and concepts.
>
> too numerous and thus too dangerous.
>
> >
> > it might prove illustrative to quantify every variable in Jan's
> > assertion. this means quantifying the single free occurence of s.
> > there are two ways to do that, and I am tempted to say that this next
> > way is the right way.
> >
> > forall s.((forall s1. ( ST s1 T(s))) implies forall s . ( ST s
T(s) ))
>
>
> WARNING : The notation forall s1 , s . alpha(s1, s) is since unbounded
> forall's commute simply an abbreviation
> for either forall s1. forall s . alpha(s1,s) or forall s. forall s1 .
> alpha(s1,s)
>
>
> >
> > (redundant parentheses added for emphasis.) but to be perfectly
> > intellectually honest, Jan wrote the formula, so Jan has a right to
> > decide what it means. Jan could have meant this next. the only
> > syntactic difference between that last formula and this next one is that
> > the scope of the "forall s" that I added to Jan's assertion is limited
> > to the left of the "implies".
> >
> > (forall s,s1.( ST s1 T(s))) implies forall s . ( ST s T(s) )
>
> yes using braces is better if there is risk of confusion
>
> >
> > the latter has the considerable advantage of being true whereas the
> > former is false.
>
> If you mean by the former : [forall s1. ST s1 T(s) ] => [forall s. ST s
> T(s)] then I must say
> that on the contrary this is TRUE
>
> REMEMBER : [ forall s1. ST s1 T(s)] is EQUIVALENT to [forall s1, s . ST s1
> T(s)]
>
> These are the formall rules of forall (even not using Bourbaki's logic)
>
> >however, the true one is less useful in establishing
> > conclusions than the false one. if we have already proved (forall s1. (
> > ST s1 T(foo))) for some concrete thing "foo", then the false formula
> > allows us immediately to conclude forall s.(ST s T(s)).
> >
> >
> > moreover, Jan wrote that "(forall y) ( forall x ) alpha(x,y) is
> > equivalent with alpha(x,y)".
> > I am tempted to say that that is just
> > wrong,
>
> 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?)
>
> > but rather I ask Jan: do you think that the two formulae, which I
> > call the false one and the true one, are equivalent?
>
> Your false one (?)===[forall s1 . ST s1 T(s) ] => [forall s. ST s T(s)]
>
> Your true one (?) ===[forall s. (forall s1. ST s1 T(s) ] => [forall s . ST
s
> T(s)]
>
> Then these 2 implications are EQUIVALENT.
> >
> >
> > btw, the natural-deduction style of proof is a lot more useful
> > than that Bourbaki stuff for understanding this dispute.
>
> I am more and more thinking that the natural-deduction style of proff is
> either wrong or bad interpreted.
> AS for Bourbaki : use Bourbaki from now on.
>
>
> > eg,
> > here is a proof in the natural-deduction style of the "true formula".
> >
> > step 1. suppose (forall s,s1.( ST s1 T(s))).
> >
> > step 2. consider an arbitrary thing, foo.
> >
> > step 3. by instatiation of the s in step 1, (forall s1.(ST s1 T(foo))).
>
> for ANY foo.
> >
> > step 4. by instatiation of the s1 in step 3, (ST foo T(foo)).
>
> for ANY foo.
> >
> > step 5. summarizing steps 2-4, (forall s.(ST s T(s)))).
>
> Correct
>
> >
> > step 6. summarizing steps 1-5, (forall s,s1.( ST s1 T(s))) implies
> > forall s . ( ST s T(s) )
>
> Correct
> >
> > here is an invalid proof of the false formula. step 3 is invalid
>
> No you have just replaced a variable's name s by another variable's name
> foo
>
> > because to replace an old quantified variable with a new one is only
> > valid if the new variable does not occur free in the old variable's
> > scope. this error is called "variable capture".
>
> NO error, sorry.
> >
> > step 1. consider an arbitrary thing. call it s this time instead of
foo.
> >
> > step 2. suppose (forall s1.(ST s1 T(s)))
> >
> > step 3. change the quantified variable from s1 to s, yielding (forall
s.
> > (ST s T(s))).
> >
> > step 4. summarizing steps 2-3, (forall s1.(ST s1 T(s))) implies forall
> > s . ( ST s T(s) )
> >
> > step 5. summarizing steps 1-4, forall s.((forall s1. ( ST s1 T(s)))
> > implies forall s . ( ST s T(s) ))
>
> Correct
> (you see no need to use foo)
> >
> > this has been a very tedious post. if you've read this far I would love
> > to know which if any of the "proof assistants"
>
> I you mean a Haskell program. I don't know
>
> > you reccommend that can be
> > used to let the machine perform the checking of "trivial but tedious"
> > proofs like those last 2.
> >
> >
>
>
> 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 .
>
> Very Friendly
> Jan Brosius
>
