Certifying Logic Research

Justification Logic is based on classical propositional logic augmented by justification assertions t:F that read t is a justification for F. This essay is on the history and theoretical results of justification logic, and the significance of mainstream epistemology.G(o|¨)del's paper (1933) left two problems concerning (1) the exact intended semantics of G?del's provability calculus S4, and (2) the modal logic of the formal provability predicate"Provable(F)". The solution to the first problem led to LP (the first logic of justification). Several justification logics have been created, starting with the logic LP.These can be thought of as explicit versions of modal logics, or of logics of knowledge, in which the unanalyzed necessity (knowledge) operator has been replaced with a family of explicit justification terms. We sketch the basics of justification logics and their relations with modal logics. Then we move to new technical aspects. Modal logics come in various strengths. For their corresponding justification logics, what we show here is that for justification logics corresponding to modal logics extending T, various familiar extensions are actually conservative with respect to each other.