Realizations, Nonconstructively
We now fill in the details of the last part of Figure 7.1, the lower left. Constructive proofs of the existence of realizations have all been tied to cut-free proof systems, and thus they are limited to modal logics for which such proof systems are known to exist.
There is also a nonconstructive approach that is very general in its applicability. The argument was implicit in Fitting (2005), and clarified in Fitting (2014a, 2016a). In what was something of a surprise, the family of modal logics having justification counterparts turns out to be infinite. We give the central theorem here, and the entire of the next chapter is devoted to examples illustrating its use. Because of Corollary 7.15, it is enough to show the existence of quasi-realizations.Theorem 7.22 (Nonconstructive Quasi-Realization Theorem) Let KL be a normal modal logic characterized by a class of frames F (KL). Let JL be a justification logic, CS be a constant specification for it, and assume JL(CS) has the internalization property. Ifthe canonical Fitting model (Section 4.4.2) for JL(CS) is based on a frame in F(KL), then every validity of KL has a quasi-realization provable in JL(CS).
This is case (1); case (2) is similar.
7.12