Normal deduction in the intuitionistic linear logic
type: Item
instance of: scholarly article
title: Normal deduction in the intuitionistic linear logic
zbMATH Open document ID: 0936.03058
published in: Archive for Mathematical Logic
publication date: 2000-05-15T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F52
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 1210625
zbMATH Keywords: linear logic
zbMATH Keywords: normalization
zbMATH Keywords: cut elimination
zbMATH Keywords: second order
zbMATH Keywords: natural deduction
author: G. E. Mints
reviewed by: Serguei V. Solov'ev
MaRDI profile type: Publication
full work available at URL: s001530050106
OpenAlex ID: W2088514694
DOI: 10.1007/S001530050106
description: scientific article; zbMATH DE number 1210625