4
$\begingroup$

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?

Thanks in advance!

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

The tricky aspect of the set-builder notation is that it includes an implicit existential quantification for all variables that occur freely within the set formula and are not bound outside of the set formula.

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

$\endgroup$
  • $\begingroup$ Thanks for this answer, it is really helpful! $\endgroup$ – lesibius Feb 28 '18 at 16:30
  • $\begingroup$ @lesibius Feel free to upvote :-) $\endgroup$ – Uwe Feb 28 '18 at 16:47
  • $\begingroup$ I did but I do not have enough reputation yet for it to be recorded :-( With the incoming headaches related to my journey through ZFC, I expect that it will come soon ^^ $\endgroup$ – lesibius Feb 28 '18 at 17:10

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.