If this machinery is added to that for \(\mathsf{J4}\) we get the logic \(\mathsf{J45}\), a justification counterpart of \(\mathsf{K45}\). Axiomatic soundness and completeness can be proved. In a similar way, related logics \(\mathsf{JD45}\) and \(\mathsf{JT45}\) can be formulated semantically. A Realization Theorem taking the operator \(?\) into account was shown in (Rubtsova 2006).