On the linear decoration of intuitionistic derivations (Q1345901): Difference between revisions

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).