# Translating Set-Builder Notation to Predicate Logic

I am struggling to understand how one converts a set written using the set-builder notation to elementary predicate logic. Just for you to have an idea of my background, I studied engineering in college, and I used "high-level" maths (high level in the informatics sense, i.e. without digging to deep in the meaning of what I was writing) and I decided to start learning about ZFC for its own sake. I have no trouble understanding and manipulating sets written using predicate logic, but whenever a set-builder notation pops, I become lost because I am unable to go back to pure logic.

For simple cases such as $S = \{x|x\in A\}$, I clearly understand that it can be translated to ${\forall x(x \in S \leftrightarrow x \in A)}$.

I really started to realize that I did not understood this notation when solving an exercise involving $\{dom R | R \in A\}$. The mistake I made was that I was translating $x\in\{dom R | R \in A\}$ by $\exists y (x,y)\in R$ which is obviously wrong since $x$ should be a domain and not an element of a domain.

Although I am not sure of this, I would expect the solution to be something like $x=dom R \wedge R \in A$.

After this long introduction, my question is pretty simple: how do I turn ANY set written using the set-builder notation, even a complicated one, to a predicate logic formula?

• It is not propositional logic; it is predicate logic. – Mauro ALLEGRANZA Feb 28 '18 at 15:24
• My bad, I will edit this. I am not totally awake yet ^^ – lesibius Feb 28 '18 at 15:25
• In general, the set-builder notation syntax is: $S = \{ x \mid \varphi(x) \}$. Thus, we have: $a \in S \leftrightarrow \varphi(a)$. – Mauro ALLEGRANZA Feb 28 '18 at 15:25
• $\text {dom}(R)$ is a set: thus, the expression $\{ \text {dom}(R) \mid R \in A \}$ is alittle bit "weird". – Mauro ALLEGRANZA Feb 28 '18 at 15:30
• Having said that: $x \in \text {dom}(R) ↔ \exists z \in R \ \exists y \ z=(x,y)$. – Mauro ALLEGRANZA Feb 28 '18 at 15:33

Example: Consider the following sentence: Let $R \in \mathbb{N} \times \mathbb{N}$, let $n \in \mathbb{N}$, let $M = \{z^n \mid \forall w. (z,w) \in R\}$. The variable $w$ is bound by the explicit quantifier within the set-builder notation, the variables $R$, $n$, and $z$ occur freely within the set-builder notation, but $R$ and $n$ are bound outside of the set-builder notation (by the phrase "Let $R \in \mathbb{N} \times \mathbb{N}$, let $n \in \mathbb{N}$"). The usual convention is that all free variables within the set-builder notation that are not bound outside are considered as existentially quantified. In this example, that's $z$, so we get $$x \in M \Leftrightarrow \exists z. (x = z^n \land \forall w. (z,w) \in R).$$
In the general case, we have a formula $$M = \{t(y_1,\dots,y_n,z_1,\dots,z_m) \mid \varphi(y_1,\dots,y_n,z_1,\dots,z_m)\},$$ where $t(y_1,\dots,y_n,z_1,\dots,z_m)$ is a term depending on $y_1,\dots,y_n,z_1,\dots,z_m$ and $\varphi(y_1,\dots,y_n,z_1,\dots,z_m)$ is a formula with free variables $y_1,\dots,y_n,z_1,\dots,z_m$ (and possibly further variables bound within $\varphi$). If the variables $y_1,\dots,y_n$ are bound outside of the set-builder notation, then $$x \in M \Leftrightarrow \exists z_1 \dots \exists z_m. (x = t(y_1,\dots,y_n,z_1,\dots,z_m) \land \varphi(y_1,\dots,y_n,z_1,\dots,z_m)).$$