Weak essentially undecidable theories of hereditarily finite multisets

Platon Sifnaios

REVIEW 2 major objections 2 minor 1 cited by

Weak essentially undecidable theories of hereditarily finite multisets

T0 review · 2 major / 2 minor · reviewed 2026-07-14 · grok-4.5

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

Pith's one-line read Hereditarily finite multisets alone yield theories mutually interpretable with Robinson arithmetic Q and R, hence essentially undecidable.

desk verdict Abstract-only multiset theories claiming mutual interpretability with R and Q via a multiplicity pairing; coherent and potentially solid, but proofs are the whole game. read the letter →

arxiv 2607.11367 v1 pith:HSBZJMN5 submitted 2026-07-13 math.LO

Platon Sifnaios This is my paper · ORCID

classification math.LO MSC 03F3003B2503E30

keywords hereditarilyfinitemultisetsessentialundecidabilitymutualinterpretabilityRobinsonarithmeticQtheoryRinjectivepairingmultisettermscalculusofindications

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

This paper shows that two natural first-order theories of hereditarily finite multisets already sit in the mutual-interpretability classes of Robinson arithmetic Q and of Robinson's weaker theory R. The finitely axiomatized theory F− is mutually interpretable with Q and is therefore essentially undecidable; the schematic theory WF− is mutually interpretable with R. Multisets thereby join numbers, strings, trees, sets and sequences as base structures that can encode full arithmetic. The distinctive difficulty is that ordinary pairing devices fail: there is no positional order, no local order on immediate constituents, and no idempotence for Kuratowski pairing. The author recovers ordered pairs from bare multiplicity alone by proving that the term π(x,y)=⟨x⟩∪⟨x⟩∪⟨y⟩ is injective inside F−, which immediately interprets a known undecidable tree theory; the converse direction arithmetizes a normal-form calculus for multiset terms inside bounded arithmetic. Each structural axiom of F− is independent of the rest, and the same multiset reading identifies Spencer-Brown forms (modulo commutative juxtaposition) with hereditarily finite multisets, locating the onset of essential undecidability inside the calculus of indications.

What carries the argument

The term π(x,y)=⟨x⟩∪⟨x⟩∪⟨y⟩, proved injective in F−. It supplies an ordered-pair coding from pure multiplicity, allowing a direct interpretation of an already-undecidable tree theory and thereby carrying the essential undecidability of F−.

What would settle it

A model of F− (or even of its structural axioms alone) in which the term π(x,y)=⟨x⟩∪⟨x⟩∪⟨y⟩ fails to be injective, or a proof that no interpretation of Q into F− exists.

Watch

Extended reading notes

Core claim

The theories F− and WF− of hereditarily finite multisets, written in the language of empty multiset, singleton, union and containment, are mutually interpretable with Robinson arithmetic Q and Robinson's R respectively; in particular F− is essentially undecidable. Order is recovered from multiplicity by the injectivity, already inside F−, of the term π(x,y)=⟨x⟩∪⟨x⟩∪⟨y⟩, which yields a direct interpretation of the Kristiansen–Murwanashyaka tree theory T, while F− itself is interpreted in Q by an arithmetization of multiset normal forms.

Load-bearing premise

That ordered pairs can be recovered from bare multiplicity alone because the specific double-singleton term π(x,y) is already injective in the weak multiset theory F−.

Editorial extensions

If this is right

Multisets join numbers, strings, trees, sets and sequences in the mutual-interpretability classes of Q and R.
F− is essentially undecidable, so every consistent extension of F− is undecidable.
Each structural axiom of F− is independent of the others, witnessed by finite or Presburger-definable models.
Spencer-Brown forms modulo commutative juxtaposition are identified with hereditarily finite multisets, placing the boundary of essential undecidability inside the calculus of indications.
The containment axiom is conservative over the remaining axioms of F−.

Reading between the lines

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

Any further weakening that destroys injectivity of π would drop the theory out of the Q-class, giving a sharp threshold for essential undecidability among multiset axioms.
The same multiplicity coding should adapt to other commutative structures (bags, commutative words, free commutative monoids) and may yield uniform undecidability proofs for them.
Independence witnesses that are Presburger-definable suggest that fragments of F− remain decidable once the pairing term is removed, inviting a complete classification of decidable subtheories.

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.

Desk Editor's Note

read the letter

The punchline is that this paper puts hereditarily finite multisets into the same mutual-interpretability classes as R and Q, via two theories WF^- and F^-, and that the key technical move is recovering an injective pairing from bare multiplicity alone. That is a real addition to the short list of combinatorial structures that support essential undecidability in weak first-order theories.

