Pith. sign in

REVIEW 2 major objections 5 minor 33 references

When Bi-interpretability implies Synonymy

T0 review · 2 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Two sequential theories that are bi-interpretable via one-dimensional, identity-preserving interpretations are synonymous.

desk verdict Main theorem is sound; the optimality example has a fixable gap in the automorphism claim, and the paper deserves review. read the letter →

arxiv 2506.01028 v1 pith:GGC2TLLA submitted 2025-06-01 math.LO

Harvey M. Friedman , Albert Visser This is my paper
classification math.LO MSC 03A0503B3003F25
keywords InterpretationsInterpretabilitySchröder-BernsteinTheoremSynonymyDefinitionalequivalenceBi-interpretabilitySequentialtheoriesConceptual
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper asks when the loose notion of bi-interpretability—two theories that can uniformly build internal models of each other up to definable isomorphism—forces the strictest reasonable notion of sameness, synonymy, also called definitional equivalence. It proves that for sequential theories, which have enough coding to manipulate finite sequences, bi-interpretability via one-dimensional, identity-preserving interpretations implies synonymy. The proof's engine is a version of the Schröder-Bernstein theorem that works under very weak set-theoretic assumptions, formalized in a tiny class theory. A worked example shows the result is optimal: two finitely axiomatized sequential theories are bi-interpretable but not synonymous when one of the two witnessing interpretations is allowed to twist the identity relation. A reader should care because synonymy preserves finer model-theoretic structure than bi-interpretability, and the paper gives a precise criterion for when the two collapse.

What carries the argument

The weak Schröder-Bernstein theorem (Theorem 4.1) is proved inside the theory SB, which is adjunctive class theory extended with two equivalence relations A/EA and B/EB and two injections F and G between the quotient virtual classes. The proof constructs, by a uniform formula H, a definable bijection between A/EA and B/EB using 'x-switch' pairs, which are downward-closed pairs of virtual classes satisfying a small closure condition. Lifted to any conceptual theory via Corollary 4.1, this machinery lets the paper replace an arbitrary identity-preserving interpretation K with a direct interpretation K′ by finding a definable bijection between the whole domain and the virtual subclass δ_K, while preserving the bi-interpretation. The name 'Schröder-Bernstein' is inherited from the classical set-theoretic theorem that two sets with injections in both directions are equinumerous; here the same idea is made to work with virtual classes definable in a very weak theory.

What would settle it

Find two conceptual (or sequential) theories U and V that are bi-interpretable through one-dimensional, identity-preserving interpretations but are not synonymous; Theorem 5.3 says no such pair exists. A more local target is Corollary 4.1: exhibit a conceptual theory T and definable equivalence relations and injections satisfying its hypotheses for which no definable bijection H between the quotients is provable in T.

Watch

Extended reading notes

Core claim

The central result is Theorem 5.3: if V is a conceptual theory, meaning it can interpret a very weak two-sorted class theory called adjunctive class theory, and K : U → V and M : V → U form a bi-interpretation with both interpretations one-dimensional and identity-preserving, then U and V are synonymous. This covers sequential theories, which include ordinary arithmetic and set theories. The proof takes the definable isomorphism F between the full domain of V and the virtual subclass δ_{K∘M}, uses the weak Schröder-Bernstein theorem to obtain a definable bijection G between the full domain and the virtual domain δ_K, and then reshapes K into a direct interpretation K′ that is definably isomorphic to K. Since K′ is direct, an earlier retract argument (Corollary 5.1) yields full synonymy. The accompanying example of AS and ACF♭ shows that dropping identity preservation for either witness can break the conclusion even for finitely axiomatized sequential theories.

Load-bearing premise

The argument depends on the claim that the Schröder-Bernstein construction can be carried out inside any theory that can encode the very weak 'adjunctive class theory' of objects and classes; if some such theory fails to internalize that construction, the main theorem loses its proof.

Editorial extensions

