Deduction Theorem: only works with closed formulas?
On wikipedia at https://en.wikipedia.org/wiki/Universal_generalization,
under Example of a proof, it is stated:
The Deduction theorem was applicable in steps [...] because the formulas being moved have no free variables.
I wasn't aware that this was a necessary assumption? It wasn't put to me that way in university; the version I had learnt was:
Let $\mathcal{L}$ be a first order language. Assume $\Sigma$ is a set of $\mathcal{L}$-formulas. Assume $X$ and $Y$ are $\mathcal{L}$-formulas. If $\Sigma \ \cup \{X\} \vdash Y$ then $\Sigma \vdash X \rightarrow Y$.
So, when it was put to me, there wasn't any stipulation that $X$ (or $Y$) must be closed. Wouldn't the theorem work fine if there were free variables?
Solution 1:
There are 2 common ways unquantified variables are meant to be interpreted in logic. The first way, which I'll call the dependency interpretation, is that $x > 7 \vdash x > 6$ is meant to be interpreted as
$$\forall x ~(x > 7 \vdash x > 6)$$
The $x$ represents the same variable in both statements, so it is showing a variable dependency. This is the intended interpretation for natural deduction and similar logics. The second way, which I'll call the tautology interpretation, is that $x > 7 \vdash x > 6$ is meant to be interpreted as
$$(\forall x~x > 7) \vdash (\forall x~x > 6)$$
This is the case for quantifier free logics like PRA, and more decisively it is the case for Hilbert's logic. These are logics wherein every asserted statement is meant to be a tautology. Whether you are working in one interpretation or the other depends on your rules of inference. If you are in a dependency interpretation, then there is no such restriction on the deduction theorem. If you are in a tautology in interpretation, then the restriction on the deduction theorem is necessary.
In a Hilbert's logic, you can prove something like $x = 1 \vdash x = 2$ :
$$\begin{array} {rl} x = 1 \\ \forall x,~ x = 1 & \forall3\\ (\forall x, x = 1) \to (2 = 1) & \forall1\\ 2 = 1 & \text{Modus Ponens} \\ 1 = 2 & \text{a=b is b=a rule} \\ x = 2 & \text{transitivity of =} \end{array}$$
This is fine because the interpretation $(\forall x ~x=1) \vdash (\forall x~x=2)$ is vaccuously true. But the claim $\vdash x=1 \to x=2$ isn't true at all in a sound tautology only logic. So the restriction on the deduction theorem is necessary.
In the wikipedia link, they seem to be working in a tautology only logic: notice this similarities to the justifications given and the linked Hilbert axioms. In step 8, they apply universal generalization without any consideration for whether the variable $y$ is present in assumptions. This absense of a restriction on ugen is what suggests they are using a tautology only logic, which is what imposes the restriction on the deduction theorem.