TR-2004011: Logic of Knowledge with Justifications from the Provability Perspective
Sergei Nikolaevich Artemov, Elena Nogina · CUNY Academic Works (City University of New York) · 2004
An issue of a logic of knowledge with justifications has been discussed since the early 1990s.Such a logic along with the usual knowledge operator 2F "F is known" should contain assertions t:F "t is an evidence of F".In this paper we build two systems of logic of knowledge with justifications: LPS4, which is an extension of the basic epistemic logic S4 by an appropriate calculus of evidences corresponding to the logic of proofs LP together with the principle that justification implies knowledge, and LPS4 -, which is LPS4 augmented by the mixed implicit/explicit negative introspection principle.We offer a provability semantics for LPS4 and LPS4 -where the epistemic modality 2F is interpreted as "F is true and provable" and the evidence assertions t:F as "t is a proof of F".We find Kripke semantics and establish a number of fundamental properties of LPS4 and LPS4 -.On the way to those systems we find the minimal joint logic of proofs and formal provability, LPGL, complete with respect to the standard provability semantics.