Axiomatizing the lexicographic products of modal logics with linear temporal logic

Abstract

Given modal logics L1 and L2, their lexicographic product L1 x L2 is a new logic whose frames are the Cartesian products of an L1-frame and an L2-frame, but with the new accessibility relations reminiscent of a lexicographic ordering. This article considers the lexicographic products of several modal logics with linear temporal logic (LTL) based on ``next'' and ``always in the future''. We provide axiomatizations for logics of the form L x LTL and define cover-simple classes of frames; we then prove that, under fairly general conditions, our axiomatizations are sound and complete whenever the class of L-frames is cover-simple. Finally, we prove completeness for several concrete logics of the form L x LTL.