An extension of the logic of proofs with actions

Justification Logic is a family of modal logics in which the proof or justification of a necessitated proposition can be explicitly expressed. These logics can be considered as epistemic logics in which the justification (reason or evidence) for knowledge or belief of a proposition can be expressed in the language. In this paper, we study an extension of justification logics with actions. In particular, we extend the language of Artemov's logic of proofs with actions. To this end, we use the regular actions of propositional dynamic logic without the iteration operator. By combining the axiom system of the logic of proofs with that of propositional dynamic logic, we present an axiomatic proof system for this combined logic. We also present a possible world semantics, based on Kripke-Fitting models, for this combined logic, and prove the completeness theorem by means of the canonical model construction. We further establish the internalization property for this logic.