I am trying to understand the axioms of ZFC. The axiom schema of specification or the comprehension axioms says:
If A is a set and $\phi(x)$ formalizes a property of sets then there exists a set C whose elements are the elements of A with this property.
I read Is the Subset Axiom Schema in ZF necessary? and understand that ZFC axioms are defined in the language first-order logic. I do not understand the part 'phi(x) formalizes a property of sets'. If we allowed any property, e.g. $\phi(x) = x \notin x$, then we would get a Russell's paradox. But saying any property except $\phi(x) = x \notin x$ would not eliminate all the paradoxes. Thus we have to have some way to say which properties $\phi(x)$ do not make ZFC inconsistent.
Is my understanding correct? What does it mean to 'formalize a property of a set'? How do we know that a property $\phi(x)$ does not make ZFC inconsistent?
To formalize a property of a set simply means to give a formula in the language of set theory. That is $\phi(x)$ is nothing but a formula in the language.
Now, for each such property of sets $\phi(x)$ there is an axiom that says that given any set $A$ the set $\{x\in A\mid \phi(x)\}$ exists. This is the axiom schema of specification. Russele's Paradox does not creep in here since you still can't form the set $\{x\mid x\notin x\}$ not since you can't formulate the property $\phi(x)=x\notin x$ (you certainly can) but simply since using the axiom schema of specification will only allow you to create such sets as $\{x\in A\mid x\notin x \}$. By the axiom of foundation this set is just $A$.