Relative completeness

In computer science, relative completeness, or completeness in the sense of Cook, is a property of a formal system relying on weakest preconditions, which holds when every true formula can be derived over said language both by use of weakest liberal preconditions, and by assuming a sufficiently strong axiomatic system, as to provide as a weaker alternative to the usual notion of completeness.

Background

Developed in 1974 by Stephen Cook, relative completeness sidesteps the pitfalls of logical completeness: given a complete Hoare logic with respect to some language and axiomatic system, it is possible to solve the halting problem with the consequence rule thanks to the Hoare triple ${\displaystyle {\{{\texttt {true}}\}S\{{\texttt {false}}\}}}$, which is true if and only if ${\displaystyle S}$ never terminates. As such, no Hoare logic over some Turing-complete language can ever be complete, regardless of the assertion language. Similarly, the Hoare triple ${\displaystyle {\{{\texttt {true}}\}{\texttt {skip}}\{S\}}}$ is true if and only if ${\displaystyle S}$ is true. Consequently, any complete Hoare logic must be over a sound and complete axiomatic system regardless of language, which must be unaxiomatizable by Gödel's incompleteness theorems. As such, and as witnessed by both Hoare tuples, Hoare logic is at most as complete as its backing language and axiomatic system: this result is referred to as the relative completeness of Hoare logic.

To remedy this, relative completeness bestows the system with an oracle that decides the validity of assertions such as ${\displaystyle S}$, or, equivalently, a proof system which determines all true statements to be axioms, while also changing the use of weakest preconditions in some formal system to weakest liberal preconditions. These two changes prevent the two above counterexamples, and ergo preserve a useful definition for completeness of a formal system relying on weakest preconditions. This notion is commonly referred to as relative completeness, and is commonly used to provide a useful notion of completeness for other formal systems.

References