Correspondence results for relational proof systems with application to the Lambek calculus (Q1850953)

The aim of the paper is to present a general framework for proof systems for relational theories. The authors describe logics of relations and proof systems, being Rasiowa-Sikorski style deductive systems, for these logics. They give principles of a construction of deduction rules which represent the same information as specific axioms and which can replace these axioms in deduction processes. They discuss correspondences reflecting relationships between semantics of relational logics and rules of the appropriate proof systems. The methods outlined in the paper are illustrated by examples concerning relational interpretation of Lambek syntactic calculus and some of its extensions. An extensive list of 41 references is given.