I have been using Garson's Modal Logic for Philosophers, 2nd edition, to learn how to use natural deduction with modal logic. (BTW, does anyone know where there's an answer key for chapters 1 and 2 of Garson?)
For some of the exercises, it seems to me that the obvious approach is to use indirect proof (IP), which Garson includes (of course) among the rules for PL, and therefore for K and other modal logics. Unfortunately, Garson does not give an example of a proof of a modal sentence involving IP.
The problem I'm running into is that I am able to establish a contradiction in a modal subproof, but it's not clear to me how to propagate this back to the main proof and thereby establish the desired result.
For example, exercise 2.3(c) in Garson is to prove that <><>A <-> <>A in S4. Here's my attempt to prove the forward implication (<><>A -> <>A):
|<><>A |----- ||~<>A ||---- ||~A (~<>) ||~A (4) ||<><>A (Reit) |||, <>A (<> Out) |||------- |||~A ( Out) ||||, A (<> Out) ||||----- ||||~A ( Out) ||||# (# In)
Here I would like to write
|<>A (IP) <><>A -> <>A (CP)
Is that legitimate? Does the # (contradiction) in the sub-sub-subproof license IP at the top level?
Thanks for any insight!