Cancellation of Hypothesis in Gentzen Deduction

I am reading Dirk Van Dalen's Logic and Structure. In Section 2.4, Page 32, Van Dalen introduces Natural Deduction due to Gentzen and talks about the "cancellation of hypothesis" in reductio ab absurdum rule (RAA) and the introduction of implication rule. He makes two queries and clarifies and yet it is unclear to me what the author is trying to.

In Query $1$, he takes an example from Euclidean Geometry which says that the angles at the base are equal if the triangle is isoceles. The hypothesis here is that the triangle is isoceles and it is indeed the case the hypothesis is necessary. So, what does the author mean by cancellation of hypotheses?

Also, his other example of uniqueness of limit of a sequence is not quite clear to me. I would appreciate if someone could break it down for me.


Note that when we deduce ψ using the temporary supposition φ, the φ is said by van Dalen to be a hypothesis of the (sub)proof. And when we apply the rule of conditional proof, we rely on the fact that there is a deduction from ψ from the temporary supposition φ, and now drop the supposition and infer the conditional φ → ψ. The dropped supposition/hypothesis φ is, in other terminology, discharged or [in van Dalen's words] cancelled in applying the conditional proof rule and inferring φ → ψ.

And now note that in φ → ψ, φ is not a hypothesis, not a stand-alone proposition assumed for the sake of argument, but is the antecedent of a conditional, part of φ → ψ.

So I suspect your puzzlement about van Dalen's passage comes from confusing φ as a hypothesis, a stand-alone assumption, with φ as the antecedent of a conditional.

So to go back to almost his own words, "In abstracto: if we can deduce ψ using the hypothesis φ, then we can drop the hypothesis and infer φ → ψ [a conditional, with φ as antecedent]. And this conditional follows without any longer requiring the hypothesis φ (there may be other hypotheses in play, of course)."

For more, visit https://www.logicmatters.net/ifl and download my logic book, zip forward to Ch. 22 to look at proofs using conditionals. The lay out is different from Gentzen's (we discharge hypotheses by jumping columns rather than striking through) but the Big Ideas, in particular the use of conditional proof and the idea of discharging/cancelling hypotheses is exactly the same.