Linear Logic in View of Bounded Structural Rules

Andreja Prijatelj

In this paper we shall present an alternative living space of linear logic in view of bounded structural rules. The main purpose being to explore the famous completeness problem of linear logic from a different angle. It is well-known that the main difficulty of the problem mentioned is caused by the presence of modalities ’of course’ and ’why not’. In order to avoid this obstacle we shall consider particular axiomatic systems of modality free linear logic enriched with some bounded structural rules instead. To ensure the cut-elimination property the systems are firstly based on two-fold sequents following the idea of Girard’s LU [1]. A two-fold sequent consists of a linear part and a separated classical part. The former is inhabited with usual linear logic formulas (without explicit modalities) and the latter with modalized formulas in disguise. A bounded structural operation may act solely on formulas within a classical part, while the usual linear two-premiss ’tensor’ and ’par’ rules are suitably modified to help recovering the visual absence of both modalities. The two parts may also communicate with each other by the so-called switching rules. We shall show that there are faithfull embeddings of the systems considered into linear logic. Ultimately the two-fold systems can be transformed into equivalent linear systems mimicing the intended effects of linear logic modalities.

References:

(1) J.-Y. Girard, Linear Logic: a survey, in Bauer, Brauer, and Schwichtenberg (eds), Logic and Algebra of Specification, Heidelberg, 1993, 63-112.

(2) J.-Y. Girard, Y. Lafont, L. Reigner (eds), Advances in Linear Logic, London Math. Soc. Lec. No.

222. Cam. U.P., 1995.

(3) A. Prijatelj, From Bounded Structural Rules to Linear Logic Modalities, manuscript, Paris 1999.

Address: Department of Mathematics, University of Ljubljana, Slovenia

E-mail: Andreja.Prijatelj@fmf.uni-lj.si