pith. sign in

arxiv: 2507.00465 · v3 · submitted 2025-07-01 · 💻 cs.LO

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

Sohei Ito , Makoto Tatsuta This is my paper

Pith reviewed 2026-05-19 07:12 UTC · model grok-4.3

classification 💻 cs.LO
keywords separation logicPeano arithmeticPi-0-1 formulasvalidityundecidabilitypoints-to predicate
0
0 comments X

The pith

Pi-0-1 formulas of Peano arithmetic are valid in the standard model exactly when their translations are valid in this minimal separation logic fragment.

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

The paper constructs a translation that turns Pi-0-1 formulas of Peano arithmetic into formulas built only from the intuitionistic points-to predicate, the constant 0, and the successor function. It then proves that a formula holds in the standard model of arithmetic if and only if the translated formula holds under the standard heap interpretation of the logic. The equivalence immediately yields undecidability of validity for the fragment. Because Pi-0-1 sentences can express consistency of formal systems and non-termination of programs, the result shows that these properties can be expressed and reasoned about inside the same tiny fragment.

Core claim

The central result is an exact equivalence between validity of Pi-0-1 sentences in the standard model of arithmetic and validity of their images in the standard interpretation of the separation logic fragment that contains only intuitionistic points-to, zero, and successor. The paper supplies an explicit translation and proves the two directions of the equivalence, from which undecidability of validity in the fragment follows as a corollary.

What carries the argument

The translation that maps each Pi-0-1 formula of Peano arithmetic to a formula using only the intuitionistic points-to predicate together with 0 and successor, preserving validity exactly under the standard models.

Load-bearing premise

The translation preserves validity exactly when the arithmetic side uses the standard model and the separation-logic side uses the standard heap interpretation.

What would settle it

Exhibit one concrete Pi-0-1 sentence that is true in the natural numbers yet whose translated formula fails to hold in the standard heap model, or a sentence that is false in the naturals yet whose translation holds in the heap model.

read the original abstract

Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software where numbers are important. However, properties of the validity such as decidability and complexity for separation logic with numbers have not been fully studied yet. This paper presents the translation of Pi-0-1 formulas in Peano arithmetic to formulas in a small fragment of separation logic with numbers, which consists only of the intuitionistic points-to predicate, 0 and the successor function. Then this paper proves that a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation. As a corollary, this paper also gives a perspective proof for the undecidability of the validity in this fragment. Since Pi-0-1 formulas can describe consistency of logical systems and non-termination of computations, this result also shows that these properties discussed in Peano arithmetic can also be discussed in such a small fragment of separation logic with numbers.

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 paper presents a translation from Π₀₁ formulas of Peano arithmetic into a minimal fragment of separation logic consisting solely of the intuitionistic points-to predicate, the constant 0, and the successor function. It claims to prove that a PA formula is valid in the standard model of arithmetic if and only if its translation is valid under the standard interpretation of this SL fragment, and derives undecidability of validity in the fragment as a corollary. The result is positioned as showing that properties such as consistency and non-termination expressible in Π₀₁ arithmetic can be discussed in this restricted logic.

Significance. If the equivalence holds, the result would establish that a very small fragment of separation logic with numbers is already expressive enough to capture key Π₀₁ properties, providing a new perspective on the boundary between decidable and undecidable fragments of SL. The corollary on undecidability is a direct consequence of the reduction and would be a notable contribution if the translation is shown to be validity-preserving in both directions.

