  Although an arithmetic semantics is not possible, in (Fitting 2008) a possible world semantics, and an axiomatic proof theory, was given for  a version of \(\mathsf{LP}\) with quantifiers ranging over justifications. Soundness and completeness  were proved. At this point possible world semantics separates from  arithmetic semantics, which may or may not be a cause for alarm. It  was also shown that  \(\mathsf{S4}\)  embeds into the quantified logic by translating \(\Box Z\) as “there exists a justification \(x\)  such that \(x : Z^{*}\),” where  \(Z^{*}\) is the translation of \(Z\). While this  logic is somewhat complicated, it has found applications, e.g., in  (Dean and Kurokawa 2009b) it is used to analyze the Knower Paradox,  though objections have been raised to this analysis in (Arlo-Costa  and Kishida 2009).