A foundational characterization of Hoare Logic

TL;DR

This paper establishes a foundational equivalence between provability in Hoare Logic for partial correctness assertions and provability in a specific form of second-order logic, providing a new theoretical understanding.

Contribution

It provides the first rigorous foundational characterization of Hoare Logic by linking it to second-order logic with restricted comprehension.

Findings

Proves the equivalence between Hoare Logic and a fragment of second-order logic.

Addresses and corrects previous faulty claims of this equivalence.

Establishes a formal basis for understanding Hoare Logic's foundations.

Abstract

We show that a partial-correctness assertion about an iterative program is provable in Hoare Logic iffit is provable in standard second-order logic with comprehension restricted to first-order predicates. This equivalence was claimed twice in the past, both with faulty proofs, and seems to be the first foundational characterization of Hoare Logic.