Relative completeness

In computer science, relative completeness, or completeness in the sense of Cook,^[1] 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,^[2] 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 ${\{{\texttt {true}}\}S\{{\texttt {false}}\}}$ , which is true if and only if $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 ${\{{\texttt {true}}\}{\texttt {skip}}\{S\}}$ is true if and only if $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.^[3]

To remedy this, relative completeness bestows the system with an oracle that decides the validity of assertions such as $S$ ,^[3] or, equivalently, a proof system which determines all true statements to be axioms,^[4] while also changing the use of weakest preconditions in some formal system to weakest liberal preconditions.^[5] 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.^[6]

References

↑ de Boer, Frank S.; Hiep, Hans-Dieter A. (2021-12-31). "Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic". ACM Transactions on Programming Languages and Systems. 43 (4): 1–35. doi:10.1145/3477143. ISSN 0164-0925. Retrieved 2026-10-10.
↑ Cook, Stephen A. (1978). "Soundness and Completeness of an Axiom System for Program Verification". SIAM Journal on Computing. 7 (1): 70–90. doi:10.1137/0207005. ISSN 0097-5397. Retrieved 2026-10-10.
1 2 "CS 4110: Programming Languages and Logics - Lecture 9: Relative Completeness" (PDF). Cornell Ann S. Bowers College of Computing and Information Science. Department of Computer Science, Cornell University. 2012. Archived (PDF) from the original on 2024-04-15. Retrieved 2026-10-09.
↑ Dal Lago, Ugo; Gaboardi, Marco (2011). Linear Dependent Types and Relative Completeness. IEEE. p. 133–142. doi:10.1109/LICS.2011.22. ISBN 978-1-4577-0451-2. Retrieved 2026-10-10.
↑ Apt, Krzysztof R.; Boer, Frank S. de; Olderog, E.-R. (2009). "3.5 Completeness". Verification of sequential and concurrent programs. New York London: Springer. pp. 85–91. ISBN 978-1-84882-745-5.
↑ Apt, Krzysztof R. (1981). "Ten Years of Hoare's Logic: A Survey—Part I". ACM Transactions on Programming Languages and Systems. 3 (4): 431–483. doi:10.1145/357146.357150. ISSN 0164-0925. Retrieved 2026-10-10.

P ≟ NP

This theoretical computer science–related article is a stub. You can help Wikipedia by adding missing information.

[l796-1] Boer, Frank S.; Hiep, Hans-Dieter A. (2021-12-31). "Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic". ACM Transactions on Programming Languages and Systems. 43 (4): 1–35. doi:10.1145/3477143. ISSN 0164-0925. Retrieved 2026-10-10.

[e473-2] Cook, Stephen A. (1978). "Soundness and Completeness of an Axiom System for Program Verification". SIAM Journal on Computing. 7 (1): 70–90. doi:10.1137/0207005. ISSN 0097-5397. Retrieved 2026-10-10.

[cslecture-3] 1 2 "CS 4110: Programming Languages and Logics - Lecture 9: Relative Completeness" (PDF). Cornell Ann S. Bowers College of Computing and Information Science. Department of Computer Science, Cornell University. 2012. Archived (PDF) from the original on 2024-04-15. Retrieved 2026-10-09.

[g328-4] Dal Lago, Ugo; Gaboardi, Marco (2011). Linear Dependent Types and Relative Completeness. IEEE. p. 133–142. doi:10.1109/LICS.2011.22. ISBN 978-1-4577-0451-2. Retrieved 2026-10-10.

[c629-5] Apt, Krzysztof R.; Boer, Frank S. de; Olderog, E.-R. (2009). "3.5 Completeness". Verification of sequential and concurrent programs. New York London: Springer. pp. 85–91. ISBN 978-1-84882-745-5.

[c804-6] Apt, Krzysztof R. (1981). "Ten Years of Hoare's Logic: A Survey—Part I". ACM Transactions on Programming Languages and Systems. 3 (4): 431–483. doi:10.1145/357146.357150. ISSN 0164-0925. Retrieved 2026-10-10.

[1]

[2]

[3]

[4]

[5]

[6]