{"id":"arxiv/2605.13944","url":"https://arxiv.org/abs/2605.13944","tags":["cs.LO","math.LO"],"score":0,"title":"A foundational characterization of Hoare Logic","domain":"cs.LO","source":"arxiv","authors":["Daniel Leivant"],"reviews":0,"subject":"cs.LO","summary":"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.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-05-13","reactions":{}}