Summary: Traditional model theory (Chang and Keisler 1973, Bell and Slomson 1971), like classical predicate logic, is static in nature. Models, valuations of variables, and truth values of predicates are regarded as fixed and immutable. This tradition has surely contributed to the dominance of denotational over operational semantics in programming languages. It is somewhat ironic that first-order predicate logic is in general inadequate for handling even the most elementary and pervasive of logical constructions in computer science, namely induction. For this reason, and for its general lack of programmability, one might argue that the emphasis on first-order predicate logic in the undergraduate computer science curriculum may be detrimental to the development of sound algorithmic reasoning. Dynamic logic and other logics of programs allow one to study properties of models from a natural computational perspective. Instead of attempting to strip away all traces of dynamics from the objects under study, a programming language and data structures are provided along with a formal semantics that allow one to reason in a natural algorithmic way and still maintain rigor. In this talk we will show how trace-based and relational Kleene algebras with tests (KAT) built upon first-order (Tarskian) Kripke frames can be used to give a natural semantics for studying the dynamic properties of models. We prove the following results: Let \(V\) be a fixed vocabulary. Given a recursive atomic theory \(E\) over \(V\), we exhibit a Kripke frame \(U\) whose trace algebra is universal for Tarskian trace algebras over \(V\) satisfying \(E\), although \(U\) itself is not Tarskian. Using \(U\), we show:
1.) The following problem is r.e.-complete: given a recursive atomic theory \(E\) over \(V\), a scheme \(S\) over \(V\), and input values specified by ground terms \(t_1,\dots,t_n\), does \(S\) halt on input \(t_1,\dot,T_n\) in all models of \(E\)? The traditional halting problem for program schemes (see Manna 1974) is the case where \(E\) is empty.
2.) The following problem is \(\Pi^0_2\)-complete: given a recursive atomic theory \(E\) over \(V\) and two schemes \(S\) and \(T\) over \(V\), are \(S\) and \(T\) equivalent in all models of \(E\)? The classical scheme equivalence problem (see Manna 1974) is the case where \(E\) is empty.
Both these problems remain hard for their respective complexity classes even if \(E\) is empty and \(V\) is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate.
For the entire collection see [Zbl 0993.00042].