First-Order Definability of Transition Structures

The transition semantics presented in Rumberg :77–108, 2016a) constitutes a fine-grained framework for modeling the interrelation of modality and time in branching time structures. In that framework, sentences of the transition language \ are evaluated on transition structures at pairs consisting of a moment and a set of transitions. In this paper, we provide a class of first-order definable Kripke structures that preserves \-validity w.r.t. transition structures. As a consequence, for a certain fragment of \, validity w.r.t. transition structures turns out to be axiomatizable. The result is then extended to the entire language \ by means of a quite natural ‘Henkin move’, i.e. by relaxing the notion of validity to bundled structures.