Abstract Justification awareness models (JAMs) were proposed by S. Artemov as a tool for modelling epistemic scenarios such as Russell’s prime minister example. It was demonstrated that the sharpness and the single-conclusion property of a model play an essential role in the epistemic usage of JAMs. The problem to axiomatize these properties using the propositional justification language was left opened. We propose the solution and define a decidable justification logic $\textsf{J}_{\textit{ref}}$ that is sound and complete with respect to the class of all sharp single-conclusion justification models. We also provide the complete axiomatizations for the classes of all single-conclusion justification models and all sharp justification models.

Abstract The formal system of intuitionistic epistemic logic (IEL) was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer–Heyting–Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. We prove that IEL is PSPACE-complete.

We propose an extension of the propositional proof logic language by the second-order variables denoting the reference constructors (like ‘the formula which is proven by x’). The proof logic in this weak second-order language is axiomatized via the calculus ref, the (Functional) Logic of Proofs with References. It is supplied with the formal arithmetical semantics: we prove that ref is sound with respect to arithmetical interpretations and is a conservative extension of propositional single-conclusion proof logic ⁠. Finally, we demonstrate how the language of ref can be used as a scheme language for arithmetic and provide the corresponding proof conversion method.