A unifying theorem for algebraic semantics and dynamic logics (Q1821095)

Various logics have been proposed and studied for expressing and proving program properties. This paper considers the problem whether the class of models of a logic is first-order definable, yielding a general tool to prove that it is not first-order axiomatizable if it is indeed not. The authors show, by using the technical tool of ultraproducts, that a class of structures which is first-order axiomatizable is bounded in the sense that all iterations stop after a finite number of steps. They apply this idea to continuous algebras, dynamic algebras and general computational models of programs. They deduce as easy corollaries of the main theorem the results of \textit{A. J. Kfoury} and \textit{D. M. Park} [Inf. Control 29, 243-251 (1975; Zbl 0329.68015)] and \textit{B. Courcelle} and \textit{I. Guessarian} [J. Comput. Syst. Sci. 17, 388-413 (1978; Zbl 0392.68009)] and others.