I am confused by the proof of Lemma 2.15 in Mendelson. The proof is a bit long, but here's what's happening in the confusing part for me:
- Given a theory $K$, let $(S_0),...,(S_{n-1})$ be wffs in a proof that ends with a wff $F_n(b)$, so that $\vdash_K F_n(b)$, where $b$ is a new constant that does not occur in $(S_0),...,(S_{n-1})$. Each $S_k$ for $k=0$ to $k=n$ has the following form:
$$ (S_k):=(\exists x_k) \neg F_k(x_k) \rightarrow \neg F_k(b_k) $$
From $\vdash_K F_n(b)$, we have $\vdash_K F_n(x)$, where $x$ is a new variable, i.e. $F_n(x)$ is derived from $F_n(b)$ by replacing all occurences of $b$ in the proof with $x$.
From $\vdash_K F_n(x)$, we have $\vdash_K (\forall x) F_n(x)$ using universal generalization.
The rest of the proof then continues from here ...
I am unsure about step 3 above. Shouldn't this be $(\forall x)(\exists x)F_n(x)$ ?, i.e. it looks like that we applied universal generalization to $x$, where $x$ is a substitute for a constant $b$
... What am I missing here ?