The standard axiomatization of the modal logic $\mathbf{S4}$ is given by \begin{equation*} \begin{split} &\Box(\varphi\rightarrow\psi)\rightarrow(\Box\varphi \rightarrow\Box\psi) \\ &\Box\varphi \rightarrow\Box\Box\varphi\\ &\Box\varphi \rightarrow\varphi \end{split} \qquad \begin{split} &\bf{(K)}\\ &\bf{(4)}\\ &\bf{(T)} \end{split} \end{equation*} with rules of inference
\begin{equation*} \begin{split} \{\varphi,\varphi\rightarrow\psi\}&\vdash \psi\\ \{\varphi\}&\vdash \Box\varphi \end{split} \qquad \begin{split} &\bf{(MP)}\\ &\bf{(N)}\\ \end{split} \end{equation*} for any well formed $\varphi,\psi$. In working on a project, I came across another axiomatization which states $\mathbf{S4}$ is equivalent to
\begin{equation*} \begin{split} &\Box \top \\ &\Box(\varphi\wedge \psi) \leftrightarrow \Box \varphi \wedge \Box \psi\\ &\Box\varphi \rightarrow\Box\Box\varphi\\ &\Box\varphi \rightarrow\varphi \end{split} \qquad \begin{split} &\bf{(N)}\\ &\bf{(R)}\\ &\bf{(4)}\\ &\bf{(T)} \end{split} \end{equation*} with rules of inference \begin{equation*} \begin{split} \{\varphi,\varphi\rightarrow\psi\}&\vdash \psi\\ \{\varphi\rightarrow\psi\}&\vdash \Box\varphi\rightarrow\Box\psi \end{split} \qquad \begin{split} &\bf{(MP)}\\ &\bf{(M)}\\ \end{split} \end{equation*} for any well formed $\varphi,\psi.$
However, I can't find any reference to this axiomatization in any of the classic modal logic text (Chellas, Cresswell & Hughes, Blackburn et al.).
Does anyone know of any references as to why these are equivalent, or proofs?
Three initial points:
First, the rules are crucially mis-stated. The necessitation rule N is not $$\{\varphi\} \vdash \Box\varphi$$ but rather $$\textrm{if } \vdash\varphi \textrm{ then }\vdash \Box\varphi,$$ and similarly for M. Getting this right will help!
Second reflect that $\varphi$ is provably equivalent to $(\top \to \varphi)$, and we see why M gives the rule N; while N plus K obviously gives M.
Third, it is a routine exercise to prove R in the first version of S4. So all that remains to show that these systems really are equivalent is to prove K in the second system ... (easier said than done?).