Fixpoints in generalized Lambek calculus

Abstract

Modal logics with ϐixpoint operators have received considerable attention (e.g. dynamic logic with program iteration [3] or epistemic logic with common knowledge [2]). In this talk we discuss a positive modal logic with a binary update modality \ and its fixpoint version \∗. The update operator is a generalized version of the left division of the (non-associative) Lambek calculus. The difference is that while the Lambek left division has a relational semantics using a ternary relation on a set, the generalized \ uses a ternary relation between elements of a set, subsets of that set and members of that set. Our main technical result is a complete axiomatization of a relational semantics for the logic and a decidability result. The technique used to obtain these results is a modiϐication of the techniques used in the case of more standard ϐixpoint operators such as program iteration or common knowledge. In a sense, this work generalizes the work of Bimbó and Dunn [1] on relational semantics for the logic of Kleene algebras.