Logical Omniscience Via Proof Complexity

The Hintikka-style modal logic approach to knowledge has a well-known defect of logical omniscience, i.e., an 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 A of type `F is known' there is a proof of F in E, the complexity of which is bounded by some polynomial in the length of A. We show that the usual epistemic modal logics are logically omniscient (modulo some common complexity assumptions). We also apply LOT to Justification Logic, which along with the usual knowledge operator Ki(F) (`agent i knows F') contain evidence assertions t:F (`t is a justification for F'). In Justification Logic, 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 just...

• Type: Conference
• Year: 2006
• Where: CSL
• Authors: Sergei N. Artëmov, Roman Kuznets
• Keywords: Automated Reasoning, CSL 2006, Justification Logic, Logical Omniscience, Modal Logic