Non-circular proofs and proof realization in modal logic

作者：Wang Ren June^*

来源：Annals of Pure and Applied Logic, 2014, 165(7-8): 1318-1338.

DOI：10.1016/j.apal.2014.04.004

• Justification logic
• Timed modal epistemic logic
• Modal logic
• Realization theorem
• Hilbert-style proofs

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%26apos;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 84 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 se, is introduced, which, under an adequate interpretation, is worth studying for its own sake.

• 出版日期2014-8