# Non-uniformity of dynamic logic

Extended abstract

Conference paper

First Online:

## Abstract

Harel proved that the dynamic logic is complete in the class of arithmetical interpretations. The set of natural numbers stands for primitive notion in arithmetical interpretations, i.e. the following condition holds: "there exists a unary relation symbol nat such that for every arithmetical interpretation I, nat_{I} is the set of natural numbers". It is proved that the completeness is lost when this condition is relaxed to the following one: "for every interpretation^{I} involved, the set of natural numbers is first-order definable in I". Thus we prove that the dynamic logic is not relatively complete in the sense of Cook.

## Preview

Unable to display preview. Download preview PDF.

## References

- [1]Clarke E., M. Jr., The characterization problem for Hoare Logics, Carnegie-Mellon Univ. report CMU-CS-84-109, 1984Google Scholar
- [2]Grabowski M., On relative incompleteness of logics for total correctness, Proc. of Logics of Programs 85 conf., New York, Brooklyn, Lect. Notes in Comp. Sc., 1985Google Scholar
- [3]Harel D., Logics of programs: axiomatics and descriptive power, Report MIT/LCS/TR-200, 1978Google Scholar
- [4]Shoenfield J., Mathematical Logic, 1967Google Scholar

## Copyright information

© Springer-Verlag Berlin Heidelberg 1985