Definability in Dynamic Logic

ABSTRACT

We study the expressive power of various versions of Dynamic Logic and compare them with each other as well as with standard languages in the logical literature. One version of Dynamic Logic is equivalent to the infinitary logic LCK&ohgr;1&ohgr;, but regular Dynamic Logic is strictly less expressive. In particular, the ordinals &ohgr;&ohgr; and &ohgr; &ohgr;.2 are indistinguishable by formulas of regular Dynamic Logic.

REFERENCES

• 1: J. Barwise, Back and forth through Infinitary Logic, Studies in Model Theory, Mathematical Association of America, 1973.
• 2: A. Ehrenfeucht, An Application of Games to the Completeness Problem for Formalised Theories, Fundamenta Mathematicae 49, pp. 129–141.
• 3: David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 4: David Harel , Vaughan R. Pratt, Nondeterminism in logics of programs, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.203-213, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512782]
• 5: J. Keisler, Model Theory for Infinitary Logic, North Holland 1971.
• 6: A. Meyer, Ten Thousand and One Logics of Programming, EATCS Bulletin, to appear 1980.
• 7: Albert R. Meyer , Karl Winklmann, On the expressive power of Dynamic Logic (Preliminary Report), Proceedings of the eleventh annual ACM symposium on Theory of computing, p.167-175, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804410]
• 8: V. Pratt, Semantical Considerations in Floyd-Hoare Logic, Proc. 17th IEEE Symp. on FOCS, 1976, pp. 109–121.
• 9: H. Rogers, The Theory of Recursive Functions, McGraw-Hill, 1967.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Recursive function theory
      F.4.3 Formal Languages
          Subjects: Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets)

General Terms:
Theory