Making knowledge explicit: How hard it is

Artemov's logic of proofs LP is a complete calculus of propositions and proofs, which is now becoming a foundation for the evidence-based approach to reasoning about knowledge. Additional atoms in LP have form t: F, read as “t is a proof of F” (or, more generally, as “t is an evidence for F”) for an appropriate system of terms t called proof polynomials. In this paper, we answer two well-known questions in this area. One of the main features of LP is its ability to realize modalities in any S 4 -derivation by proof polynomials thus revealing a statement about explicit evidences encoded in that derivation. We show that the original Artemov's algorithm of building such realizations can produce proof polynomials of exponential length in the size of the initial S 4 -derivation. We modify the realization algorithm to produce proof polynomials of at most quadratic length. We also found a modal formula, any realization of which necessarily requires self-referential constants of type c: A ( c ). This demonstrates that the evidence-based reasoning encoded by the modal logic S 4 is inherently self-referential.

Authors

• Vladimir Brezhnev
• Roman Kuznets

Keywords

• Logic of proofs
• Self-reference
• Modal logic