A foundational characterization of Hoare Logic
Logic in Computer Science
2026-05-15 v1 Logic
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.
Cite
@article{arxiv.2605.13944,
title = {A foundational characterization of Hoare Logic},
author = {Daniel Leivant},
journal= {arXiv preprint arXiv:2605.13944},
year = {2026}
}