Proving a theorem in GL modal logic I'm trying to prove a number of theorems in the system GL using the basic axioms of system K and the following axiom schema from GL: $\vdash_G \Box A \rightarrow \Box\Box A$ for every A.
One of theorems that is supposed to hold for GL is giving me a really tough time. It is: $$\vdash_G \neg\Box A \leftrightarrow \diamond (\neg A \wedge \Box A)$$
Going from right to left is not the hard part for me. When proving the biconditional in that direction, I can use the weak modal distributivity to put the possibility (diamond) around each of the arguments in the conjunct, giving me $\diamond \neg A \wedge \diamond\Box A$.
I can then simplify the conjunct and using the modal negation schema, turn $\diamond \neg A$ into $\neg\Box A$. The issue is in going left to right for the conditional because I can't build the consequent.
Am I going about this the wrong way? Should I even be doing it in two parts or proceeding from some sort of tautology that applies here and then use substitution? My issue is that it seems incorrect to say that if A is not necessary then it is possible to have not A and necessary A. The conjunct does not seem to follow at all from the antecedent nor does it seem consistent if we understand the boxes and diamonds as necessities and possibilities.
 A: The axiom you wrote down: $$\square A\rightarrow \square\square A$$
is usually called "4". And the modal logic obtained by extending the basic system K by this axiom is called K4. The logic K4 is strictly weaker than the system GL, which is K extended by Löb's axiom: $$\square(\square A\rightarrow A)\rightarrow \square A.$$
The sentence you want to prove: $$(\star)\quad\lnot \square A \leftrightarrow \lozenge(\lnot A\land \square A)$$
is not provable in K4. How can we see this? Well, K4 is sound on transitive Kripke frames, so every sentence provable in K4 is valid on every transitive Kripke frame. Consider the frame with a single world $w$ which is accessible from itself ($wRw$).  Then $R$ is transitive. Interpret $A$ so that it  does not hold at $w$. Then $\lnot \square A$ is true at $w$, but $\lozenge(\lnot A\land \square A)$ is not true at $w$, since the only world accessible from $w$ is $w$, and $\square A$ is not true at $w$. Thus $(\star)$ is not valid on this frame, and hence is not provable from K4.
So if you want to prove $(\star)$ in GL, you have to use Löb's axiom. Let's try to do that, and we'll start by rewriting $(\star)$ using propositional logic.
\begin{align*}
\lozenge(\lnot A\land \square A) &\equiv \lnot \square \lnot (\lnot A \land \square A)\\
&\equiv \lnot \square (A\lor \lnot \square A)\\
&\equiv \lnot \square (\square A\rightarrow A)
\end{align*}
Ok so to prove $(\star)$, it suffices to prove $$\lnot \square A\leftrightarrow \lnot \square (\square A\rightarrow A).$$
Taking away the $\lnot$ from both sides, it suffices to prove $$\square A\leftrightarrow \square (\square A\rightarrow A).$$ After our rewriting, we can see that the $\leftarrow$ direction is exactly Löb's axiom! And the $\rightarrow$ direction is easy (this corresponds to the easy direction you proved in your quesiton). We certainly have $A\rightarrow (\square A\rightarrow A)$, so by necessitation, $\square(A\rightarrow (\square A\rightarrow A))$, and by distributivity of $\square$ over $\rightarrow$, $\square A\rightarrow \square (\square A\rightarrow A)$.
So at the end of the day, we can see that $(\star)$ was just a fancy way to rewrite Löb's axiom (modulo propositional logic and K).
