A simple dynamic logic (Q1087866)

In this paper a system of dynamic predicate logic is presented. Its distinctive features are as follows: (1) It is finitary, allowing nonstandard models of time; (2) It is essentially one-sorted, identifying time elements and data elements. After the soundness and completeness theorems are established, it is shown that this system is equivalent to the three-sorted systems due to \textit{H. Andréka}, \textit{I. Németi} and \textit{I. Sain} [Theor. Comput. Sci. 17, 193-212 and 259-278 (1982; Zbl 0475.68009 and Zbl 0475.68010)] with a conservation result for the latter system as a by-product.