Completeness Examples
We resume our examination of the justification logic examples that we first looked at axiomatically in Section 2.7, then again in Section 4.3 where semantics were given and soundness was established.
Now we show completeness with respect to appropriate Fitting model classes. For each example we begin with references to the earlier discussions of the logic involved.4.5.1 LP and Sublogics
(Continuing 2.6 and 4.3.2.)
We concentrate on completeness for LP because showing it for J, JD, JT, J4, and JD4 can be done by omitting parts of the argument. Given the work in Section 4.4.2, all that needs to be shown for LP is that the canonical model 
4.5.2 J43
(Continuing 2.7.1 and 4.3.3.)
4.5.3 JT45
(Continuing 2.7.2 and 4.3.4.) 
4.5.4 Sahlqvist Examples
(Continuing 1.13 and 4.3.5.) 
4.5.5 S4.2 and JT4.2
(Continuing 2.7.4 and 4.3.6.)
The logics S4.2 and J4.2 are especially important in this book because, as we will see in Chapter 8, they are representative cases of very general families. Because our full arguments will be generalizations of those that work for S4.2 and J4.2, we present these cases in detail, beginning with a completeness proof for the modal logic S4.2.
If this work is understood, the generalizations should be much easier to follow.
Lemma 4.14
be the canonical model for any normal 
Figure 4.1 Obtaining the Convergent Condition for S4.2
Having shown the modal case, we now turn to completeness for the justification logic J4.2. For this we need the special assumption that we have internalization, which we have if there is an axiomatically appropriate constant specification. Such an assumption was not needed for the justification logics we discussed previously, but it comes in when we prove an analog of Lemma 4.14.
Lemma 4.15 Suppose Γ is a possible world in the canonical Fitting justifi
Unlike with the Otherjustification logics considered earlier, we do not prove completeness of JX4 now. It is an instance of a very general family that will be investigated in Chapter 8, as are several other justification logics we have looked at. Unlike those other justification logics, however, a direct proof of completeness for JX4 requires us to bring in much of the machinery of the general argument of Chapter 8, meaning that many things would be presented twice. What we have chosen to do instead is give a completeness proof for the modal logic KX4. This is uncluttered enough to be considered at this point, yet the proof has the benefit that it will serve to motivate some of the features of the general argument later on. So, for the rest of this section we work with axiomatic KX4, for which the modal semantics requires transitivity and denseness.
Lemma 4.16 Assume Γ and A are sets Ofmodalformulas that are maximally consistent in KX4. 
4.6