Labeled sequent calculus for justification logics (Q331048)

Justification logics, emerging from the Logic of Proofs (LP) introduced by \textit{S. N. Artemov} [Bull. Symb. Log. 7, No. 1, 1--36 (2001; Zbl 0980.03059)], are modal-like logics whose language includes formulas of the form $t:A$, meaning ``the term $t$ provides a justification for the truth of the formula $A$''. This paper develops calculi for several justification logics: the basic justification logics J corresponding to the modal logics K, its extensions by various combinations of axioms corresponding to the common modal axioms T, D, 4, B, and 5 (including the original logic LP = JT4), and the combined modal-justification logics that extend each of the logics above with an explicit $\square $ operator. \par The calculi provided are labelled sequent calculi in the style of \textit{S. Negri} [J. Philos. Log. 34, No. 5--6, 507--544 (2005; Zbl 1086.03045)], whose language internalizes Kripke-Fitting semantics [\textit{M. Fitting}, Ann. Pure Appl. Logic 132, No. 1, 1--25 (2005; Zbl 1066.03059)] for the logics in question. The author proves admissibility of cut and other structural rules in the calculi, and their completeness. It is shown that some of the calculi are analytical in the sense that they enjoy suitable subformula, subterm, and sublabel properties.