Realizations
In this chapter we will be following very different realization strategies from Chapter 6, and a different, recursive, characterization of realization will be useful. We begin with a pure language construct; issues of provability will be brought in later.
We assume we have a fixed set of propositional variables; exact details don't matter. This is enough to fully determine a modal language, but more than one justification language is possible because we can still vary our choice of justification operation symbols and justification constant symbols. Of course the choice of justification variables can also be an issue, but we avoid this with the following stipulation.
Variable Convention From now on we take
to be an enumeration
of all justification variables, with no justification variable repeated. This list is fixed once and for all.
Then only justification constants and function symbols are language dependent. Assume that some choice has been made, some set of justification terms has been specified, and a justification language is fixed.
We want to associate with each modal formula a set of potential realizers. As we said earlier, this is a purely linguistic issue. When, however, a specific modal logic and a specific justification logic are chosen, if a modal formula has a provable normal realization it is intended that such a realization should come from our associated set of potential realizers. The recursive Definition 7.4 is central to the algorithms and proofs that follow. But first we have some bookkeeping to take care of.
If X is a modal formula, a normal realization is sensitive to positive and negative occurrences of necessity operators. In Section 5.8 we introduced signed annotated formulas to assist with this issue of polarity, and that section should be reviewed now.
If X is a modal formula, we can turn it into an annotated formula in infinitely many ways—choose any one of them, say the result is Y. An annotated necessity operator in Y occurs positively (negatively) if it occurs positively (negatively) in the signed annotated formula F Y, as specified in Definition 5.17. So, the heart of our characterization of potential realizer is in terms of signed and annotated modal formulas. Essentially, Definition 5.17 is built directly into the definition of potential realizers.
We assume we have a full set of connectives,
though a
subset would do as well.
Definition 7.4 (Potential Realizers) The mapping
associates with each signed annotated modal formula a set of signed justification formulas called potential realizers. It is defined recursively, as follows. We use the enumeration, v1, v2,..., of justification variables noted earlier.
Members of
are called potential realizers of T Y, where TY is a T signed, annotated modal formula; and similarly for the F-signed case. A potential realizer of an unsigned annotated formula Y is any justification formula Z where FZ is a potential realizer for F Y. And finally, a potential realizer for a modal formula X that is not annotated is any potential realizer for Y where Y is any annotated version of X. (This involves an arbitrary choice of annotation, but different choices produce results that differ only in justification variable usage, something that is not significant here. We ignore the issue.) 
and it is this that we now compute.
Potential realizers have the properties that were set out in Definition 7.3 except, perhaps, for provability. Negative occurrences of necessity are replaced by justification variables because negative subformulas will be signed with T according to Definition 5.17, and these become justification variables by case (6) of Definition 7.4. Distinct occurrences of necessity become distinct variables because of the way justification variables are assigned, and the fact that in annotated formulas no annotation can occur twice. And finally, the forgetful functor has the appropriate behavior, by the following Theorem, which has a straightforward proof by induction on formula complexity.
Theorem 7.6 For any annotated formula
implies
7.4