What looks new and cleanly framed: the simultaneous failure of the usual pairing devices (positional order, local order on constituents, Kuratowski via idempotence) is the genuine obstacle for multisets, and the claim that π(x,y) = ⟨x⟩ ∪ ⟨x⟩ ∪ ⟨y⟩ is provably injective in F^- is the load-bearing fix. If that holds, the direct interpretation of the Kristiansen–Murwanashyaka tree theory T follows, and the reverse direction by arithmetizing a normal-form calculus for multiset terms inside Q is the natural counterpart. The independence results for the structural axioms, with finite or Presburger-definable witnesses, and the conservativity of the containment axiom, are the kind of careful housekeeping that makes these papers useful. The Spencer-Brown application is a nice extra, not the main load.

The soft spot is exactly the one the reader and stress-test flag: we have only the abstract. No lemmas, no proof of injectivity of π, no details of the normal-form arithmetization. That is not a flaw in the argument as stated; it is simply missing evidence. Nothing in the abstract looks circular or smuggled. The research program is standard and the claims sit inside it without red flags. Confidence has to stay low until the body is checked, but the shape is ACCEPT-shaped if the proofs are there.

This is for people who work on weak arithmetic, interpretability, and essential undecidability of combinatorial theories. A serious referee should see it. I would send it to peer review; the missing proofs are what the referees are for. Bring it to reading group only after the full text is up, or if someone wants to try reconstructing the pairing argument from the abstract alone.

Referee Report

2 major / 2 minor

Summary. The manuscript introduces two first-order theories of hereditarily finite multisets, WF^- (schematic) and F^- (finitely axiomatized), in a language with empty multiset, singleton, multiset union, and containment. It claims that WF^- is mutually interpretable with Robinson's R and F^- with Robinson arithmetic Q, so that F^- is essentially undecidable; multisets thereby join the known mutual-interpretability classes of R and Q. The central technical device is the multiplicity pairing term π(x,y)=⟨x⟩∪⟨x⟩∪⟨y⟩, claimed to be provably injective in F^- and thereby to yield a direct interpretation of the Kristiansen–Murwanashyaka tree theory T, while the converse interpretation of F^- in Q proceeds by arithmetizing a normal-form calculus for multiset terms. Independence of each structural axiom of F^- (with finite or Presburger-definable witnesses) and conservativity of the containment axiom are also claimed, together with an application identifying Spencer-Brown forms modulo commutative juxtaposition with hereditarily finite multisets.

Significance. If the claimed mutual interpretabilities hold, the paper supplies a clean, natural example of essential undecidability for a combinatorial theory of multisets, filling a gap left by the known cases of numbers, strings, trees, sets and sequences. The recovery of ordered pairs from bare multiplicity via a single injective term, despite the simultaneous failure of positional order, local order and Kuratowski-style idempotence, would be a distinctive technical contribution. The independence and conservativity results, and the location of the undecidability boundary inside the calculus of indications, would further strengthen the paper's place in the literature on weak essentially undecidable theories.

major comments (2)

Only the abstract is available for review. The load-bearing claims—mutual interpretability of F^- with Q and of WF^- with R, injectivity of π in F^-, the direct interpretation of T, the reverse arithmetization of a normal-form calculus inside Q, and the independence of each structural axiom—are stated as proved but cannot be checked. Without the full text these derivations remain unverified; the recommendation is therefore necessarily provisional pending the complete manuscript.
The injectivity of π(x,y)=⟨x⟩∪⟨x⟩∪⟨y⟩ is identified as the distinctive obstacle of the multiset case and is load-bearing for the interpretation of T (and hence for mutual interpretability with Q). The abstract asserts that this injectivity is provable in F^- despite the failure of the usual pairing devices, but supplies neither the precise axioms of F^- nor a sketch of the argument. Verification of this single claim is indispensable for the central result.

minor comments (2)

The structural axioms of WF^- and F^- are not listed in the abstract; a short display of the language and the finite axiom set of F^- would make the claims self-contained even at abstract length.
The application to Spencer-Brown forms is intriguing but is stated only in a single sentence; a precise statement of the identification and of the location of the undecidability boundary would clarify the scope of the application.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: abstract-only mutual interpretability claims with classical external theories R and Q.

full rationale

