I am following the book Propositional and Predicate Calculus: A Model of Argument by Derek Goldrei, which includes a proof of the deduction theorem, first for propositional logic and then outlines a proof for predicate logic based on the proof for propositional logic. I do not see how (parts of) the proof for prop. logic works also for predicate logic.
The proof (for prop. logic) inductively shows that if $\Gamma, \phi \vdash \psi$ has a derivation $\psi_1,\dots,\psi_n = \psi$ under $\Gamma, \phi$, then we also have $\Gamma \vdash (\phi \rightarrow \psi_i)$ for $i = 1,\dots,n$. The inductive step involves "gluing" together different derivations to obtain the required derivation to complete the proof (see picture below for details).
The book later states that proving the deduction theorem for predicate calculus doesn't require much more and the prop. logic proof is most of the work required with an extended argument needed to cover Generalization as an inference rule.
Question: In predicate calculus, because of the Thinning Rule, $\Gamma \vdash \phi$ is defined by the book as there existing some $\Gamma_0 \subseteq \Gamma $ such that there exists a derivation (using certain Axioms, Modus Ponens and Generalization for variables not occurring free in any formula in the set of hypotheses) of $\phi$ under the hypotheses $\Gamma_0$. Because of this definition, how can we glue together two different derivations under $\Gamma$? What if one of the derivations involves Generalization which isn't valid unless one makes the set of hypotheses "smaller", i.e. work under $\Gamma_0$ rather than $\Gamma$.
I may be misunderstanding some definition here. If that is the case, please let me know. Thank you.
Inductive step in proof of deduction theorem for prop. logic:
See Goldrei's comment on the role of the thinning rule at page 223.
I think that there is no issue with it in the proof of the DT for predicate logic.
We have a derivation $Γ, \phi \vdash \psi$; due to the def of page 221, in it we have no use of Gen that quantifies a variable $x$ that is free in $\Gamma$ or $\phi$.
Thus, mimicking the propositional proof, in order to manage the step regarding the Gen rule we have to suppose that there is some $j < i$ such that $\psi_i$ is $∀x\psi_j$.
By the inductive hypotheses: $\Gamma \vdash \phi \to \psi_j$ and we know that $x$ is not a free variable of $\phi$, then, by axiom (A5), $(∀x(\phi → ψ_j) → (\phi → ∀xψ_j))$.
Since $Γ ⊢ \phi \to \psi_j$, we have, by Gen, $Γ ⊢ ∀x(\phi \to \psi_j)$, and so, by MP, $Γ ⊢ \phi \to ∀x\psi_j$; that is, $Γ ⊢ \phi \to \psi_i$.