TITLE: Reference on a corollary for applying Deduction Theorem multiple times in FOL.
QUESTION [1 upvotes]: This question is from "Introduction to Mathematical Logic" by Elliot Mendelson , forth edition , page 75.
In page 75 of the book , there is a corollary in a paragraph that can be used to apply the Deduction Theorem multiple times in a row.

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$.

But there seems to be no justification/proof about this corollary.I searched online but non of them seem to mention this corollary.Are there any references about this I can read or is it just too trivial?
Here is an failed attempt of mine for justifying this corollary.
1.Technique for applying deduction multiple times in Mendelson Logic.

REPLY [1 votes]: The gist of the proviso in the Deduction Theorem for predicate logic is to avoid the invalid step of quantifying a variable that is free in $B$, because $P(x) \to \forall x P(x)$ is not valid.
As already discussed, we have two derivations: the original one: $\Gamma, B \vdash C$ and the new one: $\Gamma \vdash B \to C$, and the DT gives us instructions how to produce the new one from the original one.
In the proof of Prop.2.5, we have to consider the case regarding the use of $\text {Gen}$ in the original derivation.
The text says:

Finally, suppose that there is some $j < i$ such that $D_i$ is $(\forall x_k)Dj$. By the inductive hypothesis, $\Gamma \vdash B \to D_j$, and, by the hypothesis of the theorem, either $D_j$ does not depend upon $B$ or $x_k$ is not a free variable of $B$.

The two sub-cases are considered and instructions are given for writing the corresponding steps in the new derivation.
In the first sub-case we have $\Gamma \vdash (\forall x_k)D_j$ by $\text {Gen}$. Thus, we have an application of $\text {Gen}$ in the new derivation, corresponding to the application of $\text {Gen}$ in the original one. The application is to $D_j$ that does not depend upon $B$ in the original derivation by induction hypotheses; thus, also the application in the new derivation is to a formula that does not depend upon $B$.
In the second sub-case we have $\Gamma \vdash (\forall x_k)(B \to D_j)$ by $\text {Gen}$, and we supposed that $x_k$ is not free in $B$.
In conclusion, in both sub-cases the applications of $\text {Gen}$ in the new derivation satisfy the condition:

no application of $\text{Gen}$ to a wf that depends upon $B$ has as its quantified variable a free variable of $B$ [in first sub-case: no dependency; in the second sub-case: $x_k$ not free in $B$].

But this means that if in the original derivation there were some application of $\text{Gen}$ to a wf depending upon a wf $E$ of $\Gamma$, then in the new derivation there is a corresponding application of $\text{Gen}$ that involves the same quantified variable and is applied to a wf that depends upon $E$.
This is so because applications of $\text {Gen}$ in the first derivation that are not involved in the derivation of $D_j$ are left unchanged into the new derivation and the new applications of $\text{Gen}$ discussed above generate no new dependencies.
{"set_name": "stack_exchange", "score": 1, "question_id": 4126521}