Publication Date:
2012-09-25
Description:
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 $${\hbox{ LP }}_{L}^{\mathcal{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 .
Print ISSN:
0955-792X
Electronic ISSN:
1465-363X
Topics:
Computer Science
,
Mathematics
Permalink
