# A weird definition of $Φ((x)_0, \vec{z})$

On page 29, Constructibility, K.J.Devlin, I encounter a definition of $Φ((x)_0, \vec{z})$ (We use $\vec{z}$ to denote finite strings of variables)that baffles me:

Given an LST(language of set theory) formula $Φ(y, \vec{z})$, we denote by $Φ((x)_0, \vec{z})$ the LST-formula $$(\exists u \in x)(\exists a \in u)(\exists b \in u)[x = (a,b) \landΦ(a, \vec{z})]$$ Similarly for $Φ((x)_1, \vec{z})$.

$x = (a,b)=\{\{a\},\{a,b\}\}$, so let $u = \{a,b\}$, we will have $Φ((x)_0, \vec{z}) = Φ(a, \vec{z})$. I must misunderstand it somehow.

A following lemma that may be relevent:

If$Φ (x, \vec{z})$ is a $Σ_0$ formula of LST, then so too are $Φ((x)_0, \vec{z})$ .

What does $Φ((x)_0, \vec{z})$ really mean? What's the significance of such construction?

-
The $(\cdot)_0$ here is only notational. Devlin is saying that given $\Phi(y,\vec z)$, you can construct another formula $\Psi(x, \vec z)$, given by the formula you quote from the bottom of p. 29, which represents the application of $\Phi$ to $\vec z$ and the first element of the ordered pair $x$. However, to make things easier to read, he's decided to call this formula not $\Psi(\cdot,\cdot)$, but $\Phi((\cdot)_0,\cdot)$. It's an example of syntactic sugar. Since $\Psi$ is constructed from $\Phi$ using only bounded quantifiers, it is $\Sigma_0$ whenever $\Phi$ is.