major comments (2)
  1. The manuscript does not provide an explicit definition of the 'standard interpretation' for the SL fragment (mentioned in the abstract and the equivalence claim). In particular, it is unclear whether validity of a translated formula means satisfaction under a specific heap that encodes the natural numbers via points-to and successor, or under all heaps in the standard model; without this, the 'only if' direction of the claimed equivalence N ⊨ φ ⇔ M ⊨ φ' cannot be verified and may fail due to additional heaps satisfying φ' independently of the arithmetic content of φ.
  2. The translation from Π₀₁ formulas to the SL fragment is asserted to preserve validity exactly, but the manuscript supplies no derivation steps, inductive definition of the translation, or model details (as noted in the abstract's summary of the result). This is load-bearing for the central claim; a concrete construction showing how, e.g., universal quantifiers and arithmetic predicates are encoded using only intuitionistic points-to, 0, and successor is required to assess whether monotonicity conditions in the intuitionistic semantics interfere with classical PA validity.
minor comments (1)
  1. The abstract would be clearer if it briefly indicated the syntax of the target fragment and the precise class of formulas (Π₀₁) being translated.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We address each major comment below.

read point-by-point responses

  1. Referee: The manuscript does not provide an explicit definition of the 'standard interpretation' for the SL fragment (mentioned in the abstract and the equivalence claim). In particular, it is unclear whether validity of a translated formula means satisfaction under a specific heap that encodes the natural numbers via points-to and successor, or under all heaps in the standard model; without this, the 'only if' direction of the claimed equivalence N ⊨ φ ⇔ M ⊨ φ' cannot be verified and may fail due to additional heaps satisfying φ' independently of the arithmetic content of φ.

    Authors: We agree that the definition of the standard interpretation should be stated more explicitly for clarity. The manuscript defines the standard model M for the SL fragment as having domain the natural numbers, with 0 and successor interpreted standardly, and heaps encoding the arithmetic via the points-to predicate (intuitionistic). Validity of the translated formula means it holds in all heaps that faithfully represent this model. The 'only if' direction follows from the inductive construction of the translation, which ensures that non-encoding heaps do not satisfy the formula when the original PA formula is valid. We will add an explicit formal definition of this interpretation, including the precise notion of 'faithful encoding heaps', in a revised Section 2. revision: yes

  2. Referee: The translation from Π₀₁ formulas to the SL fragment is asserted to preserve validity exactly, but the manuscript supplies no derivation steps, inductive definition of the translation, or model details (as noted in the abstract's summary of the result). This is load-bearing for the central claim; a concrete construction showing how, e.g., universal quantifiers and arithmetic predicates are encoded using only intuitionistic points-to, 0, and successor is required to assess whether monotonicity conditions in the intuitionistic semantics interfere with classical PA validity.

    Authors: The manuscript does contain an inductive definition of the translation (in Section 3) together with a proof by induction on formula structure establishing the equivalence. Atomic arithmetic predicates are encoded directly via points-to chains using 0 and successor; quantifiers are handled by ranging over the encoded domain in the heap. The intuitionistic semantics does not interfere with classical validity on the standard model because the translation restricts attention to heaps that are monotonic extensions only within the arithmetic encoding, preserving the classical truth values. To strengthen the presentation, we will expand the inductive definition with explicit clauses for each connective and quantifier, include a short proof sketch of the key lemmas, and add a remark addressing the monotonicity concern. revision: yes

Circularity Check

0 steps flagged

No circularity: standard reduction from undecidable PA validity to SL fragment

full rationale

The paper defines an explicit translation from Π₀₁ formulas of Peano arithmetic into formulas of the minimal separation-logic fragment (intuitionistic points-to, 0, successor) and proves the biconditional validity preservation under the standard model and standard interpretation. This is a conventional encoding argument whose central claim is the theorem itself, not a quantity fitted or renamed inside the paper. No self-citation is load-bearing for the equivalence, no ansatz is smuggled, and the result does not reduce by construction to its own inputs; it is independently falsifiable against the known undecidability of PA. The derivation is therefore self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the standard semantics of Peano arithmetic and of separation logic; no free parameters or invented entities are introduced.

axioms (2)
  • domain assumption Validity of Pi-0-1 formulas is assessed in the standard model of natural numbers
    The paper defines validity of the source formulas with respect to the usual arithmetic model.
  • domain assumption Validity of the translated formulas is assessed in the standard heap interpretation of separation logic
    The target logic uses the conventional points-to semantics over heaps.

pith-pipeline@v0.9.0 · 5705 in / 1389 out tokens · 39902 ms · 2026-05-19T07:12:37.248835+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

22 extracted references · 22 canonical work pages

  1. [1]

    Kanovich, and Jo¨ el Ouaknine

    Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, and Jo¨ el Ouaknine. Foundations for decision problems in sep- aration logic with general inductive predicates. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th Inter- national Conference, FOSSACS 2014, Held as Part of the European Joint Con...

    work page 2014

  2. [2]

    Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. A decidable fragment of separation logic. In Kamal Lodaya and Meena Mahajan, edi- tors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, Decem- ber 16-18, 2004, Proceedings , volume 3328 of Lecture Notes in Computer Scien...

    work page 2004

  3. [3]

    Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. Symbolic ex- ecution with separation logic. In Kwangkeun Yi, editor, Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings , volume 3780 of Lecture Notes in Computer Science, pages 52–68. Springer, 2005

    work page 2005

  4. [4]

    On the almighty wand

    R´ emi Brochenin, St´ ephane Demri, and´Etienne Lozes. On the almighty wand. Inf. Comput., 211:106–137, 2012

    work page 2012

  5. [5]

    A decision procedure for satisfiability in separation logic with inductive predicates

    James Brotherston, Carsten Fuhs, Juan Antonio Navarro P´ erez, and Nikos Gorogiannis. A decision procedure for satisfiability in separation logic with inductive predicates. In Thomas A. Henzinger and Dale Miller, editors, 29 Joint Meeting of the Twenty-Third EACSL Annual Conference on Com- puter Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Sym...

    work page 2014

  6. [6]

    O’Hearn, and Hongseok Yang

    Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. J. ACM, 58(6):26:1–26:66, 2011

    work page 2011

  7. [7]

    From sepa- ration logic to first-order logic

    Cristiano Calcagno, Philippa Gardner, and Matthew Hague. From sepa- ration logic to first-order logic. In Vladimiro Sassone, editor, Foundations of Software Science and Computational Structures, 8th International Con- ference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April ...

    work page 2005

  8. [8]

    Cristiano Calcagno, Hongseok Yang, and Peter W. O’Hearn. Computability and complexity results for a spatial assertion language for data structures. In The Second Asian Workshop on Programming Languages and Systems, APLAS’01, Korea Advanced Institute of Science and Technology, Daejeon, Korea, December 17-18, 2001, Proceedings , pages 289–300, 2001

    work page 2001

  9. [9]

    Parkinson, and James Worrell

    Byron Cook, Christoph Haase, Jo¨ el Ouaknine, Matthew J. Parkinson, and James Worrell. Tractable reasoning in a fragment of separation logic. In Joost-Pieter Katoen and Barbara K¨ onig, editors, CONCUR 2011 - Con- currency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes i...

    work page 2011

  10. [10]

    Finite Model Theory

    Heinz-Dieter Ebbinghaus and J¨ org Flum. Finite Model Theory . Springer- Verlag, 1995

    work page 1995

  11. [11]

    An undecidability result for separa- tion logic with theory reasoning

    Mnacho Echenim and Nicolas Peltier. An undecidability result for separa- tion logic with theory reasoning. Inf. Process. Lett. , 182:106359, 2023

    work page 2023

  12. [12]

    The tree width of sep- aration logic with recursive definitions

    Radu Iosif, Adam Rogalewicz, and Jir´ ı Sim´ acek. The tree width of sep- aration logic with recursive definitions. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Au- tomated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings , volume 7898 of Lecture Notes in Computer Science, pages 21–38. Spri...

    work page 2013

  13. [13]

    Representation of peano arithmetic in sepa- ration logic

    Sohei Ito and Makoto Tatsuta. Representation of peano arithmetic in sepa- ration logic. In Jakob Rehof, editor,9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, volume 299 of LIPIcs, pages 18:1–18:17. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2024

    work page 2024

  14. [14]

    Beyond symbolic heaps: Deciding sep- aration logic with inductive definitions

    Jens Katelaan and Florian Zuleger. Beyond symbolic heaps: Deciding sep- aration logic with inductive definitions. In Elvira Albert and Laura Kov´ acs, editors, LPAR 2020: 23rd International Conference on Logic for Program- ming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing , pages 390–408. ...

    work page 2020

  15. [15]

    Decidability for entailments of sym- bolic heaps with arrays

    Daisuke Kimura and Makoto Tatsuta. Decidability for entailments of sym- bolic heaps with arrays. Log. Methods Comput. Sci. , 17(2), 2021. 30

    work page 2021

  16. [16]

    A decid- able fragment in separation logic with inductive predicates and arithmetic

    Quang Loc Le, Makoto Tatsuta, Jun Sun, and Wei-Ngan Chin. A decid- able fragment in separation logic with inductive predicates and arithmetic. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verifi- cation - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II , volume 10427 of Lecture Notes in ...

    work page 2017

  17. [17]

    Spatial factorization in cyclic-proof system for separation logic

    Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yama- mura. Spatial factorization in cyclic-proof system for separation logic. Computer Software, 37(1):1 125–1 144, 2020

    work page 2020

  18. [18]

    Peter W. O’Hearn. Separation logic. Commun. ACM, 62(2):86–95, 2019

    work page 2019

  19. [19]

    Shoenfield

    Joseph R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967

    work page 1967

  20. [20]

    Separation logic with monadic in- ductive definitions and implicit existentials

    Makoto Tatsuta and Daisuke Kimura. Separation logic with monadic in- ductive definitions and implicit existentials. In Xinyu Feng and Sungwoo Park, editors, Programming Languages and Systems - 13th Asian Sym- posium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings , volume 9458 of Lecture Notes in Computer Science , pages 69–8...

    work page 2015

  21. [21]

    Decision procedure for separation logic with inductive definitions and presburger arithmetic

    Makoto Tatsuta, Quang Loc Le, and Wei-Ngan Chin. Decision procedure for separation logic with inductive definitions and presburger arithmetic. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science , pages 423–443, 2016

    work page 2016

  22. [22]

    Completeness of cyclic proofs for symbolic heaps with inductive definitions

    Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with inductive definitions. In Anthony Wid- jaja Lin, editor, Programming Languages and Systems - 17th Asian Sym- posium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, volume 11893 of Lecture Notes in Computer Science , pages 367–3...

    work page 2019