Step 2 of the completeness proof in Enderton's "Mathematical Introduction to Logic" (p. 136) reads:
"For each wwf $\phi$ (in the new language) and each variable $x$ we want to add to $\Gamma$ the wff $\neg\forall x\phi \to \phi[c/x]$ where $c$ is one of the new constants symbols. We can do this in such a way that $\Gamma$ together with the set $\theta$ of all the added wff is still a consistent set."
He continues by supplying the following detials:
Adopt a fixed enumeration of the pairs $\langle \phi, x\rangle$ where $\phi$ is a wff of the expanded language and $x$ is a variable: $\langle \phi_1,x_1\rangle, \langle \phi_2,x_2\rangle, ...$ This is possible since the language is countable. Let $\theta_1$ be $\neg\forall x_1\phi_1 \to \phi_1[c_1/x_1]$ where $c_1$ is the first of the new constant symbols not occurring in $\phi_1$. In general $\theta_n = \forall x_n \phi_n \to \phi_n[c_n/x_n]$ where $c_n$ is the first of the new constant symbols not occurring in $\phi_n$ or $\theta_k$ where $k < n$.
My question: How does this construction ensures that every formula $\phi$ in the expanded language in which only one variable occurs freely actually gets a witness?
More specifically, I am thinking that $\phi_1$ is simply the first formula by some enumeration. This means that $\phi_1$ could have $x_1$ free or not. It could be that $\phi_1$ has $x_2$ free. Say for instance $\phi_1 = P_1^1(x_2)$. Then, $\theta_1 = \forall x_1 \phi_1 \to \phi[c_1/x_1]$ would simply be $\theta_1 = \forall x_1 P_1^1(x_2) \to P_1^1(x_2)$. Since $\theta_2$ and all other $\theta_n$ are talking about different $\phi_i$ it seems to me that $\phi_1$ is left without witness in the overall construction. Why am I wrong? what am I missing?
