Labelled Tableau Calculi Generating Simple Models for Substructural Logics
Kazushige Terui

Abstract:
In this paper we apply the methodology of Labelled Deductive Systems to the 
tableau method in order to obtain a deductive framework for substructural 
logics which incorporates the facility of model generation. For this 
special purpose, we propose new labelled tableau calculi TL and TLe for two 
substructural logics L (essentially the Lambek calculus) and Le (the 
multiplicative fragment of intuitionistic linear logic). The use of labels 
makes it possible to generate countermodels in terms of a certain very 
simple semantics based on monoids, which we call the simple semantics. We 
show that, given a formula C as input, every nonredundant tableau 
construction procedure for TL and TLe terminates in finitely many steps, 
yielding either a tableau proof of C or a finite countermodel of C in 
terms of the simple semantics. It shows the finite model property for L 
and Le with respect to the simple semantics.