If this is right

  • If the theorem is right, then any pair of sequential theories whose mutual interpretations are one-dimensional and identity-preserving are not merely bi-interpretable but have a common definitional extension.
  • Known bi-interpretations upgrade to synonymies: PA− and the theory of discretely ordered commutative rings become synonymous, as do Th(N) and Th(Q).
  • The same upgrade applies to the Ackermann and von Neumann bi-interpretation between ZF_fin^+ and PA, and to a version of ZF with a countable set of urelements and ordinary ZF.
  • The AS / ACF♭ example shows the boundary is sharp: a single non-identity-preserving witness can destroy synonymy, even when both theories are finitely axiomatized and sequential.
  • Because every interpretation into a sequential theory can be replaced by a one-dimensional one up to i-isomorphism, the essential hypothesis in the sequential case is identity preservation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper, the weak Schröder-Bernstein construction may serve as a general definable-cardinality tool inside weak theories: any two definable virtual classes with mutual definable injections would get a definable bijection, independent of the synonymy application.
  • A natural open question suggested by the proof is whether identity preservation can be relaxed to allow definable twists that cancel, or whether the AS / ACF♭ example is the first case of a general dichotomy in which failure of identity preservation always blocks synonymy.
  • The automorphism-action argument used to separate AS from ACF♭ suggests a cheap test for non-synonymy in any bi-interpretable pair: if automorphisms act on elements of the two internal models with different orbit patterns, the theories are not synonymous even if bi-interpretable.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper proves that bi-interpretability between two conceptual theories via one-dimensional, identity-preserving interpretations implies synonymy (definitional equivalence). The main theorem, Theorem 5.3, is proved through a weak Schröder-Bernstein theorem, Theorem 4.1, established in the weak adjunctive class theory SB and then transferred to conceptual theories via Corollary 4.1. The paper also constructs an optimality example: two finitely axiomatized sequential theories, AS and ACF♭, claimed to be bi-interpretable but not synonymous, with exactly one of the witnessing interpretations failing to be identity-preserving. Applications in Section 6 include synonymy for PA− and DOCR, Th(N) and Th(Q), and ZF+fin and PA.

Significance. The main theorem is a clean and useful result that identifies a natural sufficient condition for synonymy, and the weak Schröder-Bernstein theorem is of independent interest. The proof is self-contained, short, and honest about correcting an earlier erroneous result. The applications in Section 6 give a unified route to several known synonymies. The optimality example is conceptually appealing, but as written its non-synonymy proof omits a load-bearing verification; once that proof is supplied, the paper will be fully convincing. The transfer in Corollary 4.1 is standard and does not appear to be a weak point, since a conceptual theory is exactly one that interprets ac, and the SB construction is formalized uniformly in SB.

major comments (2)
  1. [Section 7] The non-synonymy argument for AS and ACF♭ rests on the assertion, introduced by 'Clearly', that for every finite subset X0 of M there is an order-2 automorphism σ of M fixing X0 and having only finitely many fixed points. This assertion is load-bearing: if σ had infinitely many fixed points, the family {p,σp}^N would not yield infinitely many σ-fixed classes and the contradiction would fail. A proof should be supplied. For instance, one can fix pointwise the finite ∈-transitive closure S of X0 and define σ(⟨i,X⟩)=⟨1−i,σ[X]⟩ for every node not in S; the well-founded recursion on M makes this an involutive automorphism with Fix(σ)=S. As written, the optimality claim is not fully supported.
  2. [Section 7] The sentence 'Clearly there is an infinity of such classes' needs explicit justification. The argument requires that infinitely many distinct classes {p,σp}^N occur as p ranges over the objects of N. This follows from the fact that N is a model of ACF♭ (hence infinite) together with the finiteness of Fix(σ), but the step is not written out. Since this is the only mechanism that produces infinitely many σ-fixed classes, the proof should say explicitly how the orbits of σ under the action on N yield an infinite family of distinct fixed classes.
minor comments (5)
  1. [Section 5] The word 'synonynous' appears in Theorem 5.2 and in Corollary 5.1; it should be 'synonymous'.
  2. [Section 7] There is a typo 'om M' in the sentence about an automorphism on M; it should read 'on M'.
  3. [Theorem 5.3] The notation δK^M is used without being defined; please define the superscript convention or rewrite the displayed identity δK∘M = δK^M ∩ δK in terms of the composition of translations.
  4. [Introduction] The name Ahlbrandt is misspelled as 'Alhbrandt' in the introduction; the reference list correctly spells 'Ahlbrandt'.
  5. [Appendix C] At the end of the verification for the interpretation N, the sentence 'It is now trivial to check that G is indeed an isomorphism' could be expanded, since the definition of G has several clauses and the argument uses the partition of δN into obN and clN.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the main theorem is a genuine reduction of identity-preserving bi-interpretability to synonymy via an independently proved weak Schröder-Bernstein lemma; self-citations are supported by in-paper proofs.

