Expressiveness and the completeness of Hoare's logic

Abstract

The authors prove three theorems about completeness issues regarding Hoare's logic for while-programs: (1) expressiveness is not a necessary condition on a structure for the completeness of its Hoare logic, (2) complete number theory is the only extension of Peano Arithmetic which yields a logically complete Hoare logic and (3) a computable structure with enumeration is expressive iff its Hoare logic is complete. Here expressiveness means the ability of expressing strongest postconditions in first-order formulas over the structure concerned; a Hoare logic H is called complete relative to a structure A if any partial correctness formula valid over A is provable in H, where facts about A can be used as an oracle; a Hoare logic H is called logically complete with respect to a specification (theory) T if any partial correctness formula that is valid on all models of T is provable in H. The authors conclude from (1) that in general Cook's analysis of the completeness of Hoare logic is not sufficient, but also that by (3), in the most interesting cases in which computable structures are involved, Cook's notion of expressiveness is enough for the study of completeness. Since for every finite structure expressiveness is guaranteed, their Hoare logics are always complete. Moreover, for every infinite computable structure it is proved to be possible to enrich the signature, such that expressiveness becomes equivalent to completeness of the Hoare logic relative to the enriched structure. However, it is still an open problem whether this also holds in general for the original (infinite computable) structure. Finally a note on the use of Lemma 4.5 in the proof of Theorem 4.3 on p. 277: the three bottom lines have to be replaced by: ''From Lemma 4.5 and II(d) we obtain ⊢¬φ(x)→∀y(x≠y)''.