\[\mathcal{E}(t,X) \subseteq \mathcal{E}(!t,t{:}X)\] These conditions together entail the validity of \(t{:}X \rightarrow !t{:}t{:}X\) and produce a semantics for \(\mathsf{J4}\), a justification analog of \(\mathsf{K4}\), with a Realization Theorem connecting them. Adding reflexivity leads to a logic that is called \({\textsf{LP}}\) for historical reasons.