>
>
>
> > 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
> > > > isomorphism.
> > >
> > > Sorry, never heard of in logic. But perhaps you can explain.
> >
> > [I hope it is ok if I reply, although I am sure Marcin can defend
> > himself just as well]
> >
> > Maybe because you have only learnt about classical logic, which is a
> > shame especially for a computer scientist. Have a look at a standard
> > text book, like Troestra & van Dalen's "Intuitionism I,II".
>
> Sorry, but I cannot study all sorts of logic that circulate around. I
don't
> know what a computer scientist is supposed to know. I follow Bourbaki's
> logic where there is no need for an axiom of choice . However the so
called
> axiom of choice is there a theorem that is one proves that the Cartesian
> product of a non empty family of non empty sets is in fact non empty.
>
> What about me : I have done theoretical physics and mathematics.
> >
> I have embraced formal logic ,and the whole of math can be build on it.
> Formal logic is not sentimental.
> >
> > Anyway, in intuitionistic logic it is natural indentify proofs and
> > programs and proposition and types. Maybe best illustrated by the BHK
> > (Brouwer-Heyting-Kolmogoroff) semantics:
> >
> > A proof of a /\ b is a proof of a and a proof of b, hence a /\ b = (a,b)
>
> Sorry, are you going to say that a tuple (a,b) is the same as " a AND b "
> Then the Haskell language didn't state it. Sorry, a tuple is a tuple and
> nothing else,
> what you tell me is that the notation of tuple can be used as logical AND
> for propositions.
>
> > A proof of a \/ b is a proof of a or a proof of b, hence a /\ b = Either
a
> b
>
> You mean a V b = Either a b ?
> I guess you mean with a V b the logical or?
>
> > A proof of a -> b is a method to calculate a proof of b from a proof
>
> Here you use the sign -> (function ) for the sign => (implies)
>
> > of a hence a -> b = a -> b
>
> In formal logic we say just this
>
> a (true)
>
> a => b (true )
> *********************
> b (true)
>
>
> > There is no proof of False, hence one would identify False with the
> > empty type, but as far as I know there is no empty type in Haskell?
> >
> > As an example how do we prove (a \/ b) /\ c -> (a /\ c) \/ (a /\ b)
> > in Haskell ?
> >
> > lem :: (Either a b,c) -> Either (a,c) (b,c)
> > lem (Left a,c) = Left (a,c)
> > lem (Right b,c) = Right (b,c)
>
> Sorry I don't have to know all this , do you really think I am illiterate
in
> propositional logic or boolean algebra
>
> (a + b) . c = a . c + b . c (distributivity) AND (a.b) + c = (a+c).(b+c)
>
> >
> > The disputed forall is just the (2nd order) quantification over all
> > propositions.
>
> RunST is not the only disputed thing .
> newSTRef is also disputed.
>
> and what I was saying (UP TO NOW NOBODY could show where I was wrong)
> is the following:
>
> Hi, folks you can forget everything about this second order
quantification,
> the usual forall does all .
>
> What I want to say is this :
>
> put forall s. ST s a in a logical phrase . This is an invitation.
>
>
> By the way I am trying to forward my comments to the Haskell committee.
How
> can I reach them?
>
> It is a pleasure to know that somebody else than Marcin is also reading ,
> because the discussion is reaching the point
> where it will be yes against no . Please people don't come with books nor
with
> names to strengthen claims.
> Talk logically about it , try to define very clearly what you mean.
>
> >
> > > >I see no reason to change the notation of forall in types,
> > > > which coresponds to forall in formulas.
> > >
> > > This is your claim . I leave it to you to prove it
> >
> > Seems more an issue of explanation?!
>
> Sorry , I don't understand . In a logical language there are RELATIONS
> (formula's if you want) and TERMS (types if you want) and these
> 2 are distinct and shall ever be distinct. But if I can learn something
new
> , why not ?
>
> e.g. (a,b) is a tuple , a special TERM and no RELATION . But you and the
> Haskell committee are free to
> INTERPRET this as a AND b , but in that latter case a and b denote
> RELATIONS . In the former case
> a and b denote TERMS
>
> >
> > Cheers,
> > Thorsten
> >
> >
>
> May I forward this mail to the Haskell - mailing list?
I saw that your email allready found his way to the Haskell-list
>
> Very friendly
> Jan Brosius
>
