Non-circular proofs and proof realization in modal logic

In this paper a complete proper subclass of Hilbert-style S4 proofs, named non-circular, will be determined. This study originates from an investigation into the formal connection between S4, as Logic of Provability and Logic of Knowledge, and Artemov's innovative Logic of Proofs, LP, which later developed into Logic of Justification. The main result concerning the formal connection is the realization theorem  , which states that S4 theorems are precisely the formulas which can be converted to LP theorems with proper justificational objects substituting for modal knowledge operators. We extend this result by showing that on the proof level, non-circular proofs are exactly the class of S4 proofs which can be realized to LP proofs. In turn, this study provides an alternative algorithm to achieve the realization theorem, and a novel logical system, called S4ΔS4Δ, is introduced, which, under an adequate interpretation, is worth studying for its own sake.