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 1 (for linear time) with constant domain. Our present research owes much to Bowen [2], Fine [5] and Gabbay [6].

It is shown that de re formulas are eliminable in the modal logic S5 extended with the axiom scheme □∃xφ ⊃ ∃x□φ.