On the Completeness of Dynamic Logic

摘要

The impossibility of semantically complete deductive calculi for logics for imperative programs has led to the study of two alternative approaches to completeness: "local" semantic completeness on the one hand (Cook's relative completeness, Harel's Arithmetical completeness), and completeness with respect to other forms of reasoning about programs, on the other. However, local semantic completeness is problematic on several counts, whereas proof theoretic completeness results often involve ad hoc ingredients, such as formal theories for the natural numbers.rnThe notion of inductive completeness, introduced in [18], provides a generic proof theoretic framework which dispenses with extraneous ingredients, and yields local semantic completeness as a corollary.rnHere we prove that (first-order) Dynamic Logic for regular programs (DL) is inductively complete: a DL-formula φ is provable in (the first-order variant of) Pratt-Segerberg deductive calculus DL iff φ, is provable in first-order logic from the inductive theory for program semantics. The method can be adapted to yield the schematic relative completeness of DL: if S is an expressive structure, then every formula true in S is provable from the axiom-schemas that are valid in S. Harel's Completeness Theorem falls out then as a special case.