discharge assumption in another branch

Question

I am self studying from Chiswell & Hodges mathematical logic, and I have a general question about discharging assumptions. To demonstrate, I am using exercise 2.5.1(c), which asks for a proof of:

$$\{(\phi \leftrightarrow \psi),(\psi \leftrightarrow \chi)\} \vdash ((\phi \leftrightarrow \chi)$$

I apologize for posting a possible solution via imgur, but I couldn't figure out how to label the rules beside the horizontal lines in Tex.

solution for exercise

QUESTION: can I discharge an assumption in a different branch of the overall derivation than where the discharge occurs? (see picture) i.e. can I discharge the $\phi$ in the right branch with the $(\rightarrow I)$ in the left branch?

P.S. I know the provided solution is wrong; in the right branch I struggled to obtain $\phi$ for $(\chi\rightarrow\phi)$, but eventually solved it in a self-contained manner. However, it did raise the question above, and I wanted to confirm that such an option was not possible.

P.P.S. I am aware of this question, but I feel that it does not quite answer mine, and wanted further clarity.

Answer 1

I recommend you learn Fitch-style natural deduction as well (see examples and rules), which show explicitly the context of every single statement. This would also make clear precisely what is going on in tree-style natural deduction. Specifically, discharging an assumption corresponds to coming out from under the context of that assumption.

Here is the Fitch-style proof: $ \def\eq{\leftrightarrow} $

---

$P \eq Q$.

$Q \eq R$.

$P \to Q$.

$Q \to R$.

If $P$:

  $Q$.

  $R$.

$P \to R$.   [(1)]

[... Similarly ...]

$R \to P$.

$P \eq R$.

---

As you can see, the $\to$-introduction at (1) corresponds exactly to what is called 'discharging of $P$' in tree-style natural deduction. Importantly, you can also see that according to the rules you cannot 'discharge $P$' at other places. It makes no sense anyway.

An in-between alternative is sequent-style natural deduction as described in Rautenberg's Concise Introduction to Mathematical Logic. Either form of natural deduction will also make it easy to understand Hilbert-style systems for first-order logic, which are otherwise rather opaque.