Is the Axiom of Extensionality equivalent to Leibniz's Law?

Question

Leibniz's law states that $$ \forall x\forall y[\forall P(Px \equiv Py) \rightarrow x = y]. $$ This seems awfully similar to the Axiom of Extensionality, $$ \forall A \forall B[\forall x(x\in A \equiv x \in B)\rightarrow A = B]. $$ Within the framework of set theory, are these logically equivalent? Is Extensionality a strictly stronger statement? Are they even comparable?

Answer 1

It depends on how you interpret Leibniz' law.

Leibniz' law follows from Extensionality if we allow predicates of the form "contains $x$" for arbitrary $x$. But arbitrary $x$ are not in general definable in any nice way, so these predicates wouldn't be expressibile in any nice way. To give an example of why that's a problem, consider the predicate "$=x$" - this is expressible in terms of $x$, and serves to distinguish any $y\not=x$ from $x$, since $x$ satisfies the predicate "$=x$" but such a $y$ doesn't satisfy the predicate "$=x$".

So a too-broad interpretation of what predicates can be trivializes Leibniz' law. But it is exactly that kind of broad interpretation which allows extensionality to imply Leibniz' law in general - there can be indiscernible elements which are different but can't be distinguished by any formula in whatever fixed system we're working in.

What about the other way around? This also fails, and a good example of this happening in an interesting situation can be provided by certain set theories with urelements. In these set theories, we start with a bunch of "atoms" (or "urelements") in addition to the empty set. These urelements may come with additional structure, algebraic or topological or whatever - for instance, we could start with a ring of urelements. In this case we may be able to distinguish urelements from each other in a nice, definable way. But any two urelements have the same elements, namely none.

So really, neither implies the other; the most that can be said is that a too-liberal interpretation of Leibniz' law is trivially true, and hence a fortiori follows from extensionality.