Logical Omniscience Via Proof Complexity

Abstract The Hintikka-style modal logic approach to knowledge contains a well-known defect of logical omniscience, i. e. , the unrealistic feature that an agent knows all logical consequences of her assumptions. In this paper, we suggest the following Logical Omniscience Test (LOT): an epistemic system E is not logically omniscient if for any valid in E knowledge assertion \(\mathcal{A}\) of type ‘ Fis known, ’ there is a proof of F in E, the complexity of which is bounded by some polynomial in the length of \(\mathcal{A}\). We show that the usual epistemic modal logics are logically omniscient (modulo some common complexity assumptions). We also apply LOT to evidence-based knowledge systems, which, along with the usual knowledge operator K i ( F ) (‘ agent i knows F ’), contain evidence assertions t: F (‘ t is a justification for F ’). In evidence-based systems, the evidence part is an appropriate extension of the Logic of Proofs LP, which guarantees that the collection of evidence terms t is rich enough to match modal logic. We show that evidence-based knowledge systems are logically omniscient w. r. t. the usual knowledge and are not logically omniscient w. r. t. evidence-based knowledge.

Authors

• Sergei N. Artëmov
• Roman Kuznets

Keywords

No keywords are indexed for this paper.