Universal generalization proof

Question

Assume $\Gamma$ is a set of formulas, $P(x)$ a formula, and $\Gamma\vdash P(c)$ has been derived.

The generalization rule states that $\Gamma \vdash \forall x\,P (x)$ can be derived if $c$ does not occur in $\Gamma$.

This is an intuitive rule, since if we can deduce $P(c)$ having no information about the constant $c$, that means $c$ could have any value, and therefore P would be true for any interpretation, that is $\forall x\,P (x)$.

However, I have tried to demonstrate this rule using first order logic, but I think it is impossible since there is no way to directly translate "c does not occur in $\Gamma$" in FOL as far as I know.

What logic system do I need to use in order to demonstrate this?

Where can I find a formal proof for this rule?

Answer 1

I don't know exactly what it should mean to 'demonstrate this rule using first order logic'. This is a rule of inference... it is part of the metatheory... it is a statement about first order logic, not in it.

There are a couple adjacent things that make sense.

1. One could prove that it is an admissible inference rule in a given system of first order logic. This would consist of proving that if a deduction of $P(c)$ exists from a $\Gamma$ where $c$ doesn't appear, then a deduction of $\forall x P(x)$ exists. Oftentimes universal generalization taken as a primitive rule, so this is trivial, but sometimes it is not. In any case one would need to know what the rules and axioms of the system are in order to produce such an argument.
2. One could prove that the rule is sound semantically, i.e. if $P(c)$ is a logical consequence of $\Gamma$, then $\forall xP(x)$ is as well. So let $M$ be an interpretation where $\Gamma$ holds and $y$ in the domain of $M.$ We will show $P(y)$ holds in $M.$ Consider the interpretation $M'$ which is the same as $M$ except $c$ is interpreted as $y$ instead of whatever $M$ had it as. Since $c$ does not appear in $\Gamma,$ $M'$ still satisfies $\Gamma,$ and so by assumption, $P(c)$ holds in $M',$ and thus so does $P(y).$ And $P(y)$ does not contain $c,$ so $P(y)$ holds in $M.$

Answer 2

If we are talking about Hilbert-style proof system, this rule is not an inference rule within the theory. A proof of "if $\Gamma \vdash P(c)$ then $\Gamma \vdash (\forall x)P(x)$" would be a meta-proof, i.e. a proof of the sentence about the first-order theory, but not a sentence in the theory.

So an informal proof is as follows. Since $\Gamma \vdash P(c)$, there exists a proof, i.e. a finite sequence of sentences each of which is either an axiom, or a sentence of $\Gamma$, or a sentence derived by inference rule of the theory. Now we pick a new variabe $y$ such that $y$ does not appear in the proof. This is possible because (1) the proof must be of a finite sequence, hence contains a finite number of variables; (2) in a first-order theory, there are infinitely (though countable) many variables. After we pick such a $y$, we replace $c$ by $y$ in the proof, yielding a new finite sequence of sentences. It is not difficult to verify that this new sequence is indeed a proof in the theory. That is, one has to verify that every sentence in this new sequence is either an axiom, or a sentence of $\Gamma$, or dervied by inference rules. Note $\Gamma$ does not contain the constant symbol $c$. So the above verification is possible. Finally, in this new proof, the last sentence must be $P(y)$. Now applying Gen rule, we can obtain $(\forall y)P(y)$. Deriving $(\forall x)P(x)$ from $(\forall y)P(y)$ is straightforward.

The above meta-proof is "informal" because it is stated in English. I think it is possible to formulate the above proof in a first-order set theory, although I'm not certeain. Nevertheless, I think it suffices to accept such an informal proof, just like other meta-proofs and meta-statements that discuss various properties about the subject-matter first-order theory, such as models, consistency, completeness, etc.