Axiom talk:Leibniz's Law

Leibniz's Law should not be adopted as an axiom, but rather can be proven (in set theory) from the definition of set equality and induction on the well-formed parts of $P(x)$. One direction is Substitutivity of Equality, while the other direction is a special case of Definition:Set Equality. --Andrew Salmon 23:12, 6 August 2012 (UTC)

Are you sure the links you are pointing to are talking about the equality of $x$ and $y$, rather than the equality of $P$ to another $P$ ? --GFauxPas 04:33, 7 August 2012 (UTC)

Yes. --Andrew Salmon 04:36, 7 August 2012 (UTC)

Can you finish Substitutivity of Equality so I can think about your comment more? In any event, it needs to be kept as an axiom for systems where it can't be proven in. --GFauxPas 04:44, 7 August 2012 (UTC)

Also, that page says "Let $x$ and $y$ be sets", I don't see it proving anything for $x$ and $y$ being objects that are not sets. --GFauxPas 04:50, 7 August 2012 (UTC)

Then use Substitutivity of Class Equality and Definition:Class Equality. In Set Theory, all objects are classes. I'll finish the proofs... --Andrew Salmon 04:58, 7 August 2012 (UTC)

And in other systems they are not. And I'd venture to say that even in set theory you need non-set objects when the universe of discourse is the physical universe. In any event, PW has defined equality and set equality differently. In many systems, "$=$" is a primitive term. What I recommend doing is creating a proof that in ZFC, "equals" can be defined in terms of "set equality". (Of course that doesn't mean that it has to be defined that way, but that it can). That would be a nice theorem, if it is a theorem. --GFauxPas 05:12, 7 August 2012 (UTC)

We have plenty of pages introduced as "axioms" which can technically be derived from another series of "even more axiomatic" statements. However, those statements are "axiomatic" in the sense that in any particular field of endeavour they are taken as the base statements.

One can in fact make the case that Leibniz's Law is the standard axiomatic statement on which set equality itself is based. So while you can derive Leibniz's Law from set equality, you can also do it the other way. Leibniz came first, "Leibniz's Law" has standing as an axiom.

There is a case for a page to be added for Leibniz's Law to be proved from set equality, but I seriously doubt it would do philosophical justice to the full thrust of Leibniz's original statement, which applies to all objects, not just sets. The fact that in mathematics, everything is (ultimately) a set weakens this statement. --prime mover 05:13, 7 August 2012 (UTC)

For pedantry it be noted that I am reading on categorical foundations lately, which provide a different characterisation of mathematics where the concept 'set' is not even (strictly speaking) defined. But I don't even grasp it fully myself, so I shut up already. --Lord_Farin 06:22, 7 August 2012 (UTC)