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?

  • $\begingroup$ Apparently not well enough. Sorry. $\endgroup$ – Arthur Oct 8 '16 at 22:58
  • $\begingroup$ @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 :-) $\endgroup$ – user376483 Oct 8 '16 at 22:59
  • $\begingroup$ 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. $\endgroup$ – Arthur Oct 8 '16 at 23:04
  • $\begingroup$ 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. $\endgroup$ – user21820 Apr 13 '17 at 16:08
  • $\begingroup$ @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. $\endgroup$ – Transcendental Oct 12 '17 at 1:19

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

  • $\begingroup$ Thanks. Seems like definite descriptions are the perfect answer how to formalize set-builder notation in ZFC. $\endgroup$ – user376483 Oct 9 '16 at 11:52

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


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.