Questions on LU and ITT
(This message was earlier posted to the logic mailing
list, but no responses were received.)
I seem to have evermore questions as I learn more about proof theory, linear
logic and LU.
1. Has a sequent presentation of Martin-Lo"f Intuitionistic Type Theory been
2. The next pair of questions are about the Intuitionistic fragments of LU
and their relation to the traditional sequent calculi for Intuitionistic
From my undersanding of Girard's paper on LU, the translation of the
intuitionistic fragments of LU into the traditional sequent calculi for
intuitionistic logic are straightforward, but the other way things may
be more delicate. Has someone proven a result showing that cut-free
(resp. not necessarily cut free) intuitionistic proofs translate into
cut-free (resp. not necessarily cut free) proofs within the intuitionistic
fragment of LU (i.e. with sequents maintaining the specified restrictions
at each stage in the proof).
I would appreciate any information on the connections between LU's
intuitionistic fragment and usual calculi for intuitionistic logic.
Sanjiva Prasad, Guest Magus E-mail: email@example.com
European Computer Industry Research Centre Off: +49 89 92 69 91 58
Arabellastrasse 17 Fax: +49 89 92 69 91 70
8000 Muenchen 81, Germany Res: +49 89 16 33 59