Cut Elimination and Realization for Epistemic Logics with Justification

ISSN： 1465-363X

Source： Journal of Logic and Computation, Vol.22, Iss.5, 2012-10, pp. : 1171-1198

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

Epistemic logics with justification, S4LP and S4LPN, are combinations of the modal epistemic logic S4 and the Logic of Proofs LP, with some connecting principles. These logics together with the modal knowledge operator F (F is known), contain infinitely many operators of the form t :F (t is a justification for F), where t is a term. Regarding the Realization Theorem of S4, LP is the justification counterpart of S4, in the sense that, every theorem of S4 can be transformed into a theorem of LP (by replacing all occurrences of by suitable terms), and vise versa. In this article, we first introduce a new cut-free sequent calculus ${LP}_{L}^{G}$ for LP, and then extend it to obtain a cut-free sequent calculus for S4LP and a cut-free hypersequent calculus for S4LPN. All cut elimination theorems are proved syntactically. Moreover, these sequent systems enjoy a weak subformula property. Then, we show that theorems of S4LP can be realized in LP and theorems of S4LPN can be realized in JS5 (the justification counterpart of modal logic S5). Consequently, we prove that S4LP and S4LPN are conservative extensions of LP.