Different formalisations have different ideas of what “equals” means.
Principia Mathematica took the approach that for booleans p and q you have a relation p \equiv q, and then if you have some universe of objects and predicates on those objects, x equals y iff for all predicates f [in your universe of predicates] f(x) \equiv f(y).
But that’s not how typical automated theorem provers define equals.
PM is kind of backwards relative to how it’s usually done. You can start with equals as a primitive notion, and then have an axiom of referential transparency that x = y → f(x) = f(y)
But PM did it backwards, define x = y as \forall f : f(x) \equiv f(y)
Different formalisations have different ideas of what “equals” means.
Principia Mathematica took the approach that for booleans p and q you have a relation p \equiv q, and then if you have some universe of objects and predicates on those objects, x equals y iff for all predicates f [in your universe of predicates] f(x) \equiv f(y).
But that’s not how typical automated theorem provers define equals.
PM is kind of backwards relative to how it’s usually done. You can start with equals as a primitive notion, and then have an axiom of referential transparency that x = y → f(x) = f(y)
But PM did it backwards, define x = y as \forall f : f(x) \equiv f(y)
having just gone and investigated how Lean does it:
axiom propext : ∀ {a b : Prop}, (a ↔ b) → a = b
[i.e. for Prop — not arbitrary types — there’s an axiom that says equivalence implies equality]