# Can one formally introduce set-builder notation in ZFC?

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?

• Apparently not well enough. Sorry. Oct 8, 2016 at 22:58
• @Arthur: I ask if it's possible to add an expression like $\{x\in A\mid \phi(x)\}$ to the formal syntax of ZFC, like one can add $\subseteq$ and $\cup$ and $\emptyset$ to the formal syntax. My the question is a bit stupid and naive, but in the best case, there is something to learn :-) Oct 8, 2016 at 22:59
• I never really caught on to much of the intuition in the strictest mathematical logic, but it seems to me like $\phi$ is a hurdle. That's the reason comprehension and replacement are not axioms, but axiom schemata. You could make a scheme for set builder notation, I guess. Or I might be out of my depth. Oct 8, 2016 at 23:04
• For anyone else who comes across this post, the formal way to do it is via definitorial expansion. This is the rigorous way of supporting so-called set-builder notation (which is essentially a constant-symbol witnessing existential statements) as well as $\cup$ (a binary function-symbol) and $\subseteq$ (a binary predicate-symbol). Note that the latter two are not represented by any objects (sets) in ZFC. Apr 13, 2017 at 16:08
• @user21820: I gave an answer below to your question along the lines of definitorial expansion, but before reading your comment. You’re right. The set-builder notation applied to a given formula with one free variable can be interpreted as a new unary function symbol to be added to the language of set theory. Oct 12, 2017 at 1:19

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$.

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))$.

• Thanks. Seems like definite descriptions are the perfect answer how to formalize set-builder notation in ZFC. Oct 9, 2016 at 11:52

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.