pith. sign in

arxiv: 2607.01970 · v1 · pith:F5OVI6UKnew · submitted 2026-07-02 · 🧮 math.LO

Bisimulations in second-order arithmetic

Yuto Takeda , Keita Yokoyama This is my paper

Pith reviewed 2026-07-03 03:07 UTC · model grok-4.3

classification 🧮 math.LO
keywords Hennessy-Milner theoremvan Benthem characterization theoremACA0RCA0second-order arithmeticmodal logicbisimulationreverse mathematics
0
0 comments X

The pith

The Hennessy-Milner theorem is equivalent to ACA₀ over RCA₀.

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

This paper formalizes two theorems from modal propositional logic inside subsystems of second-order arithmetic. It establishes that the Hennessy-Milner theorem, which equates bisimilarity of states with satisfaction of the same modal formulas, is equivalent to the axiom of arithmetical comprehension ACA₀ when added to the base system RCA₀. The paper also treats three variants of the van Benthem characterization theorem and shows that their strengths differ: the semantic version is provable already in RCA₀, the syntactic version in primitive recursive arithmetic, and the hybrid version matches the weak completeness theorem for first-order logic over RCA₀. A sympathetic reader cares because the results locate precisely how much arithmetic comprehension is required to prove these modal equivalences inside a weak base theory.

Core claim

The paper demonstrates that the Hennessy-Milner theorem is equivalent to ACA₀ over RCA₀. For the van Benthem characterization theorem, the semantic form is provable in RCA₀, the syntactic form is provable in PRA, and the hybrid form is equivalent to the weak completeness theorem for first-order logic over RCA₀.

What carries the argument

The formalizations of the Hennessy-Milner theorem and the three variants of the van Benthem characterization theorem inside second-order arithmetic that preserve the essential content of the original modal logic statements.

Load-bearing premise

The formalizations of the Hennessy-Milner theorem and the three variants of the van Benthem characterization theorem inside second-order arithmetic preserve the essential content of the original modal logic statements.

What would settle it

A model of RCA₀ in which the formalized Hennessy-Milner theorem holds but ACA₀ fails would falsify the claimed equivalence.

read the original abstract

This paper investigates the logical strength of two theorems in modal propositional logic - the Hennessy-Milner theorem and the van Benthem characterization theorem - within the framework of second-order arithmetic. We demonstrate that the Hennessy-Milner theorem is equivalent to $\mathrm{ACA}_0$ over $\mathrm{RCA}_0$. For the van Benthem characterization theorem, we introduce three variants: the semantic, syntactic, and hybrid forms. We show that the semantic form is provable in $\mathrm{RCA}_0$, the syntactic form is provable in $\mathrm{PRA}$, and the hybrid form is equivalent to the weak completeness theorem for first-order logic over $\mathrm{RCA}_0$.

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 / 2 minor

Summary. The manuscript calibrates the logical strength of the Hennessy-Milner theorem (bisimulation equivalence coincides with modal equivalence under image-finiteness) and three variants of the van Benthem characterization theorem inside subsystems of second-order arithmetic. It claims that the Hennessy-Milner theorem is equivalent to ACA₀ over RCA₀; the semantic van Benthem variant is provable in RCA₀, the syntactic variant in PRA, and the hybrid variant equivalent to the weak completeness theorem for first-order logic over RCA₀.

Significance. If the formalizations faithfully capture the original modal statements, the results supply exact reverse-mathematical calibrations for two central theorems of modal logic. The separation into semantic, syntactic, and hybrid forms of van Benthem’s theorem, together with the use of standard base theories RCA₀ and PRA, is a clear strength and yields falsifiable predictions about which subsystems suffice for each statement.

major comments (2)
  1. [§3] §3 (formalization of Hennessy-Milner): the paper must verify that the encoding of image-finiteness inside RCA₀ does not inadvertently strengthen the antecedent; if the formalized image-finiteness condition is strictly weaker than the classical one, the claimed equivalence to ACA₀ would not transfer to the original theorem.
  2. [§4.2] §4.2 (hybrid van Benthem): the reduction to weak completeness for first-order logic is stated as an equivalence over RCA₀, but the direction from weak completeness to the hybrid statement appears to rely on an unstated coding of modal formulas as first-order sentences; the precise translation must be exhibited to confirm the equivalence is not one-directional.
minor comments (2)
  1. [§4] Notation for the three van Benthem variants is introduced only in the abstract and should be repeated with explicit labels at the beginning of §4.
  2. The statement of the syntactic variant in PRA would benefit from an explicit reference to the induction schema used, since PRA is mentioned without further qualification.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report. The comments highlight important points about the faithfulness of our formalizations, which we address below.

