On Completeness Results of Hoare Logic Relative to the Standard Model

TL;DR

This paper investigates the completeness of Hoare logic relative to the standard model of Peano arithmetic, showing that restricting assertions to simpler formulas and inputs to N reduces the complexity of the assertion theory needed for completeness.

Contribution

It refines Cook's completeness results by demonstrating that restricting assertions and inputs simplifies the assertion theory required for Hoare logic's completeness.

Findings

Restricting assertions to subclasses of arithmetical formulas reduces complexity.

Input restriction to N simplifies the assertion theory.

Refined completeness results improve understanding of Hoare logic's capabilities.

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. In addition, we find that, by restricting inputs to $N$, the complexity of the minimal assertion theory for the completeness of Hoare logic to hold can be reduced. This paper further studies the completeness of Hoare Logic relative to $N$ by restricting assertions to subclasses of arithmetical formulas (and by restricting inputs to $N$). Our completeness results refine Cook's result by reducing the complexity of the assertion theory.