For a justification analog of \({\textsf{K4}}\) an additional unary operator ‘!’ is added to the term language, see Section 2.5. Recall this operator maps justifications to justifications, where the idea is that if \(t\) is a justification for \(X\), then \(!t\) should be a justification for \(t{:}X\). Semantically this adds conditions to a model \(\mathcal{M} = \langle \mathcal{G},\mathcal{R},\mathcal{E},\mathcal{V}\rangle\), as follows.