The logic of justified belief, explicit knowledge, and conclusive evidence (Q392273)

The aim of the paper is to develop a \textit{theory of explicitly justified knowledge based on the actual availability of conclusive evidence}. It consists of a logical propositional framework built over [\textit{A. Baltag} et al., Lect. Notes Comput. Sci. 7456, 168--190 (2012; Zbl 1362.03012)], with two modal operators \(K\) and \(\square\), with \(K\varphi\) meant to capture that \(\varphi\) follows from the ``hard'' information received by an underlying agent, and \(\square\varphi\) meant to capture that the agent defeasibly knows \(\varphi\). Semantically, given a set of possible worlds \(W\) and \(w\in W\), \(K\varphi\) is true at \(w\) if \(\varphi\) is true at \(v\) for all \(v\in W\) with \(v\sim w\) where \(\sim\) is an equivalence relation over \(W\) (\(v\sim w\) indicates that \(v\) and \(w\) cannot be distinguished under the currently available information), and \(\square\varphi\) is true at \(w\) if \(\varphi\) is true at \(v\) for all \(v\in W\) with \(w\geq v\), where \(\geq\) is a preorder relation over \(W\) (\(w\geq v\) indicates that \(v\) is at least as plausible as \(w\)); worlds \(\sim\)-equivalent are supposed to be \(\geq\)-comparable, and conversely. The language also contains terms built over the set of terms of the form \(c_\varphi\), where \(\varphi\) is a propositional formula, and closed under two operators, \(\cdot\) and \(+\). Such a term \(t\) is supposed to represent a piece of evidence in favour of a formula \(\varphi\), denoted \(t\gg\varphi\). A term of the form \(c_\varphi\) is referred to as a \textit{certificate for \(\varphi\)}, and represents a ``canonical'' piece of evidence in support of \(\varphi\), so \(c_\varphi\gg\varphi\); if \(t\gg\varphi\Rightarrow \psi\) and \(s\gg\varphi\) then \(t\cdot s\gg\psi\); if \(t\gg\varphi\) and \(s\gg\psi\) then \(t+s\gg\varphi\) and \(t+s\gg\psi\); \(\gg\) is the \(\subseteq\)-smallest relation satisfying the previous conditions. Finally, and crucially for this work, the logical language encompasses formulas of the form \(Et\) meant to capture ``\textit{explicit goodness}'' of \(t\), because: (i) the agent has actually observed all the certificates which are part of \(t\), and (ii) the agent has actually constructed \(t\) as an argument. Semantically, \(E\) maps every possible world to a set of terms, with the properties that for all \(w\in W\): \(c_\top\) in \(E(w)\) (Trivial Evidence for the tautology \(\top\)), \(c_\varphi\in E(w)\) whenever \(t\in E(w)\) and \(t\gg\varphi\) (Certification of Evidence), \(t,s\in E(w)\) whenever \(t\cdot s\in E(w)\) or \(t+s\in E(w)\) (Subterm Closure), and for all \(w'\in W\) with \(w'\sim w\) and \(t,s\in E(w')\), \(t\cdot s\in E(w')\) and \(t+s\in E(w')\) whenever \(t\cdot s\in E(w)\) and \(t+s\in E(w)\), respectively (Availability of Evidence). Using \(B\varphi\) as an abbreviation for \(\lozenge\square\varphi\) to capture a notion of \textit{implicit belief}, \(B^e\varphi\), \(\square^e\varphi\) and \(K^e\varphi\) are defined as \(B(E c_\varphi)\), \(\square(E c_\varphi)\) and \(K(E c_\varphi)\) to capture notions of \textit{explicit belief}, \textit{explicit defeasible knowledge} and \textit{explicit information}, respectively. Along the same lines, notions of \textit{justification} and \textit{conditional beliefs} are defined with both ``implicit'' and ``explicit'' versions. The authors provide intuitions to help understand what these subtle notions mean and do not mean, before proving a number of validities and non-validities in relation to certain principles from Artemov and Fitting's justification logic. Then they prove a soundness and completeness result for their logic, show that it satisfies the finite model property, and establish some \textit{internalization} properties, which intuitively express that any proof of a formula \(\varphi\) may be represented as a term \(t\) to which the logic accords status as justification for \(\varphi\). Finally, the authors formalise in their setting and analyse two examples, the first of which is due to Edmund Gettier and runs as follows. ``The agent has a justified belief that \(f\): `Jones owns a Ford'. Indeed, she has seen Jones driving a Ford, Jones told her that it is his car and showed her the car ownership papers, etc. If \(c_f\) is the totality of the evidence in favor of \(f\) possessed by the agent, then \(c_f\) looks pretty conclusive, and if it were legitimate then it would certainly support \(f\). So the agent accepts this evidence (believes it to be good): \(B^e f\). However, unknown to the agent, \(c_f\) is not legitimate: the car papers are fake and in fact Jones does not own a Ford (but only borrowed one from a friend).'' The paper ends with considerations on logical omniscience. The authors argue that implicit attitudes of belief, knowledge, and information suffer from many forms of omniscience; however, their explicit notions can be controlled (by careful definition of the good-evidence availability function \(E\)) to avoid them if it is so desired.