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. © 1982.
Bergstra, J. A., & Tucker, J. V. (1982). Expressiveness and the completeness of Hoare’s logic. Journal of Computer and System Sciences, 25(3), 267–284. https://doi.org/10.1016/0022-0000(82)90013-7