Expressiveness and the completeness of Hoare's logic

Abstract

Three theorems are proven which reconsider the completeness of Hoare's logic for the partial correctness of while-programs equipped with a first-order assertion language. The results are about the expressiveness of the assertion language and the role of specifications in completeness concerns for the logic: (1) expressiveness is not a necessary condition on a structure for its Hoare logic to be complete, (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 if and only if its Hoare logic is complete.