Modeling arithmetic in the first-order language enriched with temporal quantifiers

We investigate the classical first-order language with equality enriched by the modalities of the computational tree logic $\bf CTL^\ast$. As a semantics for it we consider serial Kripke frames with constant domains. We construct an embedding of the truth arithmetics into the set of all formulas that are valid in the class of such frames. Then, we obtain some corollaries concerned algorithmical, syntactical, and semantical properties for a large class of logic in the language.