>From: Peter Douglass <[EMAIL PROTECTED]>
>To: 'Jan Brosius' <[EMAIL PROTECTED]>; Frank Atanassow <[EMAIL PROTECTED]>
>Cc: <[EMAIL PROTECTED]>
>Sent: Friday, May 19, 2000 6:03 PM
>Subject: RE: more detailed explanation about forall in Haskell
| Jan Brosius wrote:
|
| > look at this example:
| >
| > alpha(x) == x is_an Integer => x^2 > -1
| >
| > this is an example of a formula that is true
| >
Sorry, this is not my logic. Since this formula is "true" it is allowed to be
generalized
forall x . alpha(x) == forall x. (x is_an Integer => x^2 > -1)
and this may be rewritten in a more known form
forall x. alpha(x) == [forall x is_an Integer. (x^2 > -1)]
or still another way
forall x. alpha(x) == [forall x `element_of` N) .( x^2 > -1)] (where N denotes the
set of integers)
which can be read as " forall x element of the set of integers N , x^2 > -1 "
The forall in the above expression is an example of a bounded forall. It is also an
example of a so called
closed formula (because having no free variables anymore ) or also called a sentence.
An other example , let R be the set of real numbers and we want to express that the
square of a real number is
always >= 0 then on can write
beta == [forall x `element_of R . ( x^2 >= 0)]
then by definition of a bounded forall :
beta == [forall x . (x `element_of R => x^2 >= 0 )]
and define next : alpha (x) ==( x `element_of R => X^2 >=0 )
Next remember that everybody agreed that the following is a TRUE implication:
(*) forall x . alpha(x) => alpha(x)
Finally remember that the Modus Ponens rule gives us a way to derive new theorems from
implications :
P => Q true
P true
*******************
Q true
Then I get
[forall x . alpha(x)] => alpha(x) (true)
forall x . alpha(x) (true)
*******************************************
alpha(x) (true)
So we get the true formula
alpha(x)
where x is free.
I only wanted to state that this is not my logic and that IF one accepts the validity
of the Modus Ponens rule and the fact agreed by everybody that the implication
[forall x . alpha(x)] => alpha(x) is true,
then one HAS to accept that the following formula
alpha(x)
is true.
Finally, since I have been attacked by someone to have misread Bourbaki's book , well
here
you have something:
Book entitled : " N. Bourbaki
Elements de Mathematique
editor : Hermann, Paris 1970
page: E I.39
Theoreme 1. - x = x
" Designons par S la relation x = x de T0. ......
For those who don't know French : In Bourbaki one proves theorem 1 : x = x
this shows that alpha(x) == x = x is a true formula in a quantified theory with an
equal sign
A message to the one who liked to ridiculize me so much : If you don't agree with all
this , please send your
comments directly to Bourbaki (a famous french society of mathematicians ) , say to
these mathematicians
they are a laughing stock for all logicians from the time of Tarski , Gentzen and ...
your name . Please
don't forget to put a stamp on the envelope ( joke about Dutch).
I hope that this will settle once and for all that this is not my logic , but I
appreciate it much that you (the person in Dutch - land) want to give me full credit
of their work.
| > *If you want to come up with your own logic, where alpha(x)
| > is equivalent to
| > *forall x. alpha(x), then that's fine.
| >
| > No, if alpha(x) is a true formula then forall x. alpha(x) is
| > again a true assertion
|
| I think part of the confusion here has to do with the notation alpha(x).
| The traditional mathematical notation f(x) is ambiguous. It may either
| refer to an abstraction or an application. In this regard, lambda notation
| is much superior. What does the alpha(x) here mean?
| If we assume it is a function like:
| alpha = \ x . (x is_an Integer => x^2 > -1 )
| then it is meaningful to debate whether or not the inner 'x's refer to the
| same x as the lambda bound x or whether "x is_an integer" creates a new
| binding.
| On the other hand, if we assume that alpha(x) is an application of alpha
| to x then the debate seems to be whether x refers to some value, or whether
| it is simply a place-holder.
| Perhaps Jan can clarify what is meant here.
| --Peter Douglass
|
|
|
|
Still friendly greetings
Jan Brosius
