Normal deduction in the intuitionistic linear logic (Q1267849): Difference between revisions

A natural deduction system NDIL for second-order intuitionistic linear logic is considered. It is an extension of a natural deduction system for !-free multiplicative intuitionistic linear logic proposed earlier by author and elaborated by A. Babaev. The (known) sequent formulation GIL and Prawitz transformation to this calculus are used to obtain a normalization theorem for NDIL. The scheme is the following: NDIL derivation \(\rightarrow\) GIL derivation \(\rightarrow\) normalization theorem for GIL (known) \(\rightarrow\) reduction sequence for NDIL. Special feature: treatment of the modality ! is inspired by Prawitz treatment of S4 combined with a construction \(\langle\dots\rangle\) introduced by the author to avoid cut-like constructions used in \(\otimes\) elimination and global restrictions employed by Prawitz. It should be noted that normal form is considered w.r.t. \(\beta\)-reduction (only). Assignment of terms and normalization are considered with the fragment with linear implication, \(\&\) and \(\otimes\). The proof of strong normalization in the case with tensor unit is sketched.