On Realization of S5-modality by Evidence Terms

摘要

We introduce a logic of evidence-based knowledge S5_nLP(S5) in which the evidence part is based on logic of proofs with negative checker LP(S5). The later is obtained from the Logic of proofs LP by adding a new unary operation of negative checker '?' and the corresponding axiom. We define Kripke-style models for S5_nLP(S5) and prove the completeness with respect to this semantics. We also define the logic of justified knowledge for S5_nLP(S5).