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 S4-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 S4-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 S4 is inherently self-referential.