read point-by-point responses

  1. Referee: [§3] §3 (formalization of Hennessy-Milner): the paper must verify that the encoding of image-finiteness inside RCA₀ does not inadvertently strengthen the antecedent; if the formalized image-finiteness condition is strictly weaker than the classical one, the claimed equivalence to ACA₀ would not transfer to the original theorem.

    Authors: The formalization in §3 encodes image-finiteness via the existence of a function enumerating the finitely many successors of each world, which is expressible in RCA₀ and coincides with the classical notion on countable structures (the setting in which the Hennessy-Milner theorem is stated). We will add a short paragraph after the definition of image-finiteness clarifying this equivalence and confirming that the antecedent is not strengthened. revision: yes

  2. Referee: [§4.2] §4.2 (hybrid van Benthem): the reduction to weak completeness for first-order logic is stated as an equivalence over RCA₀, but the direction from weak completeness to the hybrid statement appears to rely on an unstated coding of modal formulas as first-order sentences; the precise translation must be exhibited to confirm the equivalence is not one-directional.

    Authors: We agree that the standard translation from modal formulas to first-order sentences (mapping □ to universal quantification over the accessibility relation) should be written out explicitly. This translation is used in both directions of the equivalence with weak FOL completeness. We will insert the precise inductive definition of the translation in the revised §4.2. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper establishes proof-theoretic equivalences between formalized modal logic theorems (Hennessy-Milner and van Benthem variants) and standard subsystems of second-order arithmetic (ACA₀, RCA₀, PRA) via explicit formalizations and bidirectional implications. These are standard reverse-mathematics arguments that construct models or reductions to show necessity and verify sufficiency inside the base theory plus the target axiom; the formal statements are defined independently of the target strength results, with no parameter fitting, self-definitional renaming, or load-bearing self-citation chains that collapse the claimed equivalences back to their inputs by construction. The derivation chain is therefore self-contained against external benchmarks of second-order arithmetic.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The paper relies entirely on standard, previously defined subsystems of second-order arithmetic (RCA0, ACA0, PRA) and the weak completeness theorem for first-order logic; no free parameters, ad-hoc axioms, or invented entities are introduced.

axioms (3)
  • standard math RCA0 is the base theory of recursive comprehension
    Standard base system invoked for all equivalences and provability results.
  • standard math ACA0 is the system with arithmetic comprehension axiom
    Standard axiom system used for the Hennessy-Milner equivalence.
  • standard math PRA is primitive recursive arithmetic
    Standard weak system used for the syntactic van Benthem variant.

pith-pipeline@v0.9.1-grok · 5634 in / 1362 out tokens · 31241 ms · 2026-07-03T03:07:57.669023+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

15 extracted references

  1. [1]

    Cambridge University Press, Cambridge, 2001

    Patrick Blackburn, Maarten de Rijke, and Yde Venema.Modal logic, volume 53 ofCambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2001

    2001

  2. [2]

    Ehrenfeucht

    A. Ehrenfeucht. An application of games to the completeness problem for formalized theories.Fund. Math., 49:129–141, 1960/61

    1960

  3. [3]

    Sur quelques classifications des systèmes de relations.Publ

    Roland Fraïssé. Sur quelques classifications des systèmes de relations.Publ. Sci. Univ. Alger. Sér. A, 1:35–182, 1954

    1954

  4. [4]

    Perspectives in Mathe- matical Logic

    Petr Hájek and Pavel Pudlák.Metamathematics of first-order arithmetic. Perspectives in Mathe- matical Logic. Springer-Verlag, Berlin, 1993

    1993

  5. [5]

    Algebraic laws for nondeterminism and concurrency.J

    Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency.J. Assoc. Comput. Mach., 32(1):137–161, 1985

    1985

  6. [6]

    J. A. Makowsky. Algorithmic uses of the Feferman-Vaught theorem. volume 126, pages 159–213

  7. [7]

    Provinces of logic determined

  8. [8]

    Elementary proof of the van Benthem-Rosen characterisation theorem

    Martin Otto. Elementary proof of the van Benthem-Rosen characterisation theorem. Technical Report 2342, Department of Mathematics, Technische Universität Darmstadt, 2004

    2004

  9. [9]

    Bisimulation invariance and finite models

    Martin Otto. Bisimulation invariance and finite models. InLogic Colloquium ’02, volume 27 ofLect. Notes Log., pages 276–298. Assoc. Symbol. Logic, La Jolla, CA, 2006

    2006

  10. [10]

    Modal logic over finite structures.J

    Eric Rosen. Modal logic over finite structures.J. Logic Lang. Inform., 6(4):427–439, 1997

    1997

  11. [11]

    Completeness theorems for modal logic in second-order arithmetic

    Sho Shimomichi, Yuto Takeda, and Keita Yokoyama. Completeness theorems for modal logic in second-order arithmetic. In Arnold Beckmann, Isabel Oitavem, and Florin Manea, editors,Cross- roads of Computability and Logic: Insights, Inspirations, and Innovations, pages 452–466, Cham,

  12. [12]

    Springer Nature Switzerland

  13. [13]

    Simpson.Subsystems of second order arithmetic

    Stephen G. Simpson.Subsystems of second order arithmetic. Perspectives in Logic. Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, second edition, 2009

    2009

  14. [14]

    PhD thesis, University of Amsterdam, 1976

    Johan Van Benthem.Modal correspondence theory. PhD thesis, University of Amsterdam, 1976

    1976

  15. [15]

    Reverse mathematics and completeness theorems for intuitionistic logic.Notre Dame J

    Takeshi Yamazaki. Reverse mathematics and completeness theorems for intuitionistic logic.Notre Dame J. Formal Logic, 42(3):143–148, 2001. 24

    2001