Is set membership defined in the signature of ZFC, or is it *specified" in the signature of ZFC? The wikipedia article http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory says that the signature has set membership, but what does it mean by has?

If I understand correctly, the axioms specify the properties of set membership. Given set membership, how come ZFC can be foramlised in FOL when some axioms, e.g., axiom of infinity, require quantification of sets? Aren't sets unary predicates since S(a) = True iff a is a member of S? Quantification over unary predicates is a feature of second-order though.

I must be missing something...


  • $\begingroup$ Internal sets in ZFC are just elements in a model of ZFC. They're not subsets of the model (although they can contain all of the elements in a subset of the model). $\endgroup$ – Qiaochu Yuan Aug 12 '11 at 3:25
  • 2
    $\begingroup$ If you look at the article you'll see that ZFC is a one sorted theory in FOL, where sets are the individuals in the universe. Hence variables range only over sets, and set membership is a binary relation in the signature. Axiom of infinity and all axioms quantifying over sets are thus expressed in FOL. $\endgroup$ – godelian Aug 12 '11 at 3:38
  • $\begingroup$ This question should be community wiki or asked at mathstockexchange. $\endgroup$ – SNd Aug 12 '11 at 15:29

A specification is a prescription of how things are supposed to be. A model (or implementation in computer-sciency talk) is an instance of something that satisfies a specification.

In first-order logic and model theory a specification is called a theory, and it consists of two parts:

  • a signature which prescribes the non-logical part of the language (constants, function symbols, and relation symbols)

  • axioms, which are first-order statements written in the language that includes the parts provided by the signature

The division of a theory into two parts is convenient, but is not always possible outside first-order logic. For example, if we wanted to include Russell's definite operator $\iota x . \phi(x)$ ("the $x$ such that $\phi(x)$") then our syntax would get intertwined with logic because in order to even form the term $\iota x . \phi(x)$ one first has to prove something.

Anyhow, the theory ZFC specifies that there is one relation symbol $\in$, which we usually read as "element of". A model of ZFC interprets the symbol $\in$ as a binary relation, so in this sense it defines its meaning.

In a context where theory and its intended semantics are bunched together, such as the Wikipedia page seems to be, the distinction between the specification and implementation will be obsucred. In fact, most mathematicians seem to be a bit unclear about this distinction, as they never really have to distinguish the language they use from its meaning.

  • $\begingroup$ I think most mathematicians are clear about the distinction up to algebraic theories: they know the difference between a group and the theory of groups. It's when you add quantifiers/binders and implication/negation that they get fuzzy, since for some reason we are rarely taught the deductive systems we actually use. (I remember when I finally realized that dependent records gave a syntax for indexed sets -- embarrassingly, this was a couple of years after I learned about dependent types!) $\endgroup$ – Neel Krishnaswami Aug 12 '11 at 9:55
  • $\begingroup$ Just to get my terminology right: If I understand correctly, a theory specifies a symbol in its signature and defines the symbol's properties in its axioms -- is that right? $\endgroup$ – Kar Aug 12 '11 at 12:21
  • $\begingroup$ @kate: Essentially, yes, but note that axioms can describe combined properties of symbols, such as distributivity of $\cdot$ over $+$, and sometimes symbols are not mentioned in the axioms at all (for example, uninterpreted constants). $\endgroup$ – Andrej Bauer Aug 13 '11 at 11:46
  • $\begingroup$ Just to be clear, when I write "\A x (x \in S -> ...)" in FOL, "x \in S" is presumably interpreted as if it were a literal s(x) where the interpretation of s is the set that I had in mind for S? $\endgroup$ – N.S. Feb 24 at 17:15
  • $\begingroup$ That is not correct. Sets are the individuals about which set theory speaks. They are not to be equated with predicates (which leads to the paradoxes of naive set theory). $\endgroup$ – Andrej Bauer Feb 24 at 17:25

Properly speaking, the signature of ZFC includes a binary relation symbol rather than a binary relation. In set theory this symbol is usually denoted $\in$ but it could be denoted equally well as $R$ or $\prec$. In an arbitrary model of set theory, the "sets" might actually be any objects: cats, books, chairs, etc. But if we're are only interested in the elements qua elements of that model, we would likely call them "sets" anyway, and call the relation "membership", in the context of that model.

