Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

Makoto Tatsuta; Sohei Ito

arxiv: 2507.00465 · v4 · pith:QVFJIAQCnew · 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-25 08:03 UTC · model grok-4.3

classification 💻 cs.LO

keywords separation logicPeano arithmeticPi-0-1 formulasvalidityundecidabilityintuitionistic points-tostandard model

0 comments

The pith

A Pi-0-1 formula of Peano arithmetic is valid in the standard model exactly when its translation into the minimal separation logic fragment is valid in the standard interpretation.

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

The paper defines a translation that turns Pi-0-1 formulas of Peano arithmetic into formulas built only from the intuitionistic points-to predicate together with the constants 0 and successor. It then proves that the original arithmetic sentence holds in the standard model of the natural numbers if and only if the translated sentence holds under the standard interpretation of the separation logic. The same equivalence immediately yields undecidability of validity for the fragment. Because Pi-0-1 sentences can express consistency of formal systems and non-termination of computations, those properties become expressible inside the fragment as well.

Core claim

The paper establishes a translation from Pi-0-1 formulas in Peano arithmetic to formulas in the fragment of separation logic consisting of intuitionistic points-to, 0, and successor, such that a formula holds in the standard model of arithmetic if and only if its image holds in the standard interpretation of the logic.

What carries the argument

The translation function that maps Pi-0-1 formulas to separation logic formulas using only intuitionistic points-to, 0, and successor, preserving validity in standard models.

If this is right

Validity for the fragment is undecidable.
Consistency statements of logical systems can be expressed inside the fragment.
Non-termination of computations can be expressed inside the fragment.
Any Pi-0-1 property of the natural numbers becomes a property of the fragment.

Where Pith is reading between the lines

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

The result supplies a lower bound on the complexity of any decision procedure that might be attempted for slightly larger fragments of separation logic with numbers.
One could test whether the equivalence survives when the points-to predicate is replaced by a classical version or when additional arithmetic primitives are added.
The encoding may be used to transfer known Pi-0-1 independence results from arithmetic into statements about heap-manipulating programs.

Load-bearing premise

The chosen translation from Pi-0-1 formulas to the fragment is defined so that it preserves truth exactly in the standard models of both systems.

What would settle it

Exhibit one concrete Pi-0-1 sentence that is true in the natural numbers yet whose image under the translation fails in the standard interpretation of the separation logic, or vice versa.

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.

Desk Editor's Note private letter to a colleague

The paper reduces Π₀₁ validity from Peano arithmetic to a minimal separation logic fragment using only intuitionistic points-to, 0 and successor, yielding undecidability.

read the letter

The main result is a translation of Π₀₁ formulas from Peano arithmetic into formulas built from intuitionistic points-to, zero and successor alone, with a proof that validity in the standard model is preserved exactly in both directions. The corollary is undecidability of validity for that fragment. The construction is new in its choice of exactly this minimal signature; earlier work on separation logic with numbers has not pinned undecidability down to this level of restriction. The paper does well by staying inside the standard interpretation and by noting that the same fragment can therefore express consistency statements and non-termination. That keeps the claim sharp for the subfield. The soft spots are limited. The abstract gives no definition of the translation or sketch of the equivalence proof, so the body must supply the details on how quantifiers and arithmetic are encoded without extra structure. If those steps are fully spelled out and the models line up, the argument is fine; nothing in the stated claim suggests circularity or hidden parameters. This is for people who track decidability borders in separation logics that include numbers. A reader already working on complexity results for verification logics will find the minimal-fragment construction useful for comparison. It deserves a serious referee because the reduction is concrete and the target fragment is small enough that the details can be checked without excessive effort.

Referee Report

0 major / 2 minor

Summary. The paper defines a translation from Π₀₁ formulas of Peano arithmetic into formulas of a minimal fragment of separation logic consisting only of the intuitionistic points-to predicate, the constant 0, and the successor function. It proves that a Π₀₁ formula is valid in the standard model of PA if and only if its image under the translation is valid in the standard interpretation of the SL fragment, and obtains undecidability of validity in the fragment as a corollary.

Significance. If the translation and equivalence hold, the result shows that properties expressible in Π₀₁ (consistency statements, non-termination) remain expressible and undecidable already in this minimal SL fragment. The reduction is parameter-free and directly transfers known undecidability from PA, which is a standard and useful technique in the field.

minor comments (2)

[Abstract] The abstract states the main theorem but does not sketch the translation clauses; a one-sentence outline in the abstract would improve readability without lengthening the paper.
The manuscript should explicitly state the precise signature and the standard interpretation used for the SL fragment (e.g., how heaps and the successor are interpreted over the naturals).

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our contribution and for recommending minor revision. No specific major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity in the derivation

full rationale

The paper defines an explicit translation from Π₀₁ formulas of Peano arithmetic into the minimal separation logic fragment (intuitionistic points-to, 0, successor) and proves the equivalence of validity in the respective standard models. This is a standard encoding plus reduction proof; the preservation property is not assumed by definition but is the content of the claimed theorem. No self-citations, fitted parameters, ansatzes, or renamings appear as load-bearing steps in the abstract or stated claims. The derivation is self-contained and does not reduce to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract provides no information on free parameters, axioms, or invented entities; the work is described as a translation and equivalence proof without additional postulates.

pith-pipeline@v0.9.0 · 5705 in / 1080 out tokens · 76420 ms · 2026-05-25T08:03:51.220755+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Lean theorems connected to this paper

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

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean equivNat, toNat_add, toNat_mul, embed_injective unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

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

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

Finite Model Theory

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

work page 1995
[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]

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]

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]

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]

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]

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]

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]

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

work page 2019
[19]

Shoenfield

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

work page 1967
[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]

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]

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

[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