An Axiomatic Approach to Structural Rules for Locative Linear Logic
Jean‐Marc Andreoli · Cambridge University Press eBooks · 2004
This paper proposes a generic, axiomatic framework to express and study structural rules in resource conscious logics derived from Linear Logic. The proposed axioms aim at capturing minimal concepts, operations and relations in order to build an inference system which extends that of Linear Logic by the introduction of structure and structural rules, but still preserves in a very natural way the essential properties of any logical inference system: Cut elimination and Focussing. We consider here finite but unbounded structures, generated from elementary structures called “places”. The set of places is “isotropic”, in that no single place has a distinguished role in the structures, and each structure can be “transported” into an isomorphic structure by applying a permutation of places to the places from which it is built. The essential role of these places in the definition of Logic has been shown in Ludics, and leads to a locative reading of the traditional logical concepts (formulas, sequents, proofs), which is adopted here. All the logical connectives (multiplicatives, additives, exponentials) are expressed here in a locative manner. Introduction Linear Logic essentially differs from Classical Logic by the removal of the structural axioms of Contraction and Weakening. However, it retains other structural axioms, such as Exchange, which determine the essential properties of the whole system. Thus, from a sequent calculus point of view, Linear Logic sequents are built from a single constructor (usually represented as the “comma”) which is structurally considered associative-commutative, and hence, so are all the binary connectives. The structure of commutative monoid underlying phase semantics also results from this choice.