Definition of a property in ZF set theory

Question

The Axiom Shema of Comprehension in ZF set theory states that: Let P (x) be a property of x. For any A, there exists a B such that x∈B if and only if x∈A and P(x) holds. (https://www.math.uchicago.edu/~may/VIGRE/VIGRE2011/REUPapers/Lian.pdf) The paper does not state a definition for a property. How can we define a property in this set theory?

Answer 1

The author is speaking informally; the axiom scheme of comprehension, as well as that of replacement, has an axiom corresponding to each formula of first-order logic (that is, "property" is shorthand for "first-order formula with parameters"). This is identical to how the induction scheme works in (first-order) Peano arithmetic. You will find a better treatment in an actual textbook, e.g. Kunen.

---

To help understand this, here's what an instance of the comprehension scheme looks like. Let $\varphi(x, y_1, ..., y_n)$ be a first-order formula in $n+1$ variables ($n$ could be $0$). Then the corresponding instance of the comprehension scheme is $$\forall z, w_1, ..., w_n\exists u\forall x[x\in u\iff x\in z\wedge \varphi(x, w_1, ..., w_n)].$$ That is:

For any set $z$ and parameters $w_1, ..., w_n$, there is a set $u$ consisting of exactly those elements of $z$ which satisfy $\varphi(-, w_1, ..., w_n)$.

The fact that parameters are allowed here is very important (and things can get quite messy when we look at limiting the use of parameters!). As a concrete example, suppose $M$ is a model of ZFC and $a, b$ are in $M$. Then the comprehension scheme lets us prove that $$\{x: x\in a, x\not\in b\}$$ is in $M$ (or rather, if you want to be completely precise about it, the comprehension scheme tells us that there is an object $c$ in $M$ such that $M\models \forall x(x\in c\iff (x\in a\wedge x\not\in b)))$. In this case the instance of comprehension we use is that given by the formula $$\varphi(x, y_1)\equiv x\not\in y_1,$$ we take our parameter $w$ to be $b$, and we take our "outer set" to be $a$.