Deduction theorem with undischarged statement

Question

I am reading "Mathematical logic" by Ian chriswell and Hodges and at one point in the text they mention the deductive theorem (page 17) which states;

If $\Gamma \cup \left \{ \phi \right \} \vdash \psi $ then $\Gamma \vdash (\phi \rightarrow \psi) \quad$ where $\Gamma$ is the set containing the undischarged assumptions of the argument. Now my confusion starts at the point where they mention that its possible that $\phi \in \Gamma$ in which case it will still be an assumption in $\Gamma \vdash (\phi \rightarrow \psi) \quad$ however I was under the impression that the whole point of the deduction theorem was to enable us to discharge assumptions so that they no longer are apart of $\Gamma$, so what exactly is going on in this particular case? Is $\phi$ discharged or not?

The author also mentions that the rule is still correctly applied if we do not discharge all occurrences of $\phi$ which does not seem like a correct statement for a rule whose purpose is to discharge assumptions.

Answer 1

We can discharge the assumption $\phi$, but we are not forced to do so.

See page 17 :

Thus if $\phi$ is an assumption written somewhere in $D$, then we discharge $\phi$ by writing a "dandah" through it: $\phi^/$. In the rule ($\to$I) below, and in similar rules later, the $\phi$ means that in forming the derivation we are allowed to discharge [emphasis mine] any occurrences of the assumption $\phi$ written in $D$.

The rule is still correctly applied if we do not discharge all of them [emphasis mine]; in fact the rule is correctly applied even if $\phi$ is not an assumption of $D$ at all, so that there is nothing to discharge.

You have also to note that [page 17] :

We shall discharge occurrences of assumptions.

Again, we can discharge all occurrences of an assumption $\phi$ but we are not forced to do it: we can discharge some occurrences of $\phi$ but not all. In this way, after the "discharge" the set $\Gamma$ of assumption may still include occurrences of $\phi$.

---

The "idea" of an undischarged assumption is simply this : if we can prove $\vdash \varphi \to \psi$ (without assumption) we can also prove : $\sigma \vdash \varphi \to \psi$ (with an extra-assumption).

Intuitively, a "redundant" assumption does not invalidate the proof of a theorem.