Proving Realization Constructively
We have shown that establishing the existence of a quasi-realizer is sufficient for a realization result because these convert to realizers. We now start filling in the details of the upper left arrow in Figure 7.1, constructively converting a modal tableau proof into a quasi-realization.
Unlike the original proof given in Chapter 6, the construction used now proceeds one proof step at a time. Details vary from logic to logic. We present things for S4 and LP; small and obvious changes adapt the work to any of the logics discussed in Section 5.7.If there is an S4 tableau proof, it can be annotated, see Section 5.8. The result can then be turned into an annotated block tableau, see Section 5.9. All this is preprocessing. Now we describe how a closed S4 annotated block tableau T can be converted into what we call a justification sound quasi-realization Tree, something that will let us read off a potential quasi-realizer that is provable in LP, corresponding to the formula that the S4 tableau proves.
Definition 7.16 (Quasi-Realization Tree) Suppose T is an annotated block
7.8