On completeness of dynamic topological logic

A classical result on topological semantics of modal logic due to McKinsey and Tarski (often called Tarski theorem) states that the logic S4 is complete with respect to interpretations in $\mathbb R^n$ for each $n$. Recently several authors have considered dynamic topological logics, which are interpreted in dynamic spaces (abstract dynamic systems). A dynamic space is a topological space together with a continuous function on it. Artemov, Davoren, and Nerode introduced a bimodal logic S4C and proved it to be complete with respect to the class of all dynamic spaces. A number of polymodal logics for dynamic topological systems were considered by Kremer, Mints, and Rubakov. Earlier the author showed that the analogue of Tarski theorem does not hold for S4C; this result has also been established independently from the author by P. Kremer and later by J. van Benthem (private communication). In this paper we show that a certain generalization of Tarski theorem applies in the dynamic case. We prove that for any formula $\phi$ underivable in S4C there exists a countermodel in $\mathbb R^n$ for $n$ sufficiently large. We give also an upper bound on the dimension of a refuting model. It remains an open question whether our upper bound is exact.