Relational semantics and a relational proof system for full Lambek calculus

In this pager we give relational semantics and an accompanying relational proof theory for full Lambek calculus (a sequent calculus which we denote by FL). We start with the Kripke semantics for FL as discussed in [11] and develop a second Kripke-style semantics, RelKripke semantics, as a bridge to relational semantics. The RelKripke semantics consists of a set with two distinguished elements, two ternary relations and a List of conditions on the relations. It is accompanied by a Kripke-style valuation system analogous to that in [11]. Soundness and completeness theorems with respect to FL hold for RelKripke models. Then, in the spirit of the work of Orlowska [14], [15], and Buszkowski and Orlowska [3], we develop relational logic RFL. The adjective relational is used to emphasize the fact that RFL has a semantics wherein formulas are interpreted as relations. We prove that a sequent Gamma --> alpha in FL is provable if and only if a translation, t(y(1 )..... gamma(n) superset of alpha)epsilon upsilon u, has a cut-complete fundamental proof tree This result is constructive: that is, if a cut-complete proof tree for t(gamma(1) ..... gamma(n) superset of alpha)epsilon upsilon u is not fundamental, we can use the failed proof search to build a relational countermodel for t(gamma(1) ..... gamma(n) superset of alpha)epsilon upsilon u and from this, build a RelKripke countermodel for gamma(1) ..... gamma(n) superset of alpha. These results allow us to add FL, the basic substructural logic, to the list of those logics of importance in computer science with a relational proof theory.