- Original Message -
From: Jan Brosius [EMAIL PROTECTED]
To: Carl R. Witty [EMAIL PROTECTED]
Sent: Thursday, May 18, 2000 12:06 PM
Subject: Re: Fw: more detailed explanation about forall in Haskell
Thanks Carl for letting me see an ugly error that I made . SHAME on me
On 16 May 2000, Carl R. Witty wrote:
"Jan Brosius" [EMAIL PROTECTED] writes:
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
Jan Brosius writes:
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
Frank Atanassow writes:
Jan Brosius writes:
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
- 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
"Jan Brosius" [EMAIL PROTECTED] writes:
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
Jan Brosius writes:
Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM :
2. Next let me point out once and for all that
logical quantifiers are used only in logical formula's .
Types can be treated as logical formulas, according to the
Curry-Howard
