Gödel inaugurated a project of finding an arithmetic semantics for intuitionistic logic, but did not complete it. It was finished by Sergei Artemov, in the 1990’s. As part of this work, Artemov introduced the first justification logic, LP, (standing for logic of proofs). This is a propositional modal-like logic, with an infinite family of proof or justification terms. Ir can be seen as an explicit version of the well-known modal logic S4. There is a possible world semantics for LP (due to me). Since then, many other justification logic/modal logic pairs have been investigated, and justification logic has become a subject of independent interest, going beyond the original connection with intuitionistic logic. It is now known that there are infinitely many justification logics, but the exact extent of the family is not known.
Justification logics are connected with their corresponding modal logics via
Realization Theorems. A Realization Theorem connecting LP and S4 has a
constructive proof, but there are other cases for which realization holds, but it is not known if a constructive proof exists. In a sense, a realization of a modal theorem reflects the flow of information inherent in its formal proof. I will present a sketch of the basic ideas. I have an implementation of realization for S4 into LP available on my web page, but there will not be time to discuss it during the talk.