0
$\begingroup$

In set theory, the notions of set and membership are considered primitive. We only specify some of the properties that we think our primitive notions have using the axioms.

Usually, the very first axiom of set theory is the axiom of extensionality which specifies that two sets are equal if and only if they have the same members. My discomfort with specifying this axiom as the first is that we haven't said anything about how the notion of membership relates to the notion of set in any previous axiom. That is we haven't specified that it makes sense to say something is a member of a set. Yet we use this notion in the axiom of extensionality.

Why we don't have an axiom that exclusively talks about the membership of things in a set?

$\endgroup$
1
  • $\begingroup$ We make sense of elementhood, using the rules of well formed formula; rather than an Axiom. Of course, You can consider such rules of well formed formula, as axioms being caried over from Pure Logic. $\endgroup$ Commented Oct 10, 2023 at 17:32

1 Answer 1

7
$\begingroup$

ZF is built on first-order logic with equality and a single nonlogical binary relation symbol $\in.$ This tells you that the membership relation makes sense globally, i.e. $a\in b$ is a meaningful statement between any two objects $a$ and $b$ in the domain of discourse. This gels with the basic philosophy of ZF that "everything is a set".

So we don't need an axiom to tell us when the membership relation is well-formed... it's established by the background logic that the answer is 'always'.

If we want to move away from ZF and include objects other than the empty set that don't have members (i.e. urelements) one way would be to add a sort to the language and then say $x\in y$ is not well-formed when $y$ is of that sort. Similarly, if we want to add proper classes (which can't be elements of sets or classes) then we could have a sort for that and say $x\in y$ is not well-formed when $x$ is of that sort.

We could also handle it at the non-logical level, and include (e.g. in the case where we have proper classes but no urelements) a predicate $\operatorname{Set}(x):= \exists y \;x\in y$ in order to identify when an object in the (single-sorted) domain is a set.

But we don't need to do any of this in ZF, when we're in the simple situation where everything is a set.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .