# Is this system identical to S4.4?

Consider the normal modal logic system $\mathbf{TAR1}$ given by $\mathbf{T}$ plus the following axiom:

$$\mathrm{AR1}: \lozenge \square p \rightarrow (\square p \lor \square (p \rightarrow \square p))$$

Analysis using normal forms shows that it is included in $\mathbf{S4.4}$. However, algebraically I cannot either prove or disprove that it is strictly weaker. I was wondering is someone has a proof or an argument based on Kripke semantics.

Additional info, in case it helps:

• $\mathbf{S4.4}$ is usually defined as $\mathbf{S4}$ plus axiom $\mathrm{R1}$: $$\mbox{R1}: \lozenge \square p \rightarrow (p \rightarrow \square p)$$ I find that $\mathbf{S4.4}$ is also $\mathbf{T}$ plus the following axiom: $$\mathrm{4.4}: \lozenge \square p \rightarrow \square (p \rightarrow \square p)$$

• I also find that $\mathbf{TAR1}$ is equivalent to $\mathbf{TR1}$, which is $\mathbf{T}$ plus $\mathrm{R1}$. But the question now becomes whether $\mathbf{TR1}$ is equivalent to $\mathbf{S4.4}$.

• Finally, I am trying to prove $\mathrm{4.4}$ in $\mathbf{TAR1}$, but it does not seem to be possible using only normal forms of degree $\le 3$. So, unless my calculations are wrong, either the proof involves modalities of degree 4, or $\mathbf{TAR1}$ is a distinct system. If distinct, then it would not include $\mathbf{S4}$.

Philosophically, this particular system may not be particularly relevant; but an answer would help me the algebraic properties of other similar systems that I'm analyzing.

$\mathbf{KT}+\mathbf{AR1}$ is strictly weaker than $\mathbf{KT}+\mathbf{4.4}$. Consider the Kripke frame that is the reflexive closure of the following graph (so that any model built on it is a model of $\mathbf{KT}$): $$\require{AMScd}\begin{CD} A @>>> B @>>> C \end{CD}$$ Then build a model on it with, say, the valuation such that $p$ holds at each of $A$ and $B$ while $\neg p$ holds at $C$, for every propositional variable $p$. If I'm not mistaken, $\mathbf{AR1}$ holds in the resulting model while $\mathbf{4.4}$ fails. Specifically, to see that $\mathbf{AR1}$ holds, note that the antecedent of it is false at $B$ and $C$, while at $A$ the consequent is true since $\square p$ holds. But $\mathbf{4.4}$ does not hold at $A$ in this model.
• As I understand this is because the frame, not only the model, validates $\mathrm{AR1}$, which is the case. It is valid in any reflexive frame where every world sees at most one other (different) world. This was somewhat unexpected, since this class of frames corresponds to $\mathbf{T}$ plus the following axiom: $$\mathrm{W2}: (p\land q)\rightarrow (\square(p\rightarrow q)\lor\square(q\rightarrow p))$$ But then I checked and $\mathrm{AR1}$ is indeed a theorem of $\mathbf{T}+\mathrm{W2}$. Since these frames are not transitive, they are not $\mathbf{S4.4}$ frames. Dec 28, 2013 at 15:52