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

Abstract

We present a justification logic corresponding to the modal logic of transitive closure ${\mathsf{K}}^{+}$ and establish a normal realization theorem relating these two systems. The result is obtained by means of a sequent calculus allowing non-well-founded proofs.

The proof of the main lemma at the end of the article contains some inaccuracies that were corrected in preparation of the journal version