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.
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. I am adding my thoughts to the
discussion simply to argue for Marcin's conclusion using different (and
more numerous) words and concepts.
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) ))
(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) )
the latter has the considerable advantage of being true whereas the
former is false. 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, but rather I ask Jan: do you think that the two formulae, which I
call the false one and the true one, are equivalent?
btw, the natural-deduction style of proof is a lot more useful
than that Bourbaki stuff for understanding this dispute. 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))).
step 4. by instatiation of the s1 in step 3, (ST foo T(foo)).
step 5. summarizing steps 2-4, (forall s.(ST s T(s)))).
step 6. summarizing steps 1-5, (forall s,s1.( ST s1 T(s))) implies
forall s . ( ST s T(s) )
here is an invalid proof of the false formula. step 3 is invalid
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".
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) ))
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" you reccommend that can be
used to let the machine perform the checking of "trivial but tedious"
proofs like those last 2.
