>From: Frank Atanassow <[EMAIL PROTECTED]>
>To: Jan Brosius <[EMAIL PROTECTED]>
>Cc: <[EMAIL PROTECTED]>
>Sent: Thursday, May 18, 2000 2:53 PM
>Subject: Re: more detailed explanation about forall in Haskell
> Jan Brosius writes:
> > I must put this in the good way;
> >
> > [forall x . alpha(x)] => alpha(x) is True
>
> Yes, by instantiation.
I disagree.
>
> > If alpha(x) is TRUE then the following is true : alpha(x) => [forall x.
> > alpha(x)]
>
> No, alpha(x) only asserts that some element named x satisfies alpha. It
does
> not follow that therefore every other element also satisfies alpha.
No the variable x means that it can be substituted by any term. That is the
real meaning of a variable
(at least in classical logic).
Consider e.g. Carl Witty's formula : prime(x) == x is a prime number.
Then prime(2) == (2|x) prime(x) is true , and prime (4) is false
Take something else alpha(x) == prime(x) AND ¬ prime(x) ( ¬ signifies
not)
then alpha(x) is a false formula and you have ¬ [exists x. alpha(x)]
On the contrary beta(x) == ¬ alpha(x) is true for any x
>
> > So if alpha(x) is TRUE then [forall x. alpha(x) ]<=> alpha(x)
>
> This does not follow. It is truth-equivalent to:
Sorry, I disagree
>
> [forall x. alpha(x)] <=> True
( In the above you should at the very least not forget to mention that
[forall x. alpha(x)] must be true )
In principle True is a sloppy expression for saying that [forall x .
alpha(x)] is a theorem of some mathematical theory. I have used True because
discussing mathematical theories would have lead the discussion
out of the scope of the discussion.
For instance let "T=" denote a mathematical theory with equality
then one has "T=" -| x = x
that is the formula x = x is a theorem in "T=" . More sloppy the formula
x=x is TRUE in "T="
>
> which is equivalent to:
>
> forall x. alpha(x)
>
> which is only true when every element satisifies alpha; so it is not a
> tautology.
>
> I repeat: you do not understand the difference between bound and free
variables.
I disagree a free variable is not a constant.
A bound variable is a variable tied to a quantifier. In principle a bound
variable is not visibly.
This is best illustrated by Bourbaki's approach where they first define :
exists x . alpha(x) == (`t x (alpha)| x) alpha
where if e.g. alpha(x) == x = x then
`t x (alpha) == `t ( `sq = `sq ) where `sq denotes a small square and
where here both `sq are tied to `t by a line
In this way I can really say that in [existx x. x = x] the variable x has
disappeared.
Finally Bourbaki defines forall x . alpha(x) == ¬ [exists x . ¬ alpha(x)]
I repeat : there are no domains in propositional calculus , but I am aware
that in some text books about
propositional calculus one speaks about it , I regard this as cheating :
introducing a concept that one is going to define later. I remember my
prof, in logic in 1 cand. math - physics where his first lesson began by
writing
on the blackboard : p V ¬ p and he only said " p or not p " " tertium
non datur" " a third possibility is not given "
His whole course was as formally as possible, and variables were not
supposed to range about a domain.
> A free variable behaves like a constant.
No a constant is always the same constant, it is never substituted by
something else, it is "immutable".
A variable is a placeholder for a Term ( a constant is a special term)
>It is not "implicitly"
> quantified in any way, because it denotes a specific element. The only
> difference between a constant and a free variable is syntactic: a free
> variable can be bound in an outer scope,
No the real role of a variable say x in a formula alpha(x) or a term T(x)
is a PLACEHOLDER ready to be substituted by a Term (e.g. constant or a
parameterized term)
And that's the reason why I should find it weird if In Haskell 98+ one
would distinguish between
a -> a and [forall a. a -> a]
>while a constant cannot.
>
> > > 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
>
> Yes, it also implies this fact, because it can be derived by
extensionality:
>
> alpha(x) => exists y. alpha(y)
>
> However, existential quantification hides the identity of the element in
> question. The fact that we know _which_ element it is that satisifies
alpha
> permits us to say more. This is why:
>
> exists x. alpha(x),
> alpha(x),
>
> and
>
> forall x. alpha(x)
>
> are not truth-equivalent. Rather we have:
>
> forall y. alpha(y) => alpha(x) and alpha (x) => exists z. alpha(z)
AND if alpha(x) is a TRUE formula then alpha(x) => forall x. alpha(x)
A better way to express this is
Rule of genaralization:
alpha(x ) is True (and x is a variable)
********************
forall x . alpha(x ) is true
I repeat that my use of true or false is not really the way it is expressed
in Bourbaki , I used it
in order to be understood by everybody (and in this discussion it doesn'
hurt).
>
> > > "x" in the domain of your model, and that that element, at least,
> > satisfies
> >
> > x is a variable ; no domain ; no model
>
> A model must assign an element in the domain to each free variable. You
need a
> model to determine the truth-value of a first-order proposition which is
not
> tautological. We are trying to establish the truth-value of a proposition
with
> a free variable; therefore we need a model. A model needs a domain of
elements
> to draw from. Therefore we need a domain. OK?
No, you don't need a model for (formal ) logic . If at this stage
(propositional calculus) you would
talk about a domain or set then you are introducing "domain" before you
have discussed what
a domain is. If you are using a model than you are implicitly accepting the
fact that the whole
of mathematical set theory is at your disposition. Since mathematical set
theory is based on propositional calculus a variable x in propositional
calculus is really a variable which is equivalent to saying that it
can be used for substitution no more,no less.
The forall's used with domains, say e.g. N is the set of integers are in
fact bounded forall's and
one has e.g.
forall x in N . prime(x) == forall x. x in N => prime(x)
the left forall above is an example of a bounded forall where x must range
over a constant set , here N.
However more complicated bounded forall's can be considered.
In general let alpha(x) be a formula about a variable x then
[forall alpha(x) . prime(x)] == [forall x. alpha(x) => prime(x)]
>
> --
> 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
>
>
Friendly
Jan Brosius
