In
- Amati and Pirri, A uniform tableau method for intuitionistic modal logics I (1993)
a tableau method for a variety of intuitionistic modal logics is presented with signed formulas ('$\textbf{T}A$' for true formula $A$ and '$\textbf{F}A$' for false formula $A$.)
However, they employ a rule, $S \thinspace \Box$ (p.11 of the above article), which I do not understand and which is causing me much distress.
$Notation$: Let $\Gamma$ be a set of signed formulas (i.e a set of formulas assigned a truth value $\textbf{T}$ or $\textbf{F}$, where $\textbf{T}A$ indicates $A$ is true and $\textbf{F}A$ that $A$ is false) For Intuitionistic $S4$, $\Gamma^\# := \{\thinspace \textbf{T} A \hspace{0.2cm} | \thinspace \textbf{T} A \in \Gamma \thinspace \} $ and $\Gamma^N := \{\thinspace \textbf{T} \thinspace \Box A \hspace{0.2cm} | \thinspace \textbf{T} \thinspace \Box A \in \Gamma \thinspace\} \thinspace \cup \thinspace \{\thinspace \textbf{F} \thinspace \Diamond A \hspace{0.2cm} | \thinspace \textbf{F} \thinspace \Diamond A \in \Gamma \thinspace\}$ and $\textbf{T} \Diamond \Gamma$and $\textbf{F} \thinspace \Box \Gamma$ indicate, respectively, the set of formulas $\textbf{T}\Diamond A \in \Gamma$ and $\textbf{F}\thinspace \Box A \in \Gamma$.
The rule $S \thinspace \Box$ (presented in section 4.4 of their article) is as follows (where I presume $|$ indicates alternative branches of the tree):
$$ \frac{\Gamma, \textbf{F} \thinspace \Box \thinspace A}{\small\Gamma^{\#},\thinspace \textbf{T}\Diamond \Delta_1, \textbf{F}\thinspace \Box \thinspace \Omega_1 \thinspace| \thinspace ...\thinspace| \thinspace\Gamma^{\#},\thinspace \textbf{T}\Diamond \Delta_p, \textbf{F}\thinspace \Box \thinspace \Omega_p\thinspace| \thinspace\Gamma^{\#^N},\thinspace \textbf{T}\Delta_{p+1}, \textbf{F}\thinspace \Omega_{p+1}\thinspace| \thinspace...\thinspace| \thinspace \Gamma^{\#^N},\thinspace \textbf{T} \Delta_{n}, \textbf{F}\thinspace \Omega_{n} }$$
with $n \geq p \geq 0$ and where we have that the root of the following tree (i.e, the conclusion proved) is derived via structural rules or rules governing logical connective and not by rules governing $\Box$ or $\Diamond$:
$$ \frac{\Gamma^{\#^N},\thinspace \textbf{F}A}{\Gamma^{\#^N},\thinspace \textbf{T}\Delta_{1}, \textbf{F}\thinspace \Omega_{1}\thinspace| \thinspace...\thinspace| \thinspace \Gamma^{\#^N},\thinspace \textbf{T} \Delta_{n}, \textbf{F}\thinspace \thinspace \Omega_{n}} {\text{}} $$
In the rest of section 4.4 they give examples in which the rule is used. In section 4.5 they make a number of remarks about the rule which seem to be crucial to understanding it.
The rule seems to allows you to take a formula $\textbf{F}\Box A$ and remove the $\Box$, removing $\Box$ from the formulas also of the form $\textbf{T}\Box X$. Then it allows you to 're-modalise' $\textbf{T}$ formulas with $\Diamond$, and $\textbf{F}$ formulas with $\Box$, retaining any true formulas initially in $\Gamma$ as in the following derivation they give in section 4.5:
$$\Gamma, \textbf{F} \thinspace \Box (A \rightarrow B)$$ $$\Gamma^{\#^N}, \textbf{F}(A \rightarrow B) \hspace{0.5cm}{by \hspace{0.1cm} \Box S} $$ $$\Gamma^{\#^N},\textbf{T}A, \textbf{F}B \hspace{0.5cm}{by \hspace{0.1cm} S \supset}$$ $$\Gamma^{\#},\textbf{T}\Diamond A, \textbf{F} \thinspace \Box B \hspace{0.5cm}{by \hspace{0.1cm} S \Box}$$
I wanted to see if we have in Intuitionistic $S4$ (as with classical S4) $\hspace{0.3cm}$ $\vdash \Diamond \Box (A \rightarrow \Box \Diamond A)$ and generated this :
$$\textbf{F} \thinspace\Diamond \Box (A \rightarrow \Box \Diamond A) $$ $$\textbf{F} \thinspace \Box (A \rightarrow \Box \Diamond A) \hspace{0.5cm} \text{by $R \Diamond$}$$ $$\textbf{F}(A \rightarrow \Box \Diamond A) \hspace{0.5cm} \text{by $S \Box$} $$ $$\textbf{T}A, \thinspace \textbf{F} \Box \Diamond A \hspace{0.5cm} \text{by $S \supset$} $$
However, I don't know how to proceed with the proof, since $S \Box$ remains unclear to me.