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-M50535338aba17e1ec9299065
Delivery options: https://agi.topicbox.com/groups/agi/subscription
