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)
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]