The Lambek Calculus: Relational Semantics and the Method of Labelling
Natasha Kurtonina

Abstract:
Relational Semantics as it is introduced in [vB88], [vB91], [Bus.86] 
and [Or89] provides a dynamic interpretation for the Lambek Calculus: 
valuation of formulae is carried out on pairs of points, which can be 
treated as informational states. Propositions can be understood as 
programs of transformation of informational states. In [M92] Szabolcs 
Mikulas presents an algebraic proof of the corresponding Completeness 
Theorem.
The purpose of this paper is to propose a new, rather simple completeness 
proof by using the method of labelling. The general theory of labelled 
deductive systems is proposed by D.Gabbay. In the labelled version of 
the Lambek Calculus a pair of labels is attached to every formula and 
the way of labelling reflects corresponding semantical truth conditions. 
Straighforward parallelism between syntax and semantics enables one to 
obtain the completeness result.