Only the abstract is available, so no internal equations, proofs, or self-citations can be inspected for reduction-by-construction. The abstract presents F^- as mutually interpretable with Robinson arithmetic Q (hence essentially undecidable) and WF^- with Robinson's R, via two constructions: (i) the term π(x,y)=⟨x⟩∪⟨x⟩∪⟨y⟩ claimed provably injective in F^-, yielding a direct interpretation of the independent Kristiansen–Murwanashyaka tree theory T, and (ii) an interpretation of F^- in Q by arithmetizing a normal-form calculus for multiset terms. These are framed as genuine technical constructions that overcome the simultaneous failure of positional order, local order, and Kuratowski pairing; they are not presented as definitional renamings of the target undecidability, nor as fits of free parameters to data. Mutual interpretability with the classical external theories R and Q is the standard, non-circular route to essential undecidability in this literature. No self-definitional loop, fitted-input-as-prediction, load-bearing self-citation, uniqueness theorem imported from the same authors, ansatz smuggled via citation, or renaming of a known result is visible in the abstract. The distinctive injectivity claim is a mathematical assertion to be verified by proof, not a circularity. Score 0 is therefore the honest finding for an abstract-only review of a pure logic paper of this type; any later circularity would require the full text.

Assumptions & free parameters 0 free parameters · 3 assumptions · 2 invented entities

Abstract-only review: free parameters are not visible (pure logic paper). Axioms are the standard background of first-order logic plus the (unlisted) structural axioms of WF^- and F^- that the paper itself introduces and then shows independent. No invented physical entities; the theories and the pairing term π are mathematical constructions. Full axiom list would require the paper body.

assumptions (3)

standard math Standard first-order logic with equality and the usual rules of deduction.
Background for any first-order theory of R/Q interpretability; assumed throughout.
ad hoc to paper The (unlisted in abstract) structural axioms of F^- and WF^- governing empty multiset, singleton, union, and containment.
These are the paper's own axiomatizations; the abstract states each structural axiom of F^- is independent of the others.
domain assumption Robinson arithmetic Q (and R) as the external target of mutual interpretability.
Classical weak arithmetic theories used as the interpretability benchmarks.

invented entities (2)

Theories WF^- and F^- of hereditarily finite multisets
purpose: Provide first-order axiomatizations whose interpretability strength matches R and Q.
New theories introduced by the paper; their existence and strength are the contribution, not postulated particles or forces.
Multiplicity pairing term π(x,y) = ⟨x⟩ ∪ ⟨x⟩ ∪ ⟨y⟩
purpose: Recover injective ordered pairing from bare multiplicity when standard pairing devices fail.
Defined construction claimed to be provably injective in F^-; independent evidence would be the formal proof in the full paper.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Weak essentially undecidable theories of hereditarily finite multisets." pith.science (2026). https://pith.science/paper/HSBZJMN5

@misc{pith2026260711367,
  author       = {Pith},
  title        = {Pith review of: Weak essentially undecidable theories of hereditarily finite multisets},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HSBZJMN5}},
  note         = {Machine review of arXiv:2607.11367}
}

read the original abstract

We introduce two first-order theories of hereditarily finite multisets: a schematic theory WF^- and a finitely axiomatized theory F^-, in the language with the empty multiset, singleton formation, multiset union, and a containment relation. We prove that WF^- is mutually interpretable with Robinson's theory R, and F^- with Robinson arithmetic Q; in particular, F^- is essentially undecidable. Multisets thereby join numbers, strings, trees, sets, and sequences in the mutual-interpretability classes of R and Q. The distinctive obstacle of the multiset case is the simultaneous failure of the standard devices for recovering ordered pairs: positional order, local order on immediate constituents, and idempotence-based Kuratowski pairing. We show that order is recoverable from bare multiplicity: the term pi(x,y) = <x> u <x> u <y> is provably injective in F^-, yielding a direct interpretation of the Kristiansen-Murwanashyaka tree theory T; conversely, F^- is interpreted in Q by arithmetizing a normal-form calculus for multiset terms within bounded arithmetic. Each structural axiom of F^- is shown independent of the others, with finite or Presburger-definable decidable witnesses, and the containment axiom is conservative. As an application, we identify Spencer-Brown's forms modulo commutative juxtaposition with hereditarily finite multisets and locate the boundary of essential undecidability within the calculus of indications.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

The gate of self-address: where decidable adjudication ends
math.LO 2026-07 accept novelty 6.0 of 10

A single self-referential query gate makes total correct adjudication impossible; bounding the depth keeps every finite level decidable, and full adjudication costs exactly one Turing jump.

Pith tools

Reviewed July 14, 2026 · model on record in the stance chip above.