A generalization of analytic deduction via labelled deductive systems. Part 1: basic substructural logics

In this series of papers we set out to generalize the notion of classical analytic deduction (i.e., deduction via elimination rules) by combining the methodology of labelled deductive systems (LDS) with the classical systemKE. LDS is a unifying framework for the study of logics and of their interactions. In the LDS approach the basic units of logical derivation are not just formulae butlabelled formulae, where the labels belong to a given labelling algebra. The derivation rules act on the labels as well as on the formulae, according to certain fixed rules of propagation. By virtue of the extra power of the labelling algebras, standard (classical or intuitionistic) proof systems can be extended to cover a much wider territory without modifying their structure. The systemKE is a new tree method for classical analytic deduction based on analytic cut.KE is a refutation system, like analytic tableaux and resolution, but it is essentially more efficient than tableaux and, unlike resolution, does not require any reduction to normal form. We start our investigation with the family of substructural logics. These are logical systems (such as Lambek''s calculus, Anderson and Belnap''s relevance logic, and Girard''s linear logic) which arise from disallowing some or all of the usual structural properties of the notion of logical consequence. This extension of traditional logic yields a subtle analysis of the logical operators which is more in tune with the needs of applications. In this paper we generalize the classicalKE system via the LDS methodology to provide a uniform refutation system for the family of substructural logics. The main features of this generalized method are the following: (a) each logic in the family is associated with a labelling algebra; (b) the tree-expansion rules (for labelled formulae) are the same for all the logics in the family; (c) the difference between one logic and the other is captured by the conditions under which a branch is declared closed; (d) such conditions depend only on the labelling algebra associated with each logic; and (e) classical and intuitionistic negations are characterized uniformly, by means of the same tree-expansion rules, and their difference is reduced to a difference in the labelling algebra used in closing a branch. In this first part we lay the theoretical foundations of our method. In the second part we shall continue our investigation of substructural logics and discuss the algorithmic aspects of our approach.