Two theorems about the completeness of Hoare's logic (Q794426)

This paper continues a series of papers of these authors on Hoare's logic and its proof theory. The issue that is addressed here is the genericity of Hoare's logic among all possible logics for partial correctness of while-programs. The results of this paper indicate that, in some sense, Hoare's logic is generic. The main result is as follows. Let (\(\Sigma\),E) be some axiomatic specification, where \(\Sigma\) is a finite signature and E is a set of axiom written in \(L(\Sigma)\), the first-order language over \(\Sigma\). If this specification has only infinite models, then it can be extended to a specification \((\Sigma ',E'),\) i.e., \(\Sigma \subseteq \Sigma '\) and \(E\subseteq E',\) such that Hoare's logic is complete for partial correctness of while-programs over \((\Sigma ',E').\) Furthermore, this extension is conservative both for first-order assertions and partial correctness assertions. That is, if \(\phi\) is an assertion over \(\Sigma\), and \(\phi\) is true in all models of \((\Sigma ',E'),\) then \(\phi\) is true in all models of (\(\Sigma\),E).