Hoare's Logic Is Not Complete When It Could Be

Abstract

It is known (cf.[2]) that is the Hoare rules are complete for a first-order structure A, then the set of partial correctness assertions true over A is recursive in the first-order theory of A. We show that the converse is not true. Namely, there is a first-order structure C such that the set of partial correctness assertions true over C is recursive in the theory of C, but the Hoare rules are not complete for C.