pith. machine review for the scientific record. sign in

arxiv: 2605.13944 · v1 · submitted 2026-05-13 · 💻 cs.LO · math.LO

Recognition: 2 theorem links

· Lean Theorem

A foundational characterization of Hoare Logic

Daniel Leivant
Authors on Pith no claims yet

Pith reviewed 2026-05-15 02:40 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords Hoare logicpartial correctnesssecond-order logiccomprehensionprogram verificationiterative programsfoundational characterization
0
0 comments X

The pith

A partial-correctness assertion for an iterative program is provable in Hoare logic if and only if it is provable in second-order logic with first-order comprehension.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves an equivalence between Hoare logic for partial correctness of iterative programs and standard second-order logic restricted to first-order predicates in the comprehension axiom. It corrects two earlier faulty proofs of the same result and presents the equivalence as the first sound foundational characterization of Hoare logic. A sympathetic reader cares because the result pins down exactly what Hoare logic can certify about programs by mapping it onto a familiar, well-studied fragment of higher-order logic.

Core claim

We show that a partial-correctness assertion about an iterative program is provable in Hoare Logic iff it 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.

What carries the argument

The if-and-only-if equivalence between provability in Hoare logic for iterative programs and provability in second-order logic under comprehension restricted to first-order predicates.

If this is right

  • Every Hoare logic derivation for partial correctness translates directly into a second-order proof using only first-order comprehension.
  • Every second-order proof of a first-order property yields a corresponding Hoare logic derivation.
  • Hoare logic is therefore complete for all first-order expressible partial-correctness statements in this logical setting.
  • The result unifies program verification with deduction in a specific fragment of second-order logic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The equivalence suggests that proof complexity results from restricted second-order logic can be transferred to Hoare logic derivations.
  • Extensions of Hoare logic to total correctness or higher-order program properties would likely require lifting the comprehension restriction.
  • Similar characterizations may exist for other verification logics such as dynamic logic when paired with the same restricted comprehension.

Load-bearing premise

The claimed equivalence holds only under the precise syntactic definitions of Hoare logic for iterative programs and the exact restriction of comprehension to first-order predicates.

What would settle it

A concrete partial-correctness assertion about an iterative program that has a proof in Hoare logic but none in the restricted second-order logic, or vice versa, would disprove the equivalence.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript claims to prove that a partial-correctness assertion about an iterative program is provable in Hoare logic if and only if it is provable in standard second-order logic with comprehension restricted to first-order predicates. It notes that this equivalence was previously claimed twice with faulty proofs and presents the current argument as the first correct foundational characterization of Hoare logic.

Significance. If the equivalence holds with the stated syntactic restrictions, the result would supply a precise logical foundation for Hoare logic by equating its deductive strength for partial correctness of while-programs to a specific fragment of second-order logic. This could clarify the relationship between program logics and higher-order systems and support further work in proof theory and verification. The explicit correction of prior faulty proofs is a constructive contribution.

major comments (2)
  1. The abstract asserts the equivalence without derivation steps, counter-example checks, or indication of how the faulty prior proofs were repaired. The central claim therefore lacks visible support; the full proof (presumably in the main theorem section) must supply an explicit inductive argument linking the Hoare rules for iterative programs to the restricted comprehension schema.
  2. The equivalence depends on the precise syntactic definitions of the Hoare logic rules for while-programs and the exact form of the first-order comprehension restriction. The manuscript must state the comprehension axiom explicitly (likely in the preliminary definitions section) and verify that it admits precisely the predicates arising in Hoare assertions; any deviation would invalidate one direction of the iff.
minor comments (1)
  1. The abstract should be expanded to include a one-sentence outline of the proof strategy or key lemmas used to establish both directions of the equivalence.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report on our manuscript. The comments highlight important points about clarity and explicitness that we have addressed in the revision. We respond to each major comment below.

