Putting Things Together

Theorem 7.22 tells us, nonconstructively, when provable quasi-realizers exist. Theorem 7.13 and its accompanying algorithm tells us how to convert a quasi- realizer to a realizer. Putting these together we get the following central result.

Theorem 7.24 (Realization, Nonconstructively) Let KL be a normal modal logic that is characterized by a class of frames F (KL). Let JL be a justification logic and CS be an axiomatically appropriate constant specification for it. If the canonical Fitting model for JL(CS) is based on a frame in F(KL) then every theorem of KL has a JL provable normal realizer.

7.13