Universal generalization
The rule of universal generalization in FOL is stated as follows:
(Gen) From $p$ we may infer $(\forall x)p$ provided $x$ does not occur free in any premiss which has been used in the proof of $p$.
I don't understand what this means, particularly for deduction sequences. Given a set of formulae $S$ and a formula $p$ which has $x$ as a free variable, I can interpret the above in several ways. Suppose $(p_1,p_2,\ldots,p_n)$ is a deduction sequence of $S$ and $p_i = p$ for some $i$; then:
(Gen1) If $x$ does not occur free in $S$, then $(p_1,p_2,\ldots,p_n, (\forall x)p)$ is also a deduction sequence
(Gen2) If $x$ does not occur free in $p_j$ for all $j<i$, then $(p_1,p_2,\ldots,p_n, (\forall x)p)$ is also a deduction sequence.
(Gen2') If there is a deduction sequence $(p_1',\ldots,p_m' = p)$ that does not contain free occurrences of $x$, then $(p_1,p_2,\ldots,p_n, (\forall x)p)$ is also a deduction sequence.
[Say a deduction sequence $(p_1,\ldots, p_n)$ is $x$-independent if $x$ does not occur free in $\{p_j \mid p_j \in S\}$.]
(Gen3) If $(p_1,p_2,\ldots,p_{i-1})$ is $x$-independent then $(p_1,p_2,\ldots,p_n, (\forall x)p)$ is also a deduction sequence.
(Gen 3') If there is an $x$-independent deduction sequence $(p_1',\ldots,p_m' = p)$, then $(p_1,p_2,\ldots,p_n, (\forall x)p)$ is also a deduction sequence.
$\vdots$
I'm looking the most inclusive definition that results in a sound logical system. It must be easy to work with.
Example: the Deduction Theorem
For example, in the proof of the Deduction Theorem we start with a set of formulae $S$ and formulae $p,q$ so that $S\vdash (p\Rightarrow q)$; we seek to prove that $S\cup\{p\}\vdash q$. I would like to proceed as follows:
Write a deduction of $(p\Rightarrow q)$ from $S$, append $p$ and apply modus ponens to get a deduction of $q$ from $S\cup\{p\}$.
This doesn't quite work if (Gen1), say with a variable $x$, has been used in the deduction of $(p\Rightarrow q)$ and $x$ appears free in $p$, since then (Gen1) with variable $x$ is invalidated in $S\cup\{p\}$. So it appears (Gen1) is an inadequate definition (and I don't want to have to change the statement of the deduction theorem, as in here)
Qs: Which (Gen $k$) is correct, if any? Are some of them equivalent? What's the best/standard way(s) to define (Gen)?