Counterparts

We have been talking about justification logics (such as LP) corresponding to modal logics (S4 in the case of LP). Here we say a little more about what this means, beginning with a simple mapping from the language(s) of justification logic to modal language.

We want to know the circumstances under which the set of theorems of a justification logic is mapped by the forgetful functor to exactly the set of theorems of a modal logic, something captured formally in the following.

Definition 7.2 (Counterparts) Suppose KL is a normal modal logic (thus ex­tending K) and JL is a justification logic. (That is, following Definition 2.6, JL extends axiomatic J₀ with additional axiom schemes and a constant specifica­tion.) We say JL is a counterpart of KL if the following holds.

In other words, JL is a counterpart of KL if the forgetful functor is a map­ping from the set of theorems of JL onto the set of theorems of KL (provided arbitrary constant specifications are allowed).

7.3