Understanding the Deduction theorem

Question

Deduction theorem (First order predicate logic)

Suppose there exists a deduction $\Gamma,\phi\vdash\rho$ such that there is not generalized applications in formulas that depends on $\phi$ and also suppose that generalized variable it's a free variable of $\phi$. Then $\Gamma\vdash\phi\to\rho.$

My questions are:

What is the generalized variable?

Is the generalized variable any generalized variable such that doesn't depend on $\phi$? But if it doesn't depends on $\phi$ it can't be a free variable of $\phi$.

This is very confusing. Can someone explain this please?

Answer 1

Long comment

In a derivation $\Gamma \vdash \phi$, i.e. a sequence $D_1, D_2, \ldots, D_n$ where ... and $D_n= \phi$, we say that $D_i$ depends upon $B$ iff:

1. $D_i$ is $B$ and the justification for $D_i$ is that it belongs to $\Gamma$, or

2. $D_i$ is justified as a direct consequence by MP or Gen of some preceding formulas of the sequence, where at least one of these preceding formulas depends upon $B$.

With this definition in place, we have:

Deduction Theorem: Assume that, in some deduction showing that $Γ, \phi ⊢ \psi$, no application of Gen to a formula that depends upon $\phi$ has as its quantified variable a free variable of $\phi$. Then $Γ ⊢ \phi \to \psi$.

Thus, your "generalized variable" is a variable $x$ having free occurrences in $\phi$ and in the derivation there is some application of Gen to a formula that depends upon $\phi$ that quantifies $x$ (that "generalize" on it).