Completeness of Hoare logic relative to the standard model

Abstract

The general completeness problem of Hoare logic relative to the standard model N of Peano arithmetic has been studied by Cook, and it allows for the use of arbitrary arithmetical formulas as assertions. In practice, the assertions would be simple arithmetical formulas, e.g. of a low level in the arithmetical hierarchy. This paper further studies the completeness of Hoare Logic relative to N with assertions restricted to subclasses of arithmetical formulas. Our completeness results refine Cook’s result by reducing the complexity of the assertion theory.