Let L be a language of first order logic. The generalization rule for universal quantifier says that, for $\phi\in L$, $\Sigma \vdash_L \forall x\phi(x) $ iff $\Sigma\vdash_{L\cup c}\phi([c/x])$, with c a new constant symbol. Suppose I have the following: $\phi([c/x])\vdash_{L\cup c}\sigma$, $\sigma \in L$. Because $\forall x\phi(x)\vdash_L \forall x\phi(x)$, applying the generalization rule, I have $\forall x\phi(x)\vdash_{L\cup c} \phi([c/x])$, and then, combining the two, $\forall x\phi(x)\vdash_{L\cup c}\sigma$. Now, can I say that $\forall x\phi(x)\vdash_L\sigma$ is also valid, given the fact that both in $\phi$ and $\sigma$ are in $L$? Or do I need the extended language to conduct the proof?
1 Answer
$\begingroup$
$\endgroup$
Your assumption amounts to $\exists x. \phi(x) \vdash \sigma$, so what you are asking amounts to whether $\forall x. \phi(x) \vdash \exists x. \phi(x)$ is derivable. The answer is no, unless you assume that the domain of discourse is inhabited ($\exists x. \top$), in which case it is a straightforward proof. This assumption is confusingly sometimes baked into presentations of classical first-order logic.
