> Please could somebody post a short, plain text summary of the discussion
> in this thread? The recent exchanges have been long and involved, which
> has made it impossible for me (and other busy onlookers too, I suspect)
> to keep up. Without such a summary, I think that this thread may be
> reaching the end of it's useful life, at least for the main Haskell list.
I won't attempt a full summary, but in spite of some unfortunate personal
excesses (recent messages let me hope that they won't be repeated..) and
some unnecessary copying and repeating of messages, the basic issues
seem to have become a bit clearer now. So I'll try to summarize those.
The thread started in connection with the typing of state transformers
(especially runST and friends) but by now, I assume that the difficulties
are solely down to (different schools of) logic.
The baseline is that there are several interpretations of common syntax
in use which, in isolation, may or may not be consistent, but certainly lead
to confusion and inconsistencies if mixed. Our main problem is that we
are not always aware that each poster might associate different assumptions
when using the same syntax.
Jan Brosius seemed to claim that, for a formula context alpha
(1) forall x. alpha(x) <=> alpha(x)
which seemed wrong to others, who suspected that misunderstandings in
scoping were the issue. Some progress was made when it was suggested
that different interpretations of open formulae (formulae with free
variables)
and equivalence might be involved. The claim was then modified to:
(2) "forall x. alpha(x)" is a TRUE formula
iff
"alpha(x)" is a TRUE formula
>From the context in which the concept of a "TRUE formula" was used, I
assume the definition:
(3) "a" is a TRUE formula
iff [definition]
"a" is true in all interpretations (substitutions for free
variables).
Note that definition (3) validates (2), but doesn't require a contextual
equivalence of the quoted formulae, so it does not follow that
(4) forall contexts C and alpha.
( "C[forall x. alpha(x)]" is a TRUE formula
iff
"C[alpha(x)]" is a TRUE formula)
Most of the disputed examples were stated in such a form that Jan could
assume an empty context whereas others assumed an implied quantification
over all contexts. Many misunderstandings should disappear if contexts
are made explicit. E.g., for Jan, (1) was just a bad way to write down (2),
whereas others interpreted (1) as
(5) forall contexts C and alpha.
(C[forall x. alpha(x)] <=> C[alpha(x)])
Naturally, Jan concluded that (1) is valid, if badly written, whereas others
concluded that (1) is invalid. Similarly for the more complex examples.
A second source of confusion was whether free variables should be
interpreted or not. One school of reasoning assumes that variables are
placeholders for elements of a certain domain, another (apparently
favoured by Jan) assumes that variables are placeholders, period.
With uninterpreted free variables, "alpha(x)" can only be true if "alpha"
is completely independent of its parameter (we can execute the
rules of the logic purely syntactically and never need to make any
assumption about the variable "x" when evaluating "alpha(x)").
For the "uninterpreted" school, (1) is valid, because we can derive
additional information about "alpha(x)", namely that it has to be
completely parametric in "x". This additional information is not
available in the "interpreted" school: if we assume that variables
and formulae have to be interpreted in some domain, we either
have to reject open formulae alltogether or assume an implicit
quantification over free variables, as in (3). But then, the question
becomes where to put the implicit quantifiers in (1):
(6a) "forall x. alpha(x) <=> FORALL x. alpha(x)"
(6b) "FORALL x. (forall x. alpha(x)) <=> alpha(x)"
(6a) interprets "<=>" as part of the meta-logic [so there are two
formulae in (1), to be quantified individually], whereas (6b)
interprets "<=>" as part of the object-logic [so there is only a
single formula in (1)].
(6a) is valid, (6b) is not..
Again, this leads to ambiguities and to completely different
conclusions about the more complex examples and counterexamples.
The nasty part of this was that the opponents used seemingly familiar
notation (and so assumed that no definition was required), yet associated
completely different interpretations with a common notation. In fact, while
I am reasonably confident that the above identifies some of the relevant
issues, I am not at all sure whether this solves all misunderstandings, or
whether I have expressed myself in such a way that all parties involved
come to the same interpretation of this message.
Claus
PS. These issues must come up again and again when teaching or
learning logic. If anyone knows a good study/survey of
"common misunderstandings in introductory logic courses",
I would be grateful for a reference.
