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.

翻译：我们证明，关于迭代程序的部分正确性断言在霍尔逻辑中可证当且仅当它在标准二阶逻辑（其中概括规则限制于一阶谓词）中可证。这一等价关系在过去曾被两次提出，但均伴有错误的证明，且似乎是对霍尔逻辑的首个基础性特征刻画。