Garson Exercise 2.4(a), Show axiom (4) is provable in S5

Question

$\lozenge $= possible

$\square $=necessary

Hey all, I am trying to show the following axiom is provable in $S5$:

$\square A \to \square \square A = (4)$

The hint says to prove: $\square A \to \square \lozenge \square A $ first, which I have done:

1 ) $\square A$

2-) $\square \lnot \square A \to \lnot \square A$ (instance M)

3-) $\square A$ (1, Reit)

4-) $\lnot \lnot \square A$ (3, ~~In)

5-) $\lnot \square \lnot \square A$ (2-4, MT)

6-) $\lozenge \square A$ (5, Def $\lozenge$)

7-) $\lozenge \square A \to \square \lozenge \square A$ (instance of 5: $\lozenge P \to \square \lozenge P$)

8-) $\square \lozenge \square A$ (6-7, MP)

9 ) $\square A \to \square \lozenge \square A$ (1-8, CP)

I am stuck on the second leg, any help on how to prove $ \square \lozenge \square A \to \square \square A$

By the way, there is a similar question here but it is not what I am looking for. I am looking for a Natural deduction. Thanks!

Answer 1

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$ In Exercise $2.3 (i)$ you should already proved, or you need to attempt this first

direction $1$ $\fitch{\Diamond\square A} {\vdots\\\square A}\hspace{5ex}\text{direction $2$}\fitch{\square A} {\vdots\\\Diamond\square A}$

Exercise $2.4(a)$ will become much easier

$\fitch{\square A} {\Diamond\square A\hspace{10ex}\text{$2.3(i)$ direction 2}\\ \square\Diamond\square A\hspace{8ex} (5)\\ \fitch{\square} {\Diamond\square A\hspace{6.5ex}\square\text{Out}\\ \square A\hspace{8ex}\text{$2.3(i)$ direction 1}}\\ \square\square A\hspace{10ex}\square\text{In}}$

Update:

If not sure about how to prove $2.3i)$ check this

$\color{lightgrey}{\fitch{\color{black}{\square A}} {\color{black}{\Diamond\square A\hspace{16ex}\text{$2.1(a)$}}\\ \square\Diamond\square A\hspace{14ex} (5)\\ \fitch{\square} {\color{black}{\Diamond\square A\hspace{11.5ex}\square\text{Out}\\ \neg\square\neg\square A\hspace{7.5ex}\Diamond\text{Def}\\ \fitch{\neg\square A}{\Diamond\neg A\hspace{9.2ex}\text{1.10(b)}\\ \square\Diamond\neg A\hspace{7ex}(5)\\ \fitch{\square} {\Diamond\neg A\hspace{5.6ex}\square\text{Out}\\ \neg\square\neg\neg A\hspace{2.2ex}\Diamond\text{Def}}\\ \square\neg\square\neg\neg A\hspace{4ex}\square\text{In}\\ \square\neg\square A\hspace{6.8ex}\text{2.3(g)}\\ \bot\hspace{12.2ex}\bot\text{In} }}\\ \color{black}{\square A\hspace{13.8ex}\text{IP}}}\\ \square\square A\hspace{15.5ex}\square\text{In} }}$