I appended this to the Introduction: Terminological clarification
When we say that three-place relative identity is sufficient to express all of mathematics, we mean the axioms of ZFC can be formulated and faithfully interpreted using identity as the sole primitive, via definitional translations. This is merely relative interpretability in the usual logical sense. We do not claim that the axioms of relative identity alone suffice to derive or model ZFC. The present result establishes expressive adequacy and interpretability, not foundational sufficiency in the model-theoretic sense. This is necessary clarification in any paper dealing with mathematical foundations. A lot of confusion in early papers regarding Category Theory, for example, were so-misinterpreted. On Sat, Dec 27, 2025 at 9:44 AM James Bowery <[email protected]> wrote: > https://spasim.org/docs/UniversalityOfThreePlaceIdentity.pdf > > Abstract > We present a formal proof, mechanized in Lean 4, of Tom Etter’s > Universality Theorem: that three-place relative identity is foundationally > adequate for all of mathematics. The proof establishes a mutual > interpretability between identity theory and Zermelo-Fraenkel set theory > through two definitional bridges. We discuss the philosophical significance > of this result for foundations of mathematics, the nature of existence, and > the relationship between logic and ontology. > > 1 Introduction > > The question of foundational primitives in mathematics has occupied > logicians since Frege. The standard answer—that set membership ∈ suffices > as the sole primitive, with all mathematical objects reducible to sets—has > proven technically successful but philosophically unsatisfying. As > Benacerraf observed, the arbitrariness of set-theoretic encodings (why is 2 > = {∅, {∅}} rather > than {{∅}}?) suggests that sets may not capture the essence of > mathematical objects. Tom Etter proposed a radical alternative: that > identity, not membership, is the true primitive. But not the two-place > identity x = y of classical logic, which Quine showed to be expressively > impoverished. Rather, a three-place relative identity x(y = z), read “x > regards y as the same as > z.” > > This paper presents a machine-verified proof that Etter’s identity theory > is universal—capable of expressing all of mathematics. The proof has been > formalized in Lean 4. The only Mathlib dependency is in the progress > reporting module UniversalityTheorem.Progress which is not part of the > proof. The Lean4 source is available at > http://github.com/jabowery/RelativeIdentity > ------------------------------------------ Artificial General Intelligence List: AGI Permalink: https://agi.topicbox.com/groups/agi/Tc1a08ad9a0c8750c-M2326257f86135a96729d3505 Delivery options: https://agi.topicbox.com/groups/agi/subscription
