The Underlying Logic of Hoare Logic

Formulas of Hoare logic are asserted programs φ P ψ where P is a program and φ, ψ are assertions. The language of programs varies; in the 1980 survey of K. Apt, one finds the language of while programs and various extensions of it. But the assertions are traditionally expressed in first-order logic (or extensions of it). In that sense, first-order logic is the underlying logic of Hoare logic. We question the tradition and demonstrate, on the simple example of while programs, that alternative assertion logics have some advantages. For some natural assertion logics, the expressivity hypothesis in Cook’s completeness theorem is automatically satisfied.