full rationale

Walking the derivation chain, the central argument is self-contained rather than circular. Theorem 5.3 uses the given bi-interpretation only to obtain the definable injection from the full domain into δK, and the weak Schröder-Bernstein theorem (Theorem 4.1) is proved from scratch in the theory SB, whose axioms are exactly the data of two definable injections and whose conclusion is the desired definable bijection; Corollary 4.1 transfers this to conceptual T because conceptuality by definition gives an o-direct interpretation of ac, the base theory of SB. This is a genuine lemma, not an instance of the target theorem: it is stated about virtual classes and injections and says nothing about synonymy. The later steps (Theorems 5.1 and 5.2) are elementary category-theoretic retract arguments, and the identity-preservation assumptions are used, not presupposed. The SB proof is also independently supported by the reported Mizar verification, and the background citations to the authors' earlier work, e.g. [Vis06, Theorem B.1], are not load-bearing in a circular way, since the needed preservation result is proved in Appendix B of the present paper, while [Vis13] is cited only as a survey. The only caveat is in Section 7, where the optimality example relies on an automorphism existence claim introduced by 'Clearly, for any finite subset X0 of M we can find an automorphism σ...' that is not proved in the text; that is a completeness gap or correctness risk, not a circular reduction, because it is not an equation-level equivalence with the input assumptions. Accordingly, no circular step is present.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No free parameters, no new postulated entities. The theories AS, ac, ACF♭ are defined mathematical objects; 'conceptual' is a definition. The SB construction is proved within the paper, so the ledger only records background logical and domain assumptions.

assumptions (4)
  • standard math Classical first-order logic with identity, including the completeness theorem
    Used throughout to move between syntactic provability and semantic model-theoretic statements, e.g., Section 2.3.2 and Theorem A.1.
  • standard math Standard set-theoretic metatheory for constructing models and automorphisms
    Section 7 builds a specific model M of AS and reasons about automorphisms of M; this is ordinary model-theoretic reasoning.
  • domain assumption The notion of sequentiality is captured by direct interpretability of AS (or ac); conceptuality is defined via o-direct interpretation of ac
    The paper adopts Pudlak's and Visser's framework for 'theories with coding' (Sections 3, Appendix B). The main theorem's scope is exactly this class.
  • domain assumption The theory SB (ac extended with equivalence relations and injections) is consistent and its class constructions are formalizable
    Section 4 carries out the Schröder-Bernstein proof inside SB; a failure of the formalization would invalidate Corollary 4.1 and hence Theorem 5.3.

how reviews work

0 comments
Cite this review

Pith. "Pith review of When Bi-interpretability implies Synonymy." pith.science (2026). https://pith.science/paper/GGC2TLLA

@misc{pith2026250601028,
  author       = {Pith},
  title        = {Pith review of: When Bi-interpretability implies Synonymy},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GGC2TLLA}},
  note         = {Machine review of arXiv:2506.01028}
}
read the original abstract

Two salient notions of sameness of theories are synonymy, also known as definitional equivalence, and bi-interpretability. Of these two definitional equivalence is the strictest notion. In which cases can we infer synonymy from bi-interpretability? We study this question for the case of sequential theories. Our result is as follows. Suppose that two sequential theories are bi-interpretable and that the interpretations involved in the bi-interpretation are one-dimensional and identity preserving. Then, the theories are synonymous. The crucial ingredient of our proof is a version of the Schr\"oder-Bernstein theorem under very weak conditions. We think this last result has some independent interest. We provide an example to show that this result is optimal. There are two finitely axiomatized sequential theories that are bi-interpretable but not synonymous, where precisely one of the interpretations involved in the bi-interpretation is not identity preserving.

Figures

Figures reproduced from arXiv: 2506.01028 by the authors.