It is very common, when talking about a first-order theory, to conflate the symbols in the theory with their intended interpretations. For example, when we define Peano arithmetic in the signature of ordered rings, we might say that the signature has a single binary addition function $+$. Of course we already know what the "addition" function is on natural numbers, but the interpretation of the $+$ function in an arbitrary model of PA may have very little to do with addition on natural numbers. Nevertheless we usually call the elements of an arbitrary model of PA the "numbers" of the model, and we call the interpretation of the $+$ symbol the "addition" on those numbers. It's simply too cumbersome to say "The objects in the model which are intended to be numbers" or "the function in the model which is intended to be addition".

Similarly, even though the elements of an arbitrary model of ZFC might not "really" be sets, or the interpretation of the $\in$ symbol may not really be set membership, we often speak as if they are. The key observation is that, if someone "lived inside" the model, and only had access to the $\in$ relation, that person would have no way to tell that the things they see are not sets. One way of making this observation precise is the following lemma, which is proved from "outside" a model $(X, R)$ of set theory.

Mostowski Collapsing Lemma. Suppose that $R$ is a binary relation in an arbitrary class $X$ (of arbitrary objects) such that:

  • For each $y \in X$, the collection $\{ x \in X : xRy\}$ is a set
  • The model $(X,R)$ is well founded – every subset of $X$ has an $R$-minimal element
  • The model $(X,R)$ satisfies the axiom of extensionality

Then there is a transitive class $C$ (of sets) such that the structure $(C, \in)$ is isomorphic to $(X, R)$, and both $C$ and the isomorphism are uniquely determined by $X$ and $R$.

This lemma says that if we look from the outside at a model that looks even vaguely like a (well-founded) model of ZFC, we can replace it with an isomorphic model whose elements are actually sets and whose binary relation is actually set membership. This doesn't work formally for non-well-founded models, because the actual set membership relation is well founded. But "from the inside" we wont be able to tell that any model of ZFC is not well founded.

  • $\begingroup$ Mostowski, right? Gerhard "Ask Me About System Design" Paseman, 2011.08.12 $\endgroup$ – Gerhard Paseman Aug 12 '11 at 19:27
  • $\begingroup$ Two small comments. 1.- It would moreover be considered improper to use + for a noncommutative operation - this is another place where the syntax 'implies' some semantics. 2.- An interesting case in point is that structures of the form $(A,\prec)$ where $\prec$ is a linear ordering of $A$ tend to satisfy an insanely large fragment of ZFC. $\endgroup$ – François G. Dorais Aug 13 '11 at 0:37

The axioms of ZFC describe the properties of set membership. The unary predicates that you talk about are not a priori set, but what we call classes. It happens that certain classes coincide with certain sets, namely when the members of the set are precisely the sets that satisfy the predicate.

In the language of set theory you can quantify over set, as these are the objects that this language talks about, but not over classes, the unary predicates.

The usual reason for confusion that arises in the context of set theory is the fact that when doing math, we already use the relation $\in$ to talk about the things that we are studying. When talking about a structure for a first order language, we talk about a set with certain relations, functions, and constants. When considering a model of ZFC we need to be really careful: There are the things that we consider as sets in the "real world", i.e., the universe of sets in which we do mathematics (and which we assume to satisfy ZFC), and then there is a model of ZFC, let's call it $M$, which is itself a set in the universe of sets and which carries a binary relation $E$ such that $(M,E)$ satisfies ZFC.

Now, from the perspective of $M$, the elements of $M$ are the sets, and they are related to each other by $E$. $E$ does not have to be the real $\in$, even though it can be. The classes of $M$ are subsets of $M$ in the "universe of all sets"-way, but they are not known to $M$. There are some subsets $A$ of $M$ such that there is $a\in M$ with $\{b\in M:b E a\}=A$. If $A$ is a class of $M$, i.e., the collection of elements of $M$ satisfying a certain unary predicate, we identify this class with the "set" $a$ (set in the sense of $M$). But not all classes of $M$ can be identified with sets of $M$ in this way, for example all of $M$ or the class of all ordinals of $M$.

I hope this helps.

  • $\begingroup$ Very clearly, it is specified in the signature, at least where I come from. $\endgroup$ – Andrej Bauer Aug 12 '11 at 7:20
  • $\begingroup$ In the signature it is specified that there is a binary relation, which we happen to call set membership. But nothing about its properties is said. This is what the axioms are for. But you are right, of course, this is just a matter of terminology. $\endgroup$ – Stefan Geschke Aug 12 '11 at 7:25

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.