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.



Is this system identical to S4.4?
$\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.


