Model theory for tense logic: Saturated and special models with applications to the tense hierarchy

The aims of this paper are: (1) to present tense-logical versions of such classical notions as saturated and special models; (2) to establish several fundamental existence theorems about these notions; (3) to apply these powerful techniques to tense complexity.In this paper we are concerned exclusively with quantifiedK₁ (for linear time) with constant domain. Our present research owes much to Bowen [2], Fine [5] and Gabbay [6].