read point-by-point responses

  1. Referee: The abstract asserts the equivalence without derivation steps, counter-example checks, or indication of how the faulty prior proofs were repaired. The central claim therefore lacks visible support; the full proof (presumably in the main theorem section) must supply an explicit inductive argument linking the Hoare rules for iterative programs to the restricted comprehension schema.

    Authors: The abstract is kept concise by design, following standard practice. The full manuscript already contains the complete proof of the equivalence, including an explicit inductive argument that connects the Hoare rules for while-programs to the restricted comprehension schema and explains the repairs to the earlier faulty proofs. To make this support more immediately visible, we have added a short outline of the proof strategy and the key inductive steps in the introduction. revision: yes

  2. Referee: The equivalence depends on the precise syntactic definitions of the Hoare logic rules for while-programs and the exact form of the first-order comprehension restriction. The manuscript must state the comprehension axiom explicitly (likely in the preliminary definitions section) and verify that it admits precisely the predicates arising in Hoare assertions; any deviation would invalidate one direction of the iff.

    Authors: We agree that the precise syntactic form of the restricted comprehension is essential to the result. In the revised version we have added an explicit statement of the first-order comprehension axiom in the preliminaries section. We have also inserted a short lemma confirming that the predicates appearing in Hoare assertions are generated exactly by this restricted schema, thereby securing both directions of the equivalence. revision: yes

Circularity Check

0 steps flagged

No circularity: equivalence proved between independent proof systems via matching syntactic rules

full rationale

The paper derives an if-and-only-if between partial-correctness assertions in Hoare Logic for while-programs and provability in second-order logic with comprehension restricted to first-order predicates. This is established through explicit syntactic definitions of the Hoare rules and the restricted comprehension schema, without any reduction of one system to a fitted parameter or self-referential construction from the other. No load-bearing self-citations or ansatzes are invoked to force the result; the equivalence follows from independent formalizations of the two logics. The derivation remains self-contained against external benchmarks of the respective proof systems.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on the standard axioms of second-order logic together with the explicit restriction of the comprehension axiom to first-order predicates; no free parameters or new entities are introduced in the abstract.

axioms (2)
  • standard math Standard axioms of second-order logic
    The paper invokes the usual axioms for second-order logic as the ambient system.
  • domain assumption Comprehension restricted to first-order predicates
    This restriction is the key modification that makes the equivalence hold.

pith-pipeline@v0.9.0 · 5324 in / 1306 out tokens · 34870 ms · 2026-05-15T02:40:04.722172+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

