My understanding of set-builder notation is that given a set $A$ and a function $P:A\to\{true,false\}$, one can define the subset $$ B=\{a\in A:P(a)\} . $$ However, a function $f:A\to C$ is defined as a special kind of subset of the product set $$ A\times C= \{(a,c):a\in A,\,c\in C\}. $$ I was wondering if there is any circularity here, since we are using the set-builder notation to define the Cartesian product of two sets. I also imagine that in order to define the set of functions from $A$ to $C$ one needs to use set-builder notation.

  • 3
    $\begingroup$ Generally, we work with a formula in some formal logic rather than with a function $P : A \to \{\text{true}, \text{false}\}$. We can define formulae in a recursive fashion without needing to define set-builder notation, avoiding this problem. $\endgroup$
    – qaphla
    Commented Jun 5, 2016 at 2:21
  • $\begingroup$ @qaphla: Thanks a lot! Are you saying that some preliminary version of the set-builder notation must be defined before defining the full notation? $\endgroup$
    – timur
    Commented Jun 5, 2016 at 2:33
  • 1
    $\begingroup$ Usually, the set-builder notation is an abbreviation; thus, it is part of the syntax. $\endgroup$ Commented Jun 5, 2016 at 12:17
  • 2
    $\begingroup$ MO copy of the question: mathoverflow.net/questions/241517/set-builder-formula $\endgroup$ Commented Jun 6, 2016 at 4:18
  • 1
    $\begingroup$ @timur - no, I'm not saying that. We introduce it as an abbreviation to "name": the set of those $x$ such that $\varphi(x)$ holds of them, provided that that set exists. $\endgroup$ Commented Jun 6, 2016 at 5:54

1 Answer 1


In axiomatic set theory, what you described as set-builder notation corresponds to axiom schema of specification (also called axiom schema of separation).

As already said in the comments, $P(a)$ in this axiom schema does not stand for function but for a formula in the language of set theory.

Axiom schema of replacement is related to the notion of function.

In fact, if you want to define Cartesian product in axiomatic set theory you

  • Use Kuratowski definition of ordered pair, i.e., $(a,b)=\{\{a\},\{a,b\}\}$. It can be shown that for any $a$, $b$ the ordered pair $(a,b)$ exists; that $(a,b)=(a',b')$ iff $a=a'$ and $b=b'$; that $(a,b)\in\mathcal P(\mathcal P(A\cup B))$ if $a\in A$ and $b\in B$.
  • Then you can define $$A\times B = \{x\in \mathcal P(\mathcal P(A\cup B)); (\exists a\in A)(\exists b\in B) x=(a,b)\}.$$

This means that the Cartesian product is defined using axiom schema of separation (which is written using set-builder notation). And, as you rightly said, function is then defined as a subset of Cartesian product which has some additional properties.

If you want to see a formal definition of formula (as used in the ZFC), for example, it is described nicely in Encyclopedia of Mathematics. Basically, you have the following rules:

  1. For any variables $x$, $y$, the atomic formulas $x=y$ and $x\in y$ are formulas.
  2. If $\varphi$ and $\psi$ are formulas, then so are $\neg\varphi$, $\varphi\land\psi$, $\varphi\lor\psi$, $\varphi\Rightarrow\psi$ and $\varphi\Leftrightarrow\psi$.
  3. If $\varphi$ is formula, then so are $(\forall x) \varphi(x)$ and $(\exists x) \varphi(x)$.

Anything constructed by applying the above rules finitely many times is considered a formula. And nothing else is considered a formula.

So an example of a formula would be $$(\forall x) (x\in A \Rightarrow x\in B).$$ This formula corresponds to $A\subseteq B$.

  • 1
    $\begingroup$ Yes. You are allowed to use atomic formulae $x=y$ and $x\in y$ (where $x$ and $y$ are variables.) And you can combine them using logical connectives and quantifiers. $\endgroup$ Commented Jun 6, 2016 at 12:55
  • 1
    $\begingroup$ I don't think that you are allowed quantifiers in Boolean functions. For example, you want $A\subseteq B$ expressed as $(\forall x) (x\in A \Rightarrow x\in B)$ to be a formula. $\endgroup$ Commented Jun 6, 2016 at 12:58
  • 1
    $\begingroup$ If you want see formal definition of formula (as used in the ZFC), it should not be difficult to find some resources. For example, searching for ZFC language formula returns some reasonable hits. $\endgroup$ Commented Jun 6, 2016 at 13:00
  • 1
    $\begingroup$ @timur I have posted a more precise definition of formula in chat. (I did not want to post too many comments here.) If further clarifications are needed, we can continue our discussion there. $\endgroup$ Commented Jun 6, 2016 at 13:11
  • 1
    $\begingroup$ Thanks a lot! I took the liberty of editing your answer to include the discussion about formulas, in case other people find it useful. $\endgroup$
    – timur
    Commented Jun 6, 2016 at 13:49

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .