Some Results in Dynamic Model Theory
Journal Article - Open Access
Cornell University Ithaca United States
Pagination or Media Count:
First-order structures over a fixed signature give rise to a family of trace-based and relational Kleene algebras with tests defined in terms of Tarskian frames. A Tarskian frame is a Kripke frame whose states are valuations of program variables and whose atomic actions are state changes elected by variable assignments x e, where e is a Epsilon term. The Kleene algebras with tests that arise in this way play a role in dynamic model theory akin to the role played by Lindenbaum algebras in classical first-order model theory. Given a first-order theory T over Epsilon, we exhibit a Kripke frame U whose trace algebra TrU is universal for the equational theory of Tarskian trace algebras over Epsilon satisfying T, although U itself is not Tarskian in general. The corresponding relation algebra RelU is not universal for the equational theory of relation algebras of Tarskian frames, but it is so modulo observational equivalence.
- Theoretical Mathematics