Can one formally introduce set-builder notation in ZFC?

Question

If one is completely formal, then one can formulate ZFC as a set of first-order formulas over the signature $L=\{\in\}$ consisting only of one binary relation $\in$. Then one can state the usual ZFC axioms in this formal language.

I recently learned about the concept of Extension by definition. The main idea is this: in practice, we are not working in a language only consisting of $\in$, but we are constantly introducing new symbols! For example, we observe first that there is a unique set that has no elements at all, and this justifies that we can give this unique set a special symbol – we choose $\emptyset$ for that. Similarly, one can introduce a symbol $\mathbb N$ for the natural numbers. But the same concept also works when we introduce new function and relation symbols: for instance, we can define the operation $\cup$ through proving that for each A, B, there is a unique set $A\cup B$ with the property $\forall x(x\in A\cup B\iff x\in A\lor x\in B)$ (after proving that this is unique when given two sets A, B); also one can define a relation $\subseteq$ by setting $A\subseteq B:\Leftrightarrow \forall x(x\in A\implies x\in B)$.

For a formal definition of this concept of "extension by definition" see the linked wikipedia article. I wonder:

Can one similarly introduce a set-builder notation to the formal language of set theory? I have something like this in mind: given a set symbol $A$ and a formula $\phi(x)$ with one free variable, one can define the set $\{x\in A: \phi(x)\}$ to be the unique set of all elements of A that satisfy the property $\phi$. Is this just human notation or can this be made precise similar to the concept of extension by definition?

Answer 1

Here is an approach that does not employ Russell’s description operator $ \iota $.

---

Given a first-order formula $ \varphi $ with one free variable $ z $ in the language of set theory ($ \mathsf{LOST} $), you can add (i) a new unary function symbol $ F_{\varphi} $ to $ \mathsf{LOST} $ and (ii) the following new axiom to $ \mathsf{ZF} $: $$ (\forall x)(\forall y) (y = {F_{\varphi}}(x) \iff (\forall z)(z \in y \iff (z \in x \land \varphi))). \qquad (\star) $$ By the well-known technique of Extension by Definitions in first-order logic, these additions yield a conservative extension of $ \mathsf{ZF} $ because on one hand, the Axiom Schema of Specification ensures that $$ (\forall x)(\exists y)(\forall z)(z \in y \iff (z \in x \land \varphi)), $$ and on the other hand, the Axiom of Extensionality ensures that $$ (\forall x)(\exists! y)(\forall z)(z \in y \iff (z \in x \land \varphi)). $$ You may therefore think of $ F_{\varphi} $ as a formalized version of the set-builder notation applied to $ \varphi $.

Answer 2

The set-builder notation is a "term-forming" operator, i.e. a symbol that with "input" a formula produce as "output" a term, like Russell's $\iota$ for definite descriptions.

In order to "enlarge" the language with $\iota$, we have to :

1) prove : $(∃!z)Q (z, x_1, \ldots, x_n)$

2) add the axiom : $y = (\iota z)Q (z, x_1, \ldots, x_n) ↔ Q (y, x_1, \ldots, x_n)$.

In the same way, in set theory, we have to prove :

$(∃!z)(∀x)(x ∈ z ↔ \varphi(x))$

and then add the axiom :

$\{ x : \varphi(x) \} = (\iota z) (∀x)(x ∈ z ↔ \varphi(x))$.

Answer 3

Yes, the names in the development of forcing can be viewed like that, and the definition of the constructible universe $L$ can be phrased this way as well.

I recall seeing a backwards-K symbol used to denote formal terms that were essentially variant set-builder terms.