This was primarily because this is used to claim that, since we cannot prove that (a maximally great) god does not exist, it is possible that (a maximally great) god does exist, furthermore since we cannot prove that (a maximally great) god is does not exist necessarily it is possible that (a maximally great) god does exist necessarily and it therefore follows that (a maximally great) god does exist (necessarily). Sounds like BS, right?
Anyway, I also argued against a more complex version of the argument (raised by cpdavey):
1. ◊□A (Assumption for Conditional Proof (CP))
2. ~□A (Assumption for Reductio Ad Absurdum (RAA))
3. ~~◊~A (2 E2)
4. ◊~A (3 Double Negation (DN))
5. □| ◊~A (4 S5-reit)
6. □◊~A (5 nec intro)
7. □~□~~A (6 E1)
8. □~□A (7 DN)
9. ~◊~~□A (8 E2)
10. ~◊□A (9 DN)
11. ◊□A & ~◊□A (1,10 Conjunction)
12. ~~□A (1-11 RAA)
13. □A (12 DN)
14. ◊□A -> □A Q.E.D. (1-13 CP)
14. ◊□A -> □A Q.E.D. (1-13 CP)
I concluded that the Reductio Ad Absurdum wasn't actually necessary, because you can do it like this:
1. ◊□A (Initial position)
2. A <--> ~B (Assumption for Logical Fiddle)
2. A <--> ~B (Assumption for Logical Fiddle)
3. ◊□~B (Substitution of 2 into 1)
4. ~~◊~~□~B (3 double DN)
5. ~□~□~B (4 E2)
6. ~□~□A (Substitution of 2 into 5)
7. □A (6 n2)
8. ◊□A -> □A Q.E.D. (1-7)
But here we can see that the step between (6) and (7) is not valid (because it's reversed) - so there's a problem which is being disguised by the process of going through the Reductio Ad Absurdum.
I pretty much left it at that, inviting the reader to point out where the problem is, if they could see it. That was five years ago.
So, what was the obvious thing that recently leaped out at me? The proof put together, or at least presented by cpdavey relies rather heavily on the introduction of double negatives and swapping from ~□~ to ◊ and from ~◊~ to □. Both of these latter two moves can be reversed (see Classical Modal Logic). What it doesn't rely on, is the value of A. Which means we can do this:
1. ◊~G (Initial weakish atheism position)
2. ~□~~G (1 classical modal logic)
2. ~□~~G (1 classical modal logic)
3. ~~□~□~~G (2 n2, right way around)
4. □~□G (3 DN removed)
5. ~◊□G (4 classic modal logic)
This means we arrive at the same conclusion whether we assume that it is possible that there is no god (◊~G) or that it is not necessary that there is a god (~□G), namely that it is not possible that there is necessarily a god (~◊□G), which is precisely what we would expect.
Effectively all cpdavey was arguing was that if his presumption was correct, then assuming the truth of the opposite of his presumption would lead to a conclusion that his presumption was incorrect. Which it did and which we would expect. That's why there's no great problem within his "Reductio Ad Absurdum" but there is when we run his proof with no RAA. His whole argument came down to a "heads I'm right, tails you're wrong" sort of con.
The error is quite clear in Step 12 above, where cpdavey writes "12. ~~□A (1-11 RAA)". Clearly the RAA started at Step 2, not Step 1.
Sometimes we just don't see things that are staring us in the face. Perhaps I was trying too hard to be clever. But then again, so was cpdavey, since the result that he needed to get his RAA to work was precisely the one he was aiming at, via use of the RAA, ie the fallacious claim that, given ◊□A, □A.