Abstract
Justification logic began with Sergei Artemov’s work providing an arithmetic semantics for intuitionistic logic. As part of that work, a small number of explicit modal logics were introduced—logics in which there was a structure of terms that kept track of not just what was a necessary truth, but why it was necessary. These explicit modal logics were connected with standard modal logics such as S4, T, K, and others using Realization Theorems, essentially saying that modal operators concealed an underlying informational structure. Since Artemov’s work, the phenomenon of justification logic has turned out to be very broad. For instance, I have shown that infinitely many modal logics have justification counterparts. In this paper I will sketch the basics and try to give some of the ideas behind formal justification proofs, justification semantics, and realization theorems.