Prove in GL that no statement can be proven consistent with PA unless PA is inconsistent

Question

I'm trying to do a exersie on page 16 of this paper. It says:

Exercise. Show, using the rules of Godel-Lob modal logic (GL), that $\square⊥ ↔ \square \diamond p$; recall that $\diamond p = ¬\square¬p$. Informally, that is, no statement can be proven consistent with Peano Arithmetic unless Peano Arithmetic is inconsistent.

[Hint: First prove that $\square⊥ → \square \diamond p$, then that $\square \diamond p → \square ⊥$. For the latter, it will help to rewrite $¬\square⊥$ as $\square⊥ → ⊥$, then consider the Lobian axiom $\square(\square⊥ → ⊥) → \square⊥$.]

It also lists these axioms of GL:

1. All tautologies of the propositional calculus are axioms of GL, including tautologies where an expression including $\square$ has been substituted for a variable (for instance, $\square p ∨ ¬\square p$ is an axiom).
2. Modus Ponens Rule: if the expressions $A$ and $A → B$ are theorems, then so is $B$.
3. Distribution Axioms: for any expressions A and B in the language, we have the axiom $\square(A → B) → (\square A → \square B)$.
4. Generalization Rule: if the expression A is a theorem, then so is $\square A$.
5. Godel-Lob Axioms: for any expression A, we have the axiom $\square(\square A → A) →\square A$.

I first re wrote the problem as $\square⊥ ↔ \square¬\square¬p$
I couldn't figure out how to start proving $\square⊥ → \square¬\square¬p$, I didn't find any axioms that I could apply to the problem to make progress.

I made some progress with $\square¬\square¬p → \square⊥$ by using the hints:
$¬\square⊥ → ¬\square¬\square¬p$ (Axiom of PA )
$\square⊥ → ⊥ → ¬\square¬\square¬p$ (rewrite $¬\square⊥$ as $\square⊥ → ⊥$ hint)
$\square(\square⊥ → ⊥) → ¬\square¬\square¬p$ (Generalisation rule)
$\square⊥ → ¬\square¬\square¬p$ Lob's theorem
I'm not sure where to go from here though.

Any hints on where to go in either part of the proof are appreciated.

Answer 1

For $\Box\bot\to\Box\neg\Box\neg p$, use the tautology $\bot\to\neg\Box\neg p$.

For $\Box\neg\Box\neg p\to\Box\bot$, use the tautology $\bot\to\neg p$ to infer $\Box\bot\to\Box\neg p$, thus $\neg\Box\neg p\to\neg\Box\bot$, from which you can derive $\Box\neg\Box\neg p\to\Box\neg\Box\bot$. Then, as the hint tells you, $\Box\neg\Box\bot\to\Box\bot$ is an instance of Löb’s axiom.