Some general incompleteness results for partial correctness logics (Q1110500)

For \textit{C. A. R. Hoare}'s calculus of partial correctness proofs of programs [Commun. ACM 12, 567-580 (1969; Zbl 0179.231)] incompleteness theorems have been proved, e.g., by \textit{H. Andréka}, \textit{I. Németi} and \textit{I. Sain} [Lect. Notes Comput. Sci. 74, 208-218 (1979; Zbl 0411.03017)] and by \textit{J. A. Bergstra} and \textit{J. V. Tucker} [Theor. Comput. Sci. 17, 303-315 (1982; Zbl 0483.68033)]. The authors prove strengthened versions of those results which assume only very weak assumptions on the data type specifications as, e.g., the possibility of simulating arbitrarily long finite segments of the integers, and they also give recursion theoretic complexity results for relevant sets of sentences of Hoare's logics.