Some Examples We Already Discussed

Scattered through earlier chapters were several examples of modal logic, justi­fication logic pairs that were said to be counterparts. We are now in a position to prove this properly.

K4³ and J4³ These were introduced in Section 2.7.1. K4³ is complete with re­spect to frames meeting thecondition. Discussion continued

in Section 4.3.3, and finally in Section 4.5.2 we showed the canonical model for J4³ has a frame meeting the K4³ condition. Then by Theorem 7.24, there is a realization result connecting J4³ and K4³.

S5 and JT45 These were introduced in Section 2.7.2, with soundness shown in Section 4.3.4 and completeness in Section 4.5.3. The canonical JT45 model is based on an S5 frame, so we have a realization connection.

Sahlqvist Examples Two examples that are in the Sahlqvist class were intro­duced in Section 2.7.3, with soundness shown in Section 4.3.5. The com­pleteness arguments in Section 4.5.4, along with Theorem 7.24, establish realization.

S4.2 and JT4.2 These were discussed in Sections 2.7.4,4.3.6, and 4.5.5. Modal completeness was shown by a canonical model construction. In the rest of the chapter this example will be greatly expanded, and realization will fol­low as a special case.

KX4 and JX4 These can be found in Sections 2.7.5, 4.3.7, and 4.5.6. The canonical completeness proof gives us realization in this case too.

8.2