Proof of Theorem: Explained

[evinda]

Hello! (Smile)

Theorem:

Let $\phi$ a type. We suppose that the set $Y$ exists, such that: $\forall x (\phi(x) \rightarrow x \in Y)$. Then there is the set $\{ x: \phi(x) \}$.

Proof:

From the Axiom schema of specification

("Let $\phi$ a type. For each set $A$, there is a set $B$, that consists of these elements of $A$, that satisfy the identity $\phi$, so:

$$ \exists B \forall x (x \in B \leftrightarrow x \in A \wedge \phi(x))$$

so: $B=\{ x: x \in A \wedge \phi(x) \}$ is a set.")

there is the set $Z=\{ x \in Y: \phi(x) \}$

$$x \in Z \leftrightarrow (x \in Y \wedge \phi(x) ) \leftrightarrow \phi(x)$$

Therefore:

$$Z=\{ x: \phi(x) \}$$

and so, $\{x: \phi(x) \}$ is a set.Could you explain me the proof of the theorem? (Worried) (Thinking)

 

[Evgeny.Makarov]

Intuitively, one is not allowed to form the set of all objects $x$ satisfying $\phi(x)$. One is, however, allowed to pick such objects (i.e., those that satisfy $\phi$) from a previously constructed set $A$, and call the result a set. That is, if you ask the set-robot: "Collect everything satisfying $\phi$", it will answer: "Sorry, can't do. Too much work. The search scope is undefined". But if you say, "Collect everything satisfying $\phi$ from the set continuum to the power continuum", the robot will say, "Here you are".

In your proof, all sets satisfying $\phi$ are already in $Y$, so if you collect all elements of $Y$ satisfying $\phi$ (which is allowed by the axiom schema of specification), you'll get the set of all sets satisfying $\phi$ at all, whether in $Y$ or not.

For more help, please write the specific place in the proof you don't understand and what you think about it.

 

[evinda]

Intuitively, one is not allowed to form the set of all objects $x$ satisfying $\phi(x)$. One is, however, allowed to pick such objects (i.e., those that satisfy $\phi$) from a previously constructed set $A$, and call the result a set. That is, if you ask the set-robot: "Collect everything satisfying $\phi$", it will answer: "Sorry, can't do. Too much work. The search scope is undefined". But if you say, "Collect everything satisfying $\phi$ from the set continuum to the power continuum", the robot will say, "Here you are".

In your proof, all sets satisfying $\phi$ are already in $Y$, so if you collect all elements of $Y$ satisfying $\phi$ (which is allowed by the axiom schema of specification), you'll get the set of all sets satisfying $\phi$ at all, whether in $Y$ or not.

For more help, please write the specific place in the proof you don't understand and what you think about it.

Axiom schema of specification:
"Let $\phi$ a type. For each set $A$, there is a set $B$, that consists of these elements of $A$, that satisfy the identity $\phi$, so:

$$ \exists B \forall x (x \in B \leftrightarrow x \in A \wedge \phi(x))$$

so: $B=\{ x: x \in A \wedge \phi(x) \}$ is a set."

We know that $\exists Y$, such that $\forall x(\phi(x) \rightarrow x \in Y)$

From the above theorem, $\exists$ a set $B$, that contains these elements of $Y$, that satisfy $\phi$, so:

$\exists B \forall (x \in B \leftrightarrow x \in Y \wedge \phi(x))$

so: $B=\{ x: x \in Y \wedge \phi(x) \}$ is a set.

But, why will we get then the set of all sets satisfying $\phi$ at all, whether in $Y$ or not, although it is:

$$x \in Z \leftrightarrow (x \in Y \wedge \phi(x))$$

? (Thinking)