Thank you so much, @lemontree ! My proof would be like this. Is it correct ?

I assume there exists a derivation of $\phi$ with no open assumptions. $$ \vdots\\ \phi $$ Using the rule of $\to\mathbf{I}$, I can conclude $\psi \to \phi$ with no open assumptions. Therefore, $\vdash \psi \to \phi$.

The point of this exercise (I think) is to have understood that $\to I$ (and other rules that allow to discharge assumptions) may be applied without discharging (all) occurrences of the assumptions, or (like here) without the assumption even present in the derivation at all.

Thank you ! I think you raise something important, @lemontree. Could you clarify why you say that "$\to\mathbf{I}$ me be applied without discharging (all) occurrences of the assumptions" ? Is it something that could be deduced from rule definition ? Also, could you tell me a few rules that allow its application in a similar way (without discharging all occurrences of the assumptions) ?.

You already used this correctly in your proof. The rule ($\to I$) $\quad [\psi]^i \cdots \phi - \psi \to \phi\quad $ states that the antecedent $\psi$ to be introduced is an assumption from which $\phi$ was derived and which may be [discharged]${}^1$ when applying the rule. But in your proof, the assumption $\psi$ does not exist in the derivation of $\phi$, and we are allowed to $\to$-introduce it anyway: Dischargeable assumptions need not be actually present in the derivation.

The other half of the issue is that existing occurrences of dischargeable assumptions need not actually be discharged: $\psi \cdots \phi - \psi \to \phi$, yielding $\psi \vdash \psi \to \phi$ (instead of $\vdash \psi \to \phi$) would also be a correct application of the $(\to I)$ rule.

This holds for all rules that allow to discharge assumptions: You can either discharge all occurrences, leave all of them open, discharge some while keeping others open (talking about occurrences because it could be that the assumption was used multiple times in the derivation of the conclusion), or have no occurrence of the assumption at all. Other rules that allow to discharge assumptions are $\neg I$ (discharging the unnegated assumption), $\bot$ (discharging the negated assumption) and $\lor E$ (discharging the two disjunctions).

That this is generally allowed is not obvious from the notation in the rule schemata themselves and probably was mentioned in the text when introducing the ND notation and explaining the discharging of assumptions.

Thank you so much, @lemontree. I wasn't aware that this was allowed. May I ask, if I leave those assumptions undischarged, isn't the rule incorrectly applied ? Perhaps, I am missing the point.

Regarding your last comment, I found in the book on page 34: "With respect to the cancellation of hypotheses, we note that one does not necessarily cancel all occurrences of such a proposition ψ. This clearly is justified, as one feels that adding hypotheses does not make a proposition underivable (irrelevant information may always be added)."

I still do not see (although, continually use in proofs), why is the application of, for example, $\to I$ valid if I do not discharge (all) assumptions. For example, say I have an assumption 5 times, if I understand correctly, to use the inference in a correct way, I must discharge (at least) one of those assumption. But, what happens if there are none ?

Thank you for all the help, @lemontree. Reading several times your answers, I think I am starting to understand. I see ->I rule doesn't force to discharge all assumption, but the ones left open, become premises. For example, when proving $Q \vdash P \to Q$, if I leave an assumption of P open, I end up proving ${P, Q} \vdash P \to Q$. Is this correct ?

It is explained on p. 34: "W.r.t. the cancellation of hypotheses, we note that one does not necessarily cancel all occurrences of such a proposition \psi. [...] Furthermore, one may apply (-> I) if there is no hypothesis available for cancellation."

Oh, you found that exact passage. Should have finished reading all your comments before starting to talk agian.

No, leaving some or all assumptions undischarged is explicitly a correct rule application. You can and typically want to cancel dischargeable assumptions, but you don't have to. That liberty is part of how cancellation is defined.

If you have 5 occurrences of the assumption, you can discharge 0, 1, 2, 3, 4, or 5 of these occurrences. If you have 0 occurrences of the assumption, you can apply the rule anyway.

Re. your last comment: Yes, that's correct.

Note also that you are allowed to write whatever additional premises left of the $\vdash$ even if they don't occur as open assumptions in your derivation: The definition of $\vdash$ is that there is a tree whose open assumptions are a subset of the premises, given your derivation of proving P -> Q from Q, you are allowed to write not only Q |- P -> Q, but also e.g. R, Q |- P -> Q.

That's fantastic, thank you so much, @lemontree.I am almost there. I did a proof to be sure I understand. Assumption of P from line 2 is not discharged. On the other hand, assumption of P in line 4 is indeed discharged. So, there are two occurrences of the same assumption and I discharged only one of them.

I ended up proving $P,Q \vdash P \to Q$. Is this correct ? Link to image: dropbox.com/s/h3u3on218w2w0el/…