 Theorem 4: There is an algorithm which, for each modal formula \(F\) derivable in  \(\mathsf{K}\), assigns evidence terms to each occurrence of modality in \(F\) in such a way that the resulting formula \(F^{r}\) is derivable in  \(\mathsf{J}\). Moreover, the realization assigns evidence variables to the negative occurrences of modal operators in \(F\), thus respecting the existential reading of epistemic modality. 