Justification logics, logics of knowledge, and conservativity (Q1028642): Difference between revisions

The author first reminds the reader of the axiomatizations of the main logics of knowledge, namely, \textbf{T} (in which agents have the ability to apply logical reasoning to their beliefs, which are necessarily true), \textbf{S4} (in which agents also know they know what they know), and \textbf{S5} (in which agents also know they don't know what they don't know). He then points to the problematic fact that they exhibit the property of logical omniscience (agents know all tautologies and know all logical consequences of what they know), and introduces justification logics, originating from Artemov's work on the arithmetic semantics of propositional intuitionistic logic, that make use of justification terms, to build formulas of the form \(t:X\) to intuitively express that \(t\) is a justification for proposition \(X\). Four operators can be applied to justification terms, with the following intended meanings: if \(t\) and \(u\) are justifications for \(X\) and \(X\supset Y\), respectively, then \(t\cdot u\) is a justification for \(Y\); if \(t\) and \(u\) are justifications for \(X\) and \(Y\), respectively, then \(t+u\) is a justification for both \(X\) and \(Y\); if \(t\) is a justification for \(X\) then \(!t\) is a justification for \(t:X\); and if \(t\) is not a justification for \(X\) then \(? t\) is a justification for \(\neg(t:X)\). Justification terms include constants, intended to justify what one wants to justify without further analysis, and their applicability determined by one of 3 axioms (depending on whether they can justify axioms only or also theorems, and on whether they can justify justified propositions). Capturing the intended meanings of these operators gives rise to axiomatic systems that parallel \textbf{T}, \textbf{S4} and \textbf{S5}. The author outlines the possible worlds semantics for justification logics he proposed in 2005, and discusses the difference between \textit{explicit} and \textit{implicit} knowledge: replacing in a formula of a justification logic every occurrence of a justification term by the modal operator \(K\) results in a formula in the corresponding modal logic of knowledge, which amounts to transforming explicit knowledge into implicit knowledge. Artemov's Realization Theorem shows that every theorem of \textbf{T}, \textbf{S4} and \textbf{S5} is the image of a theorem in the corresponding justification logic, meaning that explicit reasons can always be extracted from a theorem of a logic of implicit knowledge. The author then points to the main gap in the relationship, before presenting two new results. The first result involves a family of justification logics, represented as \(K(S)\), where \(S\) is a subset of \(\{+,\cdot,!,?\}\), indicating which operators on justification terms are kept -- three of those justification logics are the counterparts to \textbf{T}, \textbf{S4} and \textbf{S5}; it expresses that if \(S_1\) and \(S_2\) are two of those subsets with the property that \(S_1\nsubseteq S_2\), then \(K(S_2)\) is a conservative extension of \(K(S_1)\). The second result provides sufficient conditions for one justification logic \(J_1\) to embed another justification logic \(J_2\), with \(J_1\) and \(J_2\) taken from a set of 16 justification logics, in the sense that there exists a way to map constants of \(J_1\) to justification terms of \(J_2\) that converts each theorem of \(J_1\) into a theorem of \(J_2\). The paper ends with open questions.