Relational semantics and a relational proof system for full Lambek calculus

AbstractIn this paper 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 Γ → α in FL is provable if and only if a translation,t(γ1● … ● γn⊃ α)ευu, has a cut-complete fundamental proof tree. This result isconstructive: that is, if a cut-complete proof tree fort(γ1● … ● γn⊃ α)ευuis not fundamental, we can use the failed proof search to build a relational countermodel fort(γ1● … ● γn⊃ α)ευuand from this, build a RelKripke countermodel for γ1● … ● γn⊃ α. 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.

Relational semantics and a relational proof system for full Lambek calculus Journal Articles