Realization for justification logics via nested sequents: modularity through embedding (Q435202)

The language of justification logic makes it possible to replace a single modality \(\square A\) intended to formalize the term, for instance, `\(A\) is provable' by a family of the corresponding justification counterparts \(t\!:\kern-2.6pt A\) formalizing the term `\(t\) is a proof for \(A\)' or `\(A\) is known for reason \(t\)'. In this way, justification logic, introduced and developed by \textit{S. N. Artemov} [Bull. Symb. Log. 7, No. 1, 1--36 (2001; Zbl 0980.03059); Rev. Symb. Log. 1, No. 4, 477--513 (2008; Zbl 1205.03027)], studies the operational content of modality in various modal logics. The authors develop a method for testing whether a given set of operations on justification is sufficient to represent a given modal logic defined by means of a cut-free modal nested sequent system, and apply it to study comparative strengths of several such sets of operations. The notion of Fitting's embedding of justification logics is generalized making it possible to extend the authors' realization theorem to all natural justification counterparts. This approach gives the uniform realization theorem, covering all the 15 modal logics from the modal cube, as the central result of the paper.