WhatWeDoHere
In Chapter 6 we saw the first Realization Theorem, established with its first proof. Since then, not only have many realization proofs been created, but the realization phenomenon has also been found to apply across a much wider range of modal logics than had originally been contemplated.
Here and in Chapter 8 we examine this. In order to discuss what we will be doing, the diagram in Figure 7.1 will be helpful. The rest of this introductory section is devoted to explaining what it depicts.
Figure 7.1 Organization of This Chapter
The original definition for realizing a formula of S4 in LP easily extends to other modal/justification logic pairs. A formal definition is in Section 7.2. The original realization proof was immediately seen to cover well-known sublogics of S4—just leave out some of the machinery. But eventually extensions of S4 were also brought into the picture and things got more complicated. In particular, the original motivation connecting intuitionistic logic with arithmetic began to fade because extensions of S4 can embody principles that don't correspond to arithmetic facts. Still while the arithmetic connection may disappear, the idea of turning modal operators into explicit justification terms retains its interest.
An important feature of the original realization proof is the role played by the substitution of complex justification terms for justification variables. The same feature appears in several subsequent proofs and, in fact, cannot be avoided. But it can be separated out, using machinery that traces back to Fitting (2005), though the significance was not understood until later. In Fitting (2013b) the name Quasi-Realization was introduced. Quasi-realizations are similar to realizations but they have a more complex form.
Introducing them has two important benefits. First, when their existence can be established, doing so is substantially simpler than showing a similar result for realizations, insofar as it avoids any mention of substitution. In fact they still represent an embedding from a modal logic into a justification logic and can serve some of the functions that realizations were designed for, though they do not have the intuitive simplicity we would like from realization. The second important thing concerning them is that quasi-realizations can be converted into realizations— it is at this stage that substitution enters into things. Moreover this conversion can be done constructively. The algorithm for doing so proceeds by recursion on formula structure; it makes no use of the structure of cut-free proofs, or indeed, of proofs at all. And significantly, the conversion algorithm and its correctness proof can be given uniformly across all justification logics. This is shown here in Section 7.6 and is represented in Figure 7.1 by the arrow on the right.Then establishing the existence of realizations for a modal/justification logic pair reduces to a similar problem, but for quasi-realizations. The original work on LP was constructive, and this was important because of the connection with intuitionistic logic. In Fitting (2005) a nonconstructive argument was given, and it turned out to generalize to a large number of cases for which no constructive version is currently known. All this is represented in Figure 7.1 by the two arrows on the left.
Constructive proofs of the existence of quasi-realizers all involve cut-free proof systems of some kind. Originally the sequent calculus was used. In this chapter we use tableau systems, which we covered in Chapter 5. The change is primarily one of convenience because the two kinds of proof systems can be translated into each other. Nested sequents and hypersequents have also been used. We will give some references at the end of this chapter, in Section 7.13. We will show that a quasi-realization in a justification logic can be constructed from a cut-free modal tableau proof using any of the modal tableau proof procedures from Chapter 5. We will show this for S4 and leave it to the reader to check that similar arguments work in the other cases. As is indicated in Figure 7.1, this gives us realization constructively.
The nonconstructive realization proof for LP from Fitting (2005) was eventually shown to be very general, Fitting (2014a, 2016a, b). It is semantic based and makes use of the canonical model construction for Fitting models of justification logics, from Chapter 4. This gives us a highly uniform way of showing realization, indeed for an infinite number of cases, with the disadvantage that the results are not constructive. This is covered in Section 7.9, with a multiplicity of examples provided in Chapter 8.
7.2