Relative completeness of the Hoare partial correctness calculus

If we consider a sufficiently expressive logical language, for example, the language of first order arithmetic, then, by Gödel’s incompleteness theorems, the consequence rule incorporates incompleteness into Hoare logic. That is, there exist true partial correctness formulas which cannot be deduced by the Hoare partial correctness calculus. By making use of the expressibility result of the previous section, we can prove, however, relative completeness of the Hoare calculus. This means that, if we assume true arithmetical formulas as provable, then every true partial correctness formula is derivable in the Hoare calculus.

Theorem 50. Let be an interpretation, assume is expressive for Form and Com, where Form is the set of formulas of the underlying logical language. Let . Then for every and P,

Proof. By structural induction on .

  • If , then, by Definitions 22 and 16, . The proof of is obtained by applying the consequence rule with , and .

  • : again, by Definitions 22 and 16, this implies . The result follows by applying the consequence rule to , and .

  • : then . By the expressiveness, let and . By induction hypothesis, and are provable. By the composition rule, is also provable, and, taking into account and , the consequence rule yields the result.

  • : then, by Definition 16, iff and or and . This means, either or holds, which, by the induction hypothesis, gives the result.

  • : iff property of Lemma 48 is true. Let and . Assume by property , this implies . Otherwise, if , , and . Since , by Lemma 44, we have . But holds, as well, which means . By the while rule we obtain . Lemma 44 gives , moreover, by Lemma 21, , hence the statement follows.

The question of completeness of Hoare’s calculus with respect to various underlying theories are examined in detail in [3]. Incompleteness either stems from the weakness of the underlying theory, like in the case of abacus arithmetic, or, if the theory is strong enough to capture sets of states expressing pre- or postconditions in proofs of completeness, the new obstacle is raised by Gödel’s theorem saying that there are true formulas unprovable in Peano arithmetic. Strangely enough, there are even interpretations of arithmetic for which Hoare’s logic is complete but the interpretations itselves are not expressive. The interested reader is referred to [3].