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.

  • 1
    $\begingroup$ Your suggested correction is right; see Modern Origins of Modal Logic : Axiom B4 of original Lewis' system S1. $\endgroup$ Feb 28 '15 at 14:20
  • $\begingroup$ @MauroALLEGRANZA Thank you so much!!! Interestingly, $(A\land (B\land C))\supset((A\land B)\land C)$ doesn't appear in Lewis' axioms... I wonder how associativity (as well as $\square A\rightarrow A$) can be inferred from these axioms... $\endgroup$ Feb 28 '15 at 15:21
  • $\begingroup$ @MauroALLEGRANZA Does $p\supset \lnot\lnot p$ imply, together with the other axioms, that $\square p\rightarrow p$ and that $(p\land(q\land r))\rightarrow((p\land q)\land r))$? Thank you again! $\endgroup$ Feb 28 '15 at 19:03
  • 1
    $\begingroup$ In Zeman's site, Ch.5, I think you can find the answer... $\endgroup$ Mar 2 '15 at 7:26


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


$\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}$


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$.

  • $\begingroup$ I want to thank you already. I'm trying to follow Zeman's derivations of the theorems (I hope I'm understanding the notation: for ex. I think that $Cpq$ means $p\rightarrow q$) and hope that, notwithstanding my temperature, I'll be able to study them tomorrow, since I won't work. $\endgroup$ Mar 2 '15 at 19:57
  • 1
    $\begingroup$ @Self-teachingDavide - Yes; $Cpq$ is $p \to q$; $Np$ is $\lnot p$; $Kpq$ is $p \land q$. See Polish notation for logic. $\endgroup$ Mar 2 '15 at 20:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.