In Frederic Schuller's lecture series Lectures on Geometrical Anatomy of Theoretical Physics, he declares (here) the first axiom of ZFC set theory to be the Axiom on $\in$-Relation, stated as follows:
Informal:
"$x\in y$" is a proposition if and only if $x$ and $y$ are both sets.
Formal:
$\forall x:\forall y:(x\in y)\veebar \neg(x\in y)$.
The "formal" version above (where $\veebar$ means "exclusive or") is not given in the lecture, but is stated in Simon Rea's transcription of the lectures, found here (p. 8).
Schuller does not include the traditional Axiom of Extensionality that I have seen in every other ZFC book, which states that two sets are equal if and only if their elements are identical.
Two questions:
-
Does the "formal" statement above actually encode the "informal" version given by Schuller? I can maybe see this, if the implication is that our axioms simply don't discuss variables $x$ and $y$ unless they are sets, but no other formal encodings are of the same nature, so I'm not convinced.
-
Is Schuller's axiom equivalent to the Axiom of Extensionality, all other axioms being equal? On the one hand, Schuller is a very smart man whose lectures on physics tend to be carefully thought out and steeped in mathematical rigor. On the other hand, I can't possibly see how the two are equivalent and can find absolutely no other references to Schuller's axiom online.
Best Answer
No, that's absolutely bonkers: Schuller's "axiom" is just an instance of LEM, which is built directly into the underlying logic itself. Extensionality is much more interesting than that: it says that the elementhood relation completely determines the identity of a set. One direction of this is trivial - certainly two equal sets have the same elements - but the other direction is much less trivial than it may first appear.
I think that what's happened is that Schuller has internalized Extensionality as something so basic that it's on the level of logical rules as opposed to axioms, and so he's managed to conflate it with an (instance of an) actual logical rule. But in fact we can quite easily work with failures of Extensionality without breaking logic!
The most important kind of failure of extensionality in my opinion is given by urelements. Urelements are things other than the emptyset $\emptyset$ which don't have any elements; the only way we can have them is if Extensionality isn't present. Generally, when we switch from Extensionality to (the option of having) urelements things change in quite interesting ways:
It's relatively easy to prove that the axiom of choice is not provable in ZF - Extensionality, whereas proving its independence from ZF is much harder. That said, the two approaches turn out after the fact to be closely related.
Looking at weak subtheories of ZF in the context of (higher) computability theory, Barwise showed that urelements are extremely useful in the context of admissibility theory; see his book.
For an even more extreme if more technical example, consider the difference between Quine's set theories NF and NFU (= NF without Extensionality). On the one hand, NF disproves Choice, consequently proves Infinity, and is not known to be consistent even relative to large cardinals (Holmes has a claimed consistency proof, but I don't think it's been fully vetted yet). On the other hand, NFU is consistent relative to PA, is consistent with Choice, and is consistent with the negation of Infinity. So here in fact we have a situation where adding Extensionality to a reasonably-well-behaved theory results in something which at least according to our current understanding is quite wild!