On the linear decoration of intuitionistic derivations
type: Item
instance of: scholarly article
title: On the linear decoration of intuitionistic derivations
zbMATH Open document ID: 0820.03036
DOI: 10.1007/BF02390456
author: Vincent Danos
author: Jean-Baptiste Joinet
author: Harold Schellinx
published in: Archive for Mathematical Logic
publication date: 1995-09-11T00:00:00Z
review text: Uniform translations of intuitionistic into linear logic, with their plethoric use of exponentials, are bound to give only `universal linearity information' about proofs. This paper aims at displaying the structure of `specific linearity information' hidden in a given derivation by constructing a proof-by-proof embedding of intuitionistic sequent calculus into linear logic such that: (1) the skeleton of the original proof is preserved (the linear proof is a `decoration' of the intuitionistic one), (2) each exponential in the image is necessary, as it is required by some instance of a contraction or weakening rule somewhere in the proof. A notion of `lower decoration strategy' is defined, which for the neutral intuitionistic fragment of Girard's `Unified Logic' (LU) results in a subdecoration of the uniform decoration obtained using the well-known translation of intuitionistic into linear logic. In fact, the linear proof obtained is an optimal linear version of the original LU- derivation, with essentially the same set of reductions. This is the first in a series of papers, all of which make use of linear logic as a proof-theoretical tool. An in-depth analysis of the normalization of classical sequent calculus is given in the sequel ``A new deconstructive logic: linear logic'' (to appear in J. Symb. Logic, and available via anonymous ftp or at http://boole.logique.jussieu.fr/www.hars/djs.html).
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03B20
zbMATH DE Number: 734552
zbMATH Keywords: proof theory
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: unified logic
zbMATH Keywords: linear logic
zbMATH Keywords: proof- by-proof embedding
zbMATH Keywords: intuitionistic sequent calculus
zbMATH Keywords: translation
MaRDI profile type: Publication
cites work: Q4842975
cites work: Q4282602
cites work: A new deconstructive logic: linear logic
cites work: Linear logic
cites work: On the unity of logic
cites work: Q4474830
cites work: Some Syntactical Observations on Linear Logic
description: scientific article; zbMATH DE number 734552