ZFC, set membership and FOL Hi,
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...
Thanks
 A: 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. 
A: 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.
A: 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.
