In the book The Foundations of Mathematics by Kenneth Kunen, in a chapter about set theory formalizations, the following first order logic sentence is provided (referred to as the Axiom of Comprehension/Separation Schema):
$\forall z \Big (\exists y \color{red}{\forall x} \big ( \color{red}{x} \in y \leftrightarrow x \in z \land \varphi(\color{red}{x}) \big ) \Big )$. I have colored in $\color{red}{\text{red}}$ the variable that I will be focusing on for the remainder of this question.
Consider the following two sets:
$A = \{ x \in \mathbb N \ |\ x \lt 5\}$.
$B = \{ \langle s, t \rangle \in \mathbb N \times \mathbb N \ |\ s \lt 5 \land t\lt 4 \}$
Now, let's say I wanted to look at set $A$ and confirm that it exists through the perspective of the Axiom of Comprehension Schema:
$\exists y \forall x (x \in y \ \leftrightarrow \ x \in \mathbb N \land x \lt 5)$ where $\varphi(x):= x \lt 5$. Cool. Set A exists.
To confirm set $B$'s existence, however, I run into an issue when it comes to inserting the predicate $\varphi$:
$\exists y \forall x (x \in y \ \leftrightarrow \ x \in \mathbb N \times \mathbb N \ \land \text{something} )$
I use the phrase "$\text {something}$" because "$\varphi (x)$" does not appear to decompose correctly into a statement about two variables…i.e. $\varphi(x)$ cannot be used to represent "$s \lt 5 \land t \lt 4$" because $s$ and $t$ are not necessarily equal, and therefore do not represent one object $x$.
A quick fix seems to be to switch $\forall x$ with $\forall s \forall t$ in order to generate the following statement:
$\exists y \forall s \forall t (\langle s,t \rangle \in y \ \leftrightarrow \ \langle s,t \rangle \in \mathbb N \times \mathbb N \ \land s \lt 5 \land t \lt 4 )$
I am uncertain why this is something that is allowed. Specifically, this seems to suggest that $\forall x \ \varphi(x)$ is 'semantically' (regular English definition) equivalent to $\forall s \forall t \ \varphi (s,t)$.
From what I understand about first order logic, $\forall x \ \varphi (x)$ essentially means "For all singular objects in the domain of discourse, the following sentence about a singular object is true". Comparatively, I interpret $\forall s \forall t \ \varphi(s,t)$ as saying "For any two objects in the domain of discourse, the following sentence is true about two objects".
Is the syntax "$\ s,t\ $" a singular object in the domain of discourse? It doesn't strike me as one…hence my confusion.
Any input is greatly appreciated! Thank you.
Best Answer
You use the projection functions - or rather, the projection relations. These are the binary relations $\pi_0(x,y)$ and $\pi_1(x,y)$, which we read as "$x$ is an ordered pair with left coordinate $y$" and "$x$ is an ordered pair with right coordinate $y$." Note that the expression "$u=\langle v,w\rangle$" is really shorthand for "$\pi_0(u,v)\wedge\pi_1(u,w)$."
Writing out the projection relations in terms of $\in$ alone is a good exercise. Once you've done this, you can produce $B$ by applying Separation to the formula
$$\varphi(x)\equiv \forall s,t(\pi_0(x,s)\wedge \pi_1(x,t)\rightarrow s<5\wedge t<4).$$
Separation applied to this formula, with "container set" $z=\mathbb{N}\times \mathbb{N}$, says that there is a set $B$ consisting of exactly those $a$ which are elements of $z$ and which satisfy $\varphi$ - and this $B$ is precisely what we want.