Equivalence between $\mathbf{KT_4}$ and Lewis' $\mathbf{S_4}$

Question

Let us define modal logic system $\mathbf{KT_4}$ by adding the following axioms to classic propositional logic

1. $\diamond A\leftrightarrow\lnot\square\lnot A$
2. $\square(A\rightarrow B)\rightarrow(\square A\rightarrow\square B)$
3. $\square A\rightarrow A$
4. $\square A\rightarrow\square\square A$

and using the inference rule according to which we can infer $\square\varphi$ if $\varphi$ has been inferred.

I read (D. Palladino, C. Palladino, Logiche non classiche, 'non-classical logics', 2007) that $\mathbf{KT_4}$ is equivalent to Lewis' $\mathbf{S_4}$ system defined by the following axioms, where $A\supset A\equiv\square(A\rightarrow B)$ and $\square A\equiv\lnot\diamond\lnot A$

1. $(A\land B)\supset (B\land A)$
2. $A\supset (A\land A)$
3. $(A\supset B)\land(B\supset C)\supset(A\supset C)$
4. $(A\land B)\supset A$
5. $((A\land B)\land C)\supset((A\land B)\land C)$ [sic, but I suspect that a typographical error might have occurred where $((A\land B)\land C)\supset(A\land (B\land C))$ -or even a biconditional?- were intended]
6. $A\land(A\supset B)\supset B$
7. $\diamond(A\land B)\supset\diamond A$
8. $(A\supset B)\supset(\lnot\diamond B\supset\lnot\diamond A)$
9. $\square A\supset \square\square A$

together with the inference rules $\frac{A,A\supset B}{B}$ and $\frac{A,B}{A\land B}$.

But I am not able to prove the equivalence to myself. In particular I do not see how axiom $\square A\rightarrow A$ is derived in $\mathbf{S_4}$. As to $\square((A\land (B\land C))\rightarrow((A\land B)\land C))$, is it intended to be among the axioms of $\mathbf{S_4}$ or can it be derived? I thank you very much for any clarification.

Answer 1

HINT

Following Zeman's site, Ch.5 THE ABSOLUTELY STRICT SYSTEMS S1, I've tried to "reconstruct" the derivation of :

$\square p \to p$.

The axioms are the one listed above.

Starting from 6 :

$A ∧ (A ⊃ B) ⊃ B$

with the substitution : $A/\lnot p$ and $B/p$ we get :

$\lnot p ∧ (\lnot p ⊃ p) ⊃ p$

and applying the following derived equivalence (I've used $p \supset \subset q$ for $\square (p \leftrightarrow q)$ i.e. for "strict equivalence") :

$[p \supset (q \to r)] \supset \subset [(p \land q) \supset r]$ --- (Zeman's 5.21 : a "modalized" importation/exportation law)

we have :

$(\lnot p ⊃ p) ⊃ (\lnot p \to p)$ --- Zeman's 5.96.

We can derive, from Ax.4, Ax.2 and Ax.3 the "law of identity" :

$p \supset p$ --- Zeman's 5.5

and :

$p \supset \subset p$ --- Zeman's 5.6.

From this last formula, with the subsitution $p/\square p$, we get :

$\square p \supset \subset \square p$ --- Zeman's 5.48.

Finally, we derive some "modalized" versions of the tautology : $p \leftrightarrow (\lnot p \to p)$, that is :

$p \supset \subset (\lnot p \supset p)$ --- Zeman's 5.47

and

$\square p \supset \subset (\lnot p \supset p)$ --- Zeman's 5.50.

Now, all the "ingredients" are in place; using the rule of "substitutivity of strict equivalence" we substitute into 5.96 above : $\square p$ in place of the antecedent of the strict conditional and $p$ in place of the consequent, deriving :

$\square p ⊃ p$ --- Zeman's 5.97.

To conclude, we need to meta-theorems :

5.1 --- If $\alpha$ is a theorem of Propositional Calculus, then $\square \alpha$ is a theorem of $\mathbf{S_4}$

and

5.2 --- If $\vdash_\mathbf{S_4} \square \alpha$, then also $\vdash_\mathbf{S_4} \alpha$.

Now, from 5.97 : $\square p ⊃ p$, by definition of $\supset$ we have :

$\square (\square p \to p)$

and thus, applying the meta-theorem 5.2 we conclude with :

$\vdash_\mathbf{S_4} \square p \to p$.