AI 中文总结
该研究引入遗传有限多重集的一阶理论WF⁻和F⁻，证明WF⁻与R、F⁻与Q相互可解释，F⁻本质不可判定。克服多重集恢复有序对障碍，展示顺序与多重性的关系，还证明公理独立性及应用于斯宾塞 - 布朗形式，定位本质不可判定边界。
AI 中文摘要
我们引入了两种遗传有限多重集的一阶理论：一个模式理论WF⁻和一个有限可公理化理论F⁻，其语言包含空多重集、单元素形成、多重集并集和一个包含关系。我们证明WF⁻与罗宾逊理论R相互可解释，F⁻与罗宾逊算术Q相互可解释；特别是，F⁻本质上是不可判定的。多重集因此加入了数、字符串、树、集合和序列，在R和Q的相互可解释类中。多重集情况的独特障碍是用于恢复有序对的标准方法同时失效。我们表明顺序可从纯多重性恢复：项π(x,y)=<x>∪<x>∪<y>在F⁻中可证是单射的，产生了克里斯蒂安森 - 穆尔瓦纳夏卡树理论T的直接解释；反之，F⁻通过在有界算术中对多重集项的范式演算进行算术化在Q中得到解释。F⁻的每个结构公理都被证明与其他公理独立，有有限或普雷斯伯格可定义的可判定见证，并且包含公理是保守的。作为应用，我们将斯宾塞 - 布朗的模交换并置形式与遗传有限多重集进行了识别，并在指示演算中定位了本质不可判定的边界。
英文摘要
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.
Comments21 pages
