Proving axiom M in modal logic from K plus A → ◊A

Question

I'm slowly working my way through Garson's Modal Logic for Philosophers. I'm stuck on exercise 2.1c. It asks me to prove axiom M (= ◻A → A) in system K (propositional logic + necessitation and distribution) with the added axiom A → ◊A.

I've tried a couple of ways to do this. The most obvious ways have been (1) a conditional proof and (2) an indirect derivation/reductio on the assumption of the negation of M. Each faces difficulties, though. On the first method, I keep reaching a point where I get iterated modal operators, and we haven't covered what to do with those yet. On the second strategy, I reach a point where I'm required to use ~A → ◊~A. This is, strictly speaking, not allowed. I'm only allowed to use A → ◊A plus the standard rules and axioms of K. Using the version with negation signs in it doesn't seem licit. I'm most familiar with natural deduction, but I'm not sure how to do natural deduction on a computer. I'll sketch both attempts I've made so far in a rough-and-ready ND, starting with the conditional proof.

Attempted conditional proof:

1. Assume ◻A for conditional proof
2. Begin boxed subproof: ◻
3. Bring A in line 1 under boxed subproof: A
4. Employ A → ◊A
5. By modus ponens on 3,4: ◊A
6. Bring ◊A out of boxed subproof: ◻◊A
7. ???
8. A

As you can see, once I get the iterated modal operators in line 6, I see no way forward to get to A, so I can't complete the conditional derivation.

Attempted indirect proof/reductio:

1. Assume ~(◻A → A)
2. By the negated conditional rule: ◻A & ~A
3. By simplifying left side of 2: ◻A
4. ◻A → ~◊~A
5. By modus ponens on 3,4: ~◊~A
6. By simplifying right side of 2: ~A
7. ~A → ◊~A
8. By modus ponens on 6,7: ◊~A
9. Contradiction on 5,8 under our assumption in line 1.
10. Hence, ~~(◻A → A)
11. Double negation on 10: ◻A → A

As you can see, I'm able to make it to the end of this proof and obtain what I want, but it involves asserting ~A → ◊~A on line 7, which is strictly speaking not allowed, given that I'm only allowed to work with rules of propositional logic, necessitation, the distribution axiom, and A → ◊A. I've been banging my head on this trying to find a way forward for a while. Any help would be appreciated.

By the way, I'm learning this on my own for fun. This is not a problem on any homework assignment for a class I'm in or anything of that sort!

Answer 1

"$A$" in the axiom "$A\to\operatorname{\diamond} A$" is a metavariable. As such, we can uniformly substitute in any wff we like; from $\lnot A\to\operatorname{\diamond} \lnot A$ to $\lnot (A\land\operatorname{\square}(B\lor C))\to\operatorname{\diamond} \lnot (A\land\operatorname{\square}(B\lor C))$

Garson does make this clear eventually, both through description and through example proofs.

As for your proof, it looks fine, but there is a more elegant way to do it (the technique makes other proofs easier as well, so I'd recommend working it out). As a hint, what happens if you assume $\operatorname{\square} A$ for the purposes of a conditional proof? What's the contrapositive of line 7?