Structural rules in FL: expressive power and cut elimination.
by
Nikolaos Galatos
Japan Advanced Institute of Science and Technology
Coauthors: Agata Ciabattoni, Kazushige Terui

Full Lambek calculus (FL) is one of the most important Gentzen-style systems for substructural logics. The system admits cut elimination and is decidable. Axiomatic extensions of FL are known as substructural logics and they include, classical, intuitionistic, linear, relevant and many-valued propositional logics. Its algebraic semantics is the variety FL of pointed residuated lattices, also known as FL-algebras.

Although not all extensions of FL enjoy cut elimination, we show that simple structural rules preserve cut elimination. Structural rules over FL correspond in general to quasi-equations over FL, but we identify a large class of separable structural rules that correspond to equations. Moreover, although not all separable rules preserve cut elimination, we show that every separable rule is equivalent to a (simple) rule that does preserve cut elimination. We describe an algorithm for obtaining such a simple rule, while a similar algorithm can be applied to separable equations to obtain simple ones. On the other hand, we show that there are structural rules that are not equivalent to a rule that preserves cut elimination.

The proof of cut elimination for structural rules is obtained using the theory of residuated frames, structures that form relational semantics for substructural logics. As a by-product of the proof we obtain that simple, hence also separated, equations are preserved under Dedekind-MacNeille completions of FL-algebras (or residuated lattices).

PDF

Date received: April 26, 2007