Classical multiplicative linear logic - intuitionistic mll.

Аннотация

It is known how to present every deduction in the {!, I}-free Classical Multiplicative Linear Logic as (the result of an obvious translation of) a deduction in the intuitionistic MLL. We extend the result to the language with I and give short proofs which do not use proof nets.