This is from "Introduction to Mathematical Logic" by Elliot Mendelson , forth edition , page 75.
There is this paragraph about the extension of proposition 2.4-2.7.
In Propositions 2.4-2.7, the following additional conclusion can be drawn
from the proofs. The new proof of $\Gamma \vdash \mathscr B \to \mathscr C$ (in Proposition 2.4 $\Gamma \vdash \mathscr C$ )
involves an application of Gen to a wf depending upon a wf $\mathscr E$ of $\Gamma$ only if
there is an application of Gen in the given proof of $\Gamma, \mathscr B \vdash \mathscr C$ that involves
the same quantified variable and is applied to a wf that depends upon $\mathscr E$. (In
the proof of Proposition 2.5, one should observe that $\mathscr D_j$ depends upon a
premiss $\mathscr E$ of $\Gamma$ in the original proof if and only if $\mathscr B \to \mathscr D_j$ depends upon $\mathscr E$
in the new proof.)
This supplementary conclusion will be useful when we wish to apply the
deduction theorem several times in a row to a given deduction.
Edit:If someone wants to see my attempt in understanding this paragraph then check this post of mine My Attempt.
Edit:I think I now understand this paragraph fully.What I missed is that The extension of 2.4-2.7 is actually a exercise that I have to prove . It is exercise 2.29 in page 76 of the book.I have had a second attempt of proving exercise 2.29 but I am not sure if it is correct.It is similar to the first attempt except their are some modifications of the proof of lemma 1.If someone knows a proof of exercise 2.29,please let me know.
Best Answer
Context: as explained in page 70, in Mendelson's system the "propositional" Deduction Theorem does not holds for predicate calculus.
Thus, the author's approach is to "minimize" the additional restrictions needed in order to prove the DT for predicate calculus: the usual alternative approach is (see Coroll.2.7) to assume that there are no free variable in $\mathscr B$.
Having said that, we have to note that the DT is a meta-theorem i.e. a recipe that, given a derivation of e.g. $\mathscr B \vdash \mathscr C$, allows us - under suitbale conditions - to produce a new derivation $\vdash \mathscr B \to \mathscr C$.
Assuming that you have understood the concept of "dependency" in a derivation (in a nutshell: to keep track of the assumptions effectively used in a step of the derivation), what about:
It means that, the "dependencies" in the original derivation $\Gamma, \mathscr B \vdash \mathscr C$ have generated similar dependencies in the new derivations $\Gamma \vdash \mathscr B \to \mathscr C$ (case Prop.2.5) andr $\Gamma \vdash \mathscr C$ (case Prop.2.4).
The proof of the DT (compare with the propositional version) amounts to a "procedure" for changing every step $\mathscr D_i$ in the derivation in a new step $\mathscr B \to \mathscr D_i$.
The gist of the inductive proof is to show that this move is sound, and this needs to check all the possible cases.
The critical point in the predicate calculus case is to circumvent the unsound $Px \to \forall x Px$; in order to do so, the "dependency" concept has been introduced in order to restrict the use of Gen (as said above, if there are no free variables in $\mathscr B$, of course we have no risk of misusing the rule).
In the repeated application of the DT, what is important is that if there were a dependency of the conclusion $\mathscr C$ from $\mathscr D$ and $\mathscr B$ isn the original derivation $\Gamma, \mathscr D, \mathscr B \vdash \mathscr C$, there will be a similar dependency of the conclusion $\mathscr B \to \mathscr C$ from premise $\mathscr D$ in the new proof $\Gamma, \mathscr D \vdash \mathscr B \to \mathscr C$.
A very simple example can be manufactured using first-order arithmetic: call $\mathsf {PA}$ the collection of (first-order) Peano axioms.
In Mendelson's system, from the correct (two lines) derivation: $\mathsf {PA}, x=0 \vdash \forall x (x=0)$ we cannot use DT to produce the incorrect $\mathsf {PA} \vdash x=0 \to \forall x (x=0)$, simply because in the step deriving $\forall x (x=0)$ from premise $x=0$ we have to apply Gen to the wf $x=0$ that depends upon itself and has as its quantified variable the free variable of $x=0$ (see page 70).