Thorsten Altenkirch writes:
> 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".
BTW there is a C-H correspondence for classical logic too, although it
requires a constructive presentation of the rules and considerable care with
reduction laws. The trick is to model the type of a continuation as a negated
proposition, with reductio ad absurdum as a call/cc-like operation.
See for example:
C.-H. L. Ong, A semantic view of classical proofs: type-theoretic,
categorical, denotational characterizations. In Proceedings of 11th IEEE
Annual Symposium on Logic in Computer Science, IEEE Computer Society Press,
pp. 230-241, 1996.
--
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