216 extracted references · 216 canonical work pages

  1. [1]

    Stephen Simpson , title=

    work page

  2. [2]

    Dynamic Logic

    David Harel and Dexter Kozen and Jerzy Tiuryn. Dynamic Logic

    work page

  3. [3]

    Arithmetices principia, novo methodo exposita

    Giuseppe Peano. Arithmetices principia, novo methodo exposita

    work page

  4. [4]

    van Heijenoort

    J. van Heijenoort. From Frege to G \"o del, A Source Book in Mathematical Logic, 1879--1931. 1967

    work page 1931

  5. [5]

    Ramified recurrence and computational complexity I : Word recurrence and poly-time

    Daniel Leivant. Ramified recurrence and computational complexity I : Word recurrence and poly-time. Feasible Mathematics II

    work page

  6. [6]

    A foundational delineation of poly-time

    Daniel Leivant. A foundational delineation of poly-time. Information and Computation

    work page

  7. [7]

    Proving termination assertions in dynamic logics

    Daniel Leivant. Proving termination assertions in dynamic logics. Nineteenth Symposium on Logic in Computer Science. 2004

    work page 2004

  8. [8]

    Reasoning in dynamic logic about program termination

    Daniel Leivant. Reasoning in dynamic logic about program termination. Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot. 2007

    work page 2007

  9. [9]

    D. Leivant. Predicative recurrence in finite type. Logical Foundations of Computer Science (Third International Symposium)

    work page

  10. [10]

    Predicative recursion and computational complexity

    Stephen Bellantoni. Predicative recursion and computational complexity

    work page

  11. [11]

    Friedman

    H. Friedman. Classically and intuitionistically provable recursive functions. Higher Set Theory

    work page

  12. [12]

    Syntactic translations and provably recursive functions

    Daniel Leivant. Syntactic translations and provably recursive functions. Journal of Symbolic Logic

    work page

  13. [13]

    Formalized Recursive Functions and Formalized Realizability

    Stephen C.\ Kleene. Formalized Recursive Functions and Formalized Realizability

    work page

  14. [14]

    On a number-theoretic choice schema and its relation to induction

    Charles Parsons. On a number-theoretic choice schema and its relation to induction. Intuitionism and Proof Theory

    work page

  15. [15]

    Proofs and logical flow graphs

    Alessandra Carbone. Proofs and logical flow graphs

    work page

  16. [16]

    Inductive definitions over finite structures

    Daniel Leivant. Inductive definitions over finite structures. Information and Computation

    work page

  17. [17]

    Une extension de l'interpr \' e tation de G \" o del \` a l'analyse, et son application a l' \' e limination des coupures dans l'analyse et la th \' e orie des types

    Jean-Yves Girard. Une extension de l'interpr \' e tation de G \" o del \` a l'analyse, et son application a l' \' e limination des coupures dans l'analyse et la th \' e orie des types. Proceedings of the Second Scandinavian Logic Symposium. 1971

    work page 1971

  18. [18]

    Bounded Linear Logic: A modular approach to polynomial time computability

    Jean-Yves Girard and Andre Scedrov and Philip Scott. Bounded Linear Logic: A modular approach to polynomial time computability. Theoretical Computer Science

    work page

  19. [19]

    Bounded Arithmetic

    Samuel Buss. Bounded Arithmetic

    work page

  20. [20]

    o del. \

    Kurt G \" o del. \"U ber eine bisher noch nicht benutzte E rweiterung des finiten S tandpunktes. Dialectica

    work page

  21. [21]

    Stephen C. Kleene. Introduction to Metamathematics

    work page

  22. [22]

    Contracting proofs to programs

    Daniel Leivant. Contracting proofs to programs. Logic and Computer Science

    work page

  23. [23]

    Predicative Arithmetic

    Edward Nelson. Predicative Arithmetic

    work page

  24. [24]

    Polynomial computability and recursivity in finite domains

    Vladimir Sazonov. Polynomial computability and recursivity in finite domains. Electronische Informationsverarbeitung und Kybernetik

    work page

  25. [25]

    Algebras of feasible functions

    Yuri Gurevich. Algebras of feasible functions. Twenty Fourth Symposium on Foundations of Computer Science

    work page

  26. [26]

    A note on the expressive power of PROLOG

    Christos Papadimitriou. A note on the expressive power of PROLOG. Bull. EATCS

    work page

  27. [27]

    M. Vardi. Complexity and relational query languages. Fourteenth Symposium on Theory of Computing

    work page

  28. [28]

    Relational queries computable in polynomial time

    Neil Immerman. Relational queries computable in polynomial time. Information and Control

    work page

  29. [29]

    Gurevich and S

    Y. Gurevich and S. Shelah. Fixed-point extensions of first-order logic. Annals of Pure and Applied Logic

    work page

  30. [30]

    Immerman

    N. Immerman. Languages which capture complexity classes. SIAM Journal of Computing

    work page

  31. [31]

    A. Cobham. The intrinsic computational difficulty of functions. Proceedings of the International Conference on Logic, Methodology, and Philosophy of Science

    work page

  32. [32]

    Stratified functional programs and computational complexity

    Daniel Leivant. Stratified functional programs and computational complexity. Conference Record of the Twentieth Annual ACM Symposium on Principles of Programming Languages

    work page

  33. [33]

    Lambda calculus characterizations of poly-time

    Daniel Leivant and Jean-Yves Marion. Lambda calculus characterizations of poly-time. Fundamenta Informaticae

    work page

  34. [34]

    G. Kreisel. La Pr \'e dicativit \'e. Bull. Soc. math. France

    work page

  35. [35]

    G. Kreisel. Mathematical logic. Lectures on Modern Mathematics

    work page

  36. [36]

    D. Leivant. A foundational delineation of computational feasiblity. Proceedings of the Sixth IEEE Conference on Logic in Computer Science (Amsterdam)

    work page

  37. [37]

    Kechris and Y

    A. Kechris and Y. Moschovakis. Recursion in higher types. Handbook of Mathematical Logic. 1977

    work page 1977

  38. [38]

    Descriptive characterizations of computational complexity

    Daniel Leivant. Descriptive characterizations of computational complexity. Second Annual Conference on Structure in Complexity Theory

    work page

  39. [39]

    D. Prawitz. Natural Deduction

    work page

  40. [40]

    Ideas and results in proof theory

    Dag Prawitz. Ideas and results in proof theory. Proceedings of the Second Scandinavian Logic Symposium

    work page

  41. [41]

    o nfinkel. \

    M. Sch \"o nfinkel. \"U ber die B austeine der mathematischen L ogik. Mathematische Annalen

    work page

  42. [42]

    W. A. Howard. The formulae-as-types notion of construction. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism

    work page

  43. [43]

    Semantic characterization of number theories

    Daniel Leivant. Semantic characterization of number theories. Logic from Computer Science

    work page

  44. [44]

    Reasoning about functional programs and complexity classes associated with type disciplines

    Daniel Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. Proceedings of the Twenty Fourth Annual Symposium on the Foundations of Computer Science

    work page

  45. [45]

    A new recursion-theoretic characterization of the poly-time functions

    Stephen Bellantoni and Stephen Cook. A new recursion-theoretic characterization of the poly-time functions. Computational Complexity

    work page

  46. [46]

    Subrecursion and lambda representation over free algebras

    Daniel Leivant. Subrecursion and lambda representation over free algebras. Feasible Mathematics

    work page

  47. [47]

    The Realm of Primitive Recursion

    Harold Simmons. The Realm of Primitive Recursion. Archive for Mathematical Logic

    work page

  48. [48]

    Presburger

    M. Presburger. Ueber die Vollst \"a ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt. Comptes Rendues, Ier Congr \`e des Math \'e matiques des Pays Salves

    work page

  49. [49]

    Free-variable axiomatic foundations of infinitesimal analysis: a fragment with finitary consistency proof

    Roland Chuaqui and Patrick Suppes. Free-variable axiomatic foundations of infinitesimal analysis: a fragment with finitary consistency proof. Journal of Symbolic Logic

    work page

  50. [50]

    K. Lambert. Introduction. Philosophical applications of free logic

    work page

  51. [51]

    Definedness

    Solomon Feferman. Definedness

    work page

  52. [52]

    Foundations of Constructive Mathematics

    Michael Beeson. Foundations of Constructive Mathematics

    work page

  53. [53]

    A. S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. 1973

    work page 1973

  54. [54]

    Troelstra and Dirk van Dalen

    Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics, an Introduction

    work page

  55. [55]

    Existence and description in formal logic

    Dana Scott. Existence and description in formal logic. Bertrand Russell: Philosopher of the Century

    work page

  56. [56]

    Identity and existence in formal logic

    Dana Scott. Identity and existence in formal logic. Applications of sheaves

    work page

  57. [57]

    Kapron and S.A

    B.M. Kapron and S.A. Cook. A new characerization of type-2 feasibility. SIAM Journal of Computing

    work page

  58. [58]

    Cook and Alasdair Urquhart

    Stephen A. Cook and Alasdair Urquhart. Functional interpretations of feasible constructive arithemtic (extended abstract). Proceedings of the 21st ACM Symposium on Theory of Computing

    work page

  59. [59]

    Intrinsic theories and computational complexity

    Daniel Leivant. Intrinsic theories and computational complexity. Logic and Coputational Complexity

    work page

  60. [60]

    Intrinsic reasoning about functional programs I : first order theories

    Daniel Leivant. Intrinsic reasoning about functional programs I : first order theories. Annals of Pure and Applied Logic

    work page

  61. [61]

    Kechris and Y.N

    A.S. Kechris and Y.N. Moschovakis. Recursion in Higher type. Handbook of Mathematical Logic

    work page

  62. [62]

    Kolaitis

    Phokion G. Kolaitis. Canonical forms and hierarchies in generalized recursion theory. Recursion Theory

    work page

  63. [63]

    Type two computational complexity

    Robert Constable. Type two computational complexity. Proceedings of the Fifth ACM Symposium on Theory of Computing

    work page

  64. [64]

    Polynomial and abstract subrecursive classes

    Kurt Melhorn. Polynomial and abstract subrecursive classes. JCSS. 1976

    work page 1976

  65. [65]

    Complexity for type 2 relations

    Michael Towsend. Complexity for type 2 relations. Notre Dame Journal of Formal Logic

    work page

  66. [66]

    Characterizations of the basic feasible functionals of finite type

    Bruce Kapron and Stephen Cook. Characterizations of the basic feasible functionals of finite type. Feasible Mathematics

    work page

  67. [67]

    Some desirable conditions for feasible functionals of type 2

    Anil Seth. Some desirable conditions for feasible functionals of type 2. Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science

    work page

  68. [68]

    Ramified recurrence and computational complexity II: substitutions and poly-space

    Daniel Leivant and Jean-Yves Marion. Ramified recurrence and computational complexity II: substitutions and poly-space. Computer Science Logic

    work page

  69. [69]

    Ramified recurrence and computational complexity IV: Predicative functionals and poly-space

    Daniel Leivant and Jean-Yves Marion. Ramified recurrence and computational complexity IV: Predicative functionals and poly-space. Information and Computation

    work page

  70. [70]

    Bellantoni

    Stephen J. Bellantoni. Characterizing parallel time by type 2 recursions with polynomial output depth. Logic and Coputational Complexity

    work page

  71. [71]

    Type 2 computational complexity

    Robert Constable. Type 2 computational complexity. Fifth Annual ACM Symposium on Theory of Computing

    work page

  72. [72]

    A note on the relation between polynomial time functionals and Constable's class K

    Peter Clote. A note on the relation between polynomial time functionals and Constable's class K. Computer Science Logic

    work page

  73. [73]

    The polynomial hierarchy and intuitionistic bounded arithmetic

    Samuel Buss. The polynomial hierarchy and intuitionistic bounded arithmetic. Structure in Complexity

    work page

  74. [74]

    Cook and Alasdair Urquhart

    Stephen A. Cook and Alasdair Urquhart. Functional interpretations of feasible constructive arithemtic. Annals of Pure and Applied Logic

    work page

  75. [75]

    Computability and complexity of higher type functions

    Stephen Cook. Computability and complexity of higher type functions. Logic from Computer Science

    work page

  76. [76]

    Applicative control and computational complexity

    Daniel Leivant. Applicative control and computational complexity. Computer Science Logic (Proceedings of the Thirteenth CSL Conference)

    work page

  77. [77]

    Kapron and J

    R.\ Irwin and B.M. Kapron and J. Royer. On characterizations of the basic feasible functionals Part I. Journal of Functional Programming

    work page

  78. [78]

    Termination proofs and complexity certification

    Daniel Leivant. Termination proofs and complexity certification. Theoretical aspects of computer software

    work page

  79. [79]

    Calibrating computational feasibility by abstraction rank

    Daniel Leivant. Calibrating computational feasibility by abstraction rank. Seventeenth IEEE Annual Symposium on Logic in Computer Science

    work page

  80. [80]

    Grzegorczyk

    A. Grzegorczyk. Some classes of recursive functions. Rozprawy Mate. IV

    work page

Showing first 80 references.