Weak essentially undecidable theories of hereditarily finite multisets

Platon Sifnaios

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.

Disclosure

“lity, exactly Robinson’s Q; and it is activated neither by iteration, nor by multiplicity, nor by feedback, but by unbounded discriminability of form within form. Acknowledgements During the preparation of this manuscript the author used Claude (Anthropic) as a sup- port tool for literature search, language editing, LaTeX drafting, bibliographic checking, and assistance with the formal expression of mathematical arguments. The research questions, conceptual development, mathemati”
PDF page 19

Classification: Proof ideas or individual proof-step assistance
Multiplier: 8
Verified: 2026-08-23T18:51:27.982755Z

Structural counts

Pages 21 pdf

Theorems 10 source

Lemmas 11 source

Propositions 9 source

Corollaries 6 source

Definitions 0 source

Displayed equations 15 source

Bibliography entries 38 source

Appendix pages 0 estimated

Count notes

Source counts use the expanded primary TeX file main.tex.
Appendix pages include the first PDF page with an explicit Appendix heading through the final page.