Figure 1
Figure 1. Illustration of the Proof of Theorem 5.2 We are mainly interested in the following corollary. Corollary 5.1. Suppose U and V are bi-interpretable and one of the witnessing interpretations is direct. Then U and V are synonynous. We now prove our main theorem. Theorem 5.3. Suppose V is conceptual and that K : U → V and M : V → U form a bi-interpretation of U and V . Let K and M both be identity-preserving. Then, U and… view at source ↗
Figure 2
Figure 2. Illustration of the Proof of Theorem 5.3 6.1. Natural Numbers and Integers. The theory PA− is the theory of the non-negative part of a discretely ordered commutative ring, See Richard Kaye’s book [Kay91, Chapter 2] and Emil Jeˇr´abek paper [Jeˇr12] Let DOCR be the theory of a discretely ordered commutative rings. The theories PA− and DOCR are bi￾interpretable. The interpretation of PA− in DOCR is restriction to the … view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

  1. [1]

    Quasi finitely axiomatizable totally categorical theories

    Gisela Ahlbrandt and Martin Ziegler. Quasi finitely axiomatizable totally categorical theories. Annals of Pure and Applied Logic , 30(1):63--82, 1986

    work page 1986

  2. [2]

    String theory

    John Corcoran, William Frank, and Michael Maloney. String theory. The Journal of Symbolic Logic , 39(4):625--636, 1974

    work page 1974

  3. [3]

    Collins and James D

    George E. Collins and James D. Halpern. On the interpretability of A rithmetic in S et T heory. Notre Dame Journal of Formal Logic , 11(4):477--483, 1970

    work page 1970

  4. [4]

    de Bouv \` e re

    Karel L. de Bouv \` e re. Logical synonymy. Indagationes Mathematicae , 27:622--629, 1965

    work page 1965

  5. [5]

    de Bouv \` e re

    Karel L. de Bouv \` e re. Synonymous Theories . In John W. Addison, Leon Henkin, and Alfred Tarski, editors, The Theory of Models, Proceedings of the 1963 International Symposium at Berkeley , pages 402--406. North Holland, Amsterdam, 1965

    work page 1963

  6. [6]

    Categoricity-like properties in the first order realm

    Ali Enayat and Mateusz e yk. Categoricity-like properties in the first order realm. Journal for the Philosophy of Mathematics , 1:63--98, 2024

    work page 2024

  7. [7]

    -models of finite set theory

    Ali Enayat, James Schmerl, and Albert Visser. -models of finite set theory. In J. Kennedy and R. Kossak, editors, Set Theory, Arithmetic and Foundations of Mathematics:Theorems, Philosophies , number 36 in ASL Lecture Notes in Logic, pages 43--65. ASL and Cambridge University Press, New York, 2010

    work page 2010

  8. [8]

    Model theory

    Wilfrid Hodges. Model theory . Encyclopedia of Mathematics and its Applications, vol. 42. Cambridge University Press, Cambridge, 1993

    work page 1993

Show all 33 references
  1. [9]

    Metamathematics of First-Order Arithmetic

    Petr H \'a jek and Pavel Pudl \'a k. Metamathematics of First-Order Arithmetic . Perspectives in Mathematical Logic. Springer, Berlin, 1993

    1993

  2. [10]

    Sequence encoding without induction

    Emil Je r \' a bek. Sequence encoding without induction. Mathematical Logic Quarterly , 58(3):244--248, 2012

    2012

  3. [11]

    Joosten and Albert Visser

    Joost J. Joosten and Albert Visser. The interpretability logic of all reasonable arithmetical theories. Erkenntnis , 53(1--2):3--26, 2000

    2000

  4. [12]

    Models of P eano A rithmetic

    Richard Kaye. Models of P eano A rithmetic . Oxford Logic Guides. Oxford University Press, Oxford, 1991

    1991

  5. [13]

    On interpretations of arithmetic and set theory

    Richard Kaye and Tin Lok Wong. On interpretations of arithmetic and set theory. Notre Dame Journal of Formal Logic , 48(4):497--510, 2007

    2007

  6. [14]

    Set Theory with and without urelements and categories of interpretations

    Benedikt L \"o we. Set Theory with and without urelements and categories of interpretations . Notre Dame Journal of Formal Logic , 47(1):83--91, 2006

    2006

  7. [15]

    A minimal predicative set theory

    Franco Montagna and Antonella Mancini. A minimal predicative set theory. Notre Dame Journal of Formal Logic , 35(2):186--203, 1994

    1994

  8. [16]

    Jan Mycielski, Pavel Pudl \'a k, and Alan S. Stern. A lattice of chapters of mathematics (interpretations between theorems) , volume 84 of Memoirs of the American Mathematical Society . AMS, Providence, Rhode Island, 1990

    1990

  9. [17]

    Predicative arithmetic

    Edward Nelson. Predicative arithmetic . Princeton University Press, Princeton, 1986

    1986

  10. [18]

    How to escape T ennenbaum's T heorem

    Fedor Pakhomov. How to escape T ennenbaum's T heorem. arXiv preprint , arXiv:2209.00967, 2022

    2022 arXiv

  11. [19]

    Some prime elements in the lattice of interpretability types

    Pavel Pudl \'a k. Some prime elements in the lattice of interpretability types. Transactions of the American Mathematical Society , 280:255--275, 1983

    1983

  12. [20]

    Cuts, consistency statements and interpretations

    Pavel Pudl \'a k. Cuts, consistency statements and interpretations. The Journal of Symbolic Logic , 50(2):423--441, 1985

    1985

  13. [21]

    Concatenation as a B asis for A rithmetic

    Willard Van Orman Quine. Concatenation as a B asis for A rithmetic. The Journal of Symbolic Logic , 11(4):105--114, 1946

    1946

  14. [22]

    Definability and Decision Problems in Arithmetic

    Julia Robinson. Definability and Decision Problems in Arithmetic . Journal of Symbolic Logic , 14(2):98--114, 1949

    1949

  15. [23]

    Nonstandard models and related developments

    Craig Smory\' n ski. Nonstandard models and related developments . In Leo A. Harrington, Michael D. Morley, Andre Scedrov, and Stephen G. Simpson, editors, Harvey F riedman's Research on the Foundations of Mathematics , pages 179--229. North Holland, Amsterdam, 1985

    1985

  16. [24]

    Mutual Interpretability of some essentially undecidable theories

    Wanda Szmielew and Alfred Tarski. Mutual Interpretability of some essentially undecidable theories . In Proceedings of the International Congress of Mathematicians (Cambridge, Massachusetts, 1950) , volume 1, page 734. American Mathematical Society, Providence, 1952

    1950

  17. [25]

    Interpretability logic

    Albert Visser. Interpretability logic. In Petio Petrov Petkov, editor, Mathematical logic, P roceedings of the H eyting 1988 summer school in V arna, B ulgaria , pages 175--209. Plenum Press, Boston, 1990

    1988

  18. [26]

    An inside view of E X P

    Albert Visser. An inside view of E X P . The Journal of Symbolic Logic , 57(1):131--165, 1992

    1992

  19. [27]

    The unprovability of small inconsistency

    Albert Visser. The unprovability of small inconsistency. Archive for Mathematical Logic , 32(4):275--298, 1993

    1993

  20. [28]

    An Overview of Interpretability Logic

    Albert Visser. An Overview of Interpretability Logic . In Marcus Kracht, Maarten de Rij\-ke, Heinrich Wansing, and Michael Zakharyaschev, editors, Advances in Modal Logic , volume 1, 87 of CSLI Lecture Notes , pages 307--359. Center for the Study of Language and Information, S...

    1998

  21. [29]

    Faith & F alsity: a study of faithful interpretations and false ^0_1 -sentences

    Albert Visser. Faith & F alsity: a study of faithful interpretations and false ^0_1 -sentences. Annals of Pure and Applied Logic , 131(1--3):103--131, 2005

    2005

  22. [30]

    Categories of T heories and I nterpretations

    Albert Visser. Categories of T heories and I nterpretations. In Ali Enayat, Iraj Kalantari, and Mojtaba Moniri, editors, Logic in T ehran. P roceedings of the workshop and conference on L ogic, A lgebra and A rithmetic, held O ctober 18--22, 2003 , volume 26 of Lecture N otes ...

    2003

  23. [31]

    Pairs, sets and sequences in first order theories

    Albert Visser. Pairs, sets and sequences in first order theories. Archive for Mathematical Logic , 47(4):299--326, 2008

    2008

  24. [32]

    Cardinal arithmetic in the style of B aron von M \"u nch\-hausen

    Albert Visser. Cardinal arithmetic in the style of B aron von M \"u nch\-hausen. Review of Symbolic Logic , 2(3):570--589, 2009

    2009

  25. [33]

    Albert Visser. What is sequentiality? In Patrick C \' e gielski, Charalampos Cornaros, and Costas Dimitracopoulos, editors, New Studies in Weak Arithmetics , volume 211 of CSLI Lecture Notes , pages 229--269. CSLI Publications and Presses Universitaires du P \^ o le de Recherc...

    2013

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.