Completeness of Hoare Logic Relative to the Standard Model

摘要

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.