8
$\begingroup$

This question was essentially asked and responded to here, but I don't feel it was really answered:

Is the axiom of extensionality merely called an "axiom" by convention, or is there a clear distinction between axioms and definitions that forbids it from being considered a definition of set equality?

The answer in the linked post seems to address what would happen if the axiom were rejected altogether, but doesn't discuss whether there is good reason to consider it an axiom rather than a definition. If axioms and definitions are just two different words for the same thing, then that's fine—but I get the feeling I'm missing something. Do we simply call a definition an axiom if it defines a particularly foundational concept (like equality)?

Improve this question
$\endgroup$
  • $\begingroup$ If we consider equality as a relation defined by the axiom of extensionality, then we need another axiom to tell us that "if $x=y$ and $x\in z$ then $y\in z.$" With the usual treatment, that would be taken care of by the logic of equality. At least that's how I understand it. Let's see what the experts on logic and set theory say. $\endgroup$ – bof Apr 2 '18 at 5:18
  • 2
    $\begingroup$ One way or another, you've got to be able to prove that $$\forall z(z\in x\leftrightarrow z\in y)\leftrightarrow\forall z(x\in z\leftrightarrow x\in y)$$ and I think you will need some axiom for that. $\endgroup$ – bof Apr 2 '18 at 5:26
  • 1
    $\begingroup$ @leibnewtz I mean that, instead of formalizing your set theory in first order logic with equality, you can formalize it in first order logic without equality. Since you don't have the logical notion of equality, you have to define it, e.g. by extensionality. But you still need axioms to make your defined equality work like it should. $\endgroup$ – bof Apr 2 '18 at 5:29
  • 1
    $\begingroup$ In many forms of set theory the axiom of extensionality is used to define equality. The traditional language of set theory only includes $\in$, so that $=$ has to be defined separately. However, the axiom of extensionality is phrased slightly differently in this case; see the Wikipedia article en.wikipedia.org/wiki/… $\endgroup$ – Carl Mummert Apr 2 '18 at 20:17
  • 1
    $\begingroup$ @bof Did you mean $\forall z(z \in x \leftrightarrow z \in y) \leftrightarrow \forall z (x \in z \leftrightarrow y \in z)$? $\endgroup$ – user76284 Apr 10 '19 at 18:11
12
$\begingroup$

First-order logic can be defined with or without equality. If you are working in a first-order logic with equality, which is the typical case, then stating that $X = Y \iff \forall x.x\in X\Leftrightarrow x \in Y$ is a substantial axiom that could lead to contradiction. The benefit of working in a logic with equality is that you have the rule for replacing equals for equals in predicates. As bof mentioned, this is the indiscernibility of identicals $\cfrac{x = y\qquad P(x)}{P(y)}$. Having the equality as part of the logic also impacts semantics (though considering models of set theory isn't a thing one normally does unless they are a set theorist). If equality is part of the logic, then we require equality to actually be equality in the semantics.

If, instead, we use a first-order logic without equality, then $=$ is just another binary predicate symbol like any other. No different than $\in$. In this case, the "axiom" of extensionality is merely its definition. The indiscernibility of identicals is now a meta-theorem that you would need to prove, and could easily fail to be true. This wouldn't be a problem but it would mean that the $=$ relation wouldn't behave like equality. (Again, to contrast, in FOL with equality, a failure of the indiscernibility of identicals would be a contradiction.) Semantically, $=$ would just be modeled as an equivalence relation that was compatible with $\in$.

So whether the "axiom of extensibility" is a non-trivial logical assertion or a definition depends on whether equality is already defined or not. In FOL with equality, it is and thus this is an axiom that, quite possibly, could cause a contradiction. In FOL without equality, this is merely a definition of a binary relation symbol and can't possibly cause contradiction; it can only be misleading. I should say from the perspective of informal proofs, it makes no difference which view you take. For more formal proofs, if you can use the meta-theorem proving the indiscernibility of identicals, then it also won't be much different, but that meta-theorem just means that an actual formal proof exists. The actual formal proof could be quite large where, if we were working in a logic with equality, it would be a single step of inference. This would be an issue for a mechanized implementation of logic or if you wanted to actually write out the formal proof. In this vein, working in a logic with equality is much more convenient.

Improve this answer
$\endgroup$
6
$\begingroup$

If you're asking about why the axiom of extensionality is needed in set theory specifically, the answer isn't about $=$ but rather about $\in$.

Remember that a priori, "$\in$" is just some binary relation symbol. Structures in the language $\{\in\}$ are essentially just directed graphs where there is at most one edge between any two vertices. Thought of this way, extensionality says:

If $a, b$ are vertices, and every vertex with an edge to $a$ also has an edge to $b$ and vice versa, then $a=b$.

Obviously this is not true in general! E.g. consider a graph with fifteen vertices and no edges. Basically, the point is that the semantics for first-order logic does understand what "$=$" means; however, it doesn't understand what "$\in$" is supposed to mean until we add some axioms.

Improve this answer
$\endgroup$
  • $\begingroup$ What kind of graphs then does the set theory permit? I guess that they have to be like infinite chains possibly with branching. $\endgroup$ – Atom Jul 26 '20 at 19:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.