A realization theorem for the modal logic of transitive closure \(\mathsf{K}^+\) (Q6970638)

Justification logics, introduced by \textit{S. N. Artemov} [Bull. Symb. Log. 7, No. 1, 1--36 (2001; Zbl 0980.03059)] for the modal logic S4, have since been developed for various modal logics, but realization theorems for common knowledge modal logics have remained elusive despite the existence of corresponding justification logics. This paper makes a significant contribution by establishing a normal realization theorem for the modal logic of transitive closure K\(^+\), a fixed-point logic (similar to the logic of common knowledge) where \(\Box^+A\) is the greatest fixed point of \(z \mapsto \Box A \wedge \Box z\), using a justification logic J\(^+\) with operators \([w]\) and \([s]_{tc}\) to explicitly represent epistemic justifications.\N\NThe use of a non-well-founded sequent calculus S, extended with annotated sequents and cyclic proofs, handles the infinitary nature of transitive closure, while the semantic completeness proof is accomplished via refutation trees. This approach, using bounding functions and injective substitutions, proves the theorem and suggests these methods could be used for common knowledge logics, advancing the explicit representation of epistemic structures in non-canonical modal settings.