Basic and Mkrtychev Models for the Logic of Proofs LP
The Logic of Proofs LP is historically the first justification logic. It occupies a prominent position in this area due to its arithmetical semantics and connections to the Brouwer-Heyting-Kolmogorov semantics for intuitionistic logic.
This warrants a special section devoted to basic and Mkrtychev semantics for LP.As we have seen in Section 2.6, LP is J4 with factivity t:F → F. The following is yet another Corollary of Theorem 3.14. showing that basic models for LP are J4-models with the factivity condition.
Corollary 3.23 The basic models for LP(CS), members of BM(LP(CS)), are the basic CS-models for J4 with factivity. LP(CS) is sound and complete with respect to BM(LP(CS)).
Mkrtychev models for LP are those for JT that are closed under the proof checking condition (3.1). An analogue of Theorem 3.21 holds for LP as well.
Theorem 3.24 For every Mkrtychev LP-model * there is a basic LP-model ∙ such that for each formula F,
Proof The proof is the same as the proof of Theorem 3.21, but in addition we have to verify the closure of ∙ with respect to the proof checking condition 
3.6