Realization for LP

The formulation of LP and our earlier examples should have left an impres­sion that LP is something like an explicit version of S4. The main idea driv­ing the project that created the logic of proofs project was the observation that proof polynomials apparently denoted classical proof objects and a hope that LP indeed was capable of realizing derivations in S4 by recovering proof polynomials for every occurrence of modality.

The inverse operation to the realization of modalities of proof polynomials is the forgetful projection of LP-formulas to the modal formulas obtained by replacing all t:X’s by ?X^,s. It is easy to see that the forgetful projection of LP is S4-compliant. Let F° be the forgetful projection of F. By a straightforward induction on a derivation in LP one can show the following, though we omit explicit details.

Lemma 6.4

Our goal now is to establish the converse, that LP suffices to realize any theorem of S4.

By an LP-realization of a modal formula F we mean an assignment of proof polynomials to all occurrences of the modal operator in F along with a constant specification of all constants occurring in those proof polynomials. By F^r we understand the image of F under a realization r.

A sequent calculus for S4 is presented in Section 5.3. Chapter 5 also con­tains a discussion of positive and negative occurrences of modalities in a for­mula and in a sequent. Because we will be using sequent calculus language, GS4 in particular, in the realization algorithm below, for convenience we re­call the polarity definition for a modal formula F within a given sequent.

Now, here is realization as it was first stated and proved.

Theorem 6.5 Given a derivation S4 ' F one can recover a normal realiza­tion r such that LP ' F^r.

Proof We use the cut-free sequent formulation of S4 from Section 5.3, GS4. Without loss of generality we assume that axioms are atomic, i.e., sequents of

As an illustrative example that we will follow through the proof, consider the following specific cut-free GS4 derivation, where A and B are propositional letters.

There are two negative families, 1 and 2, and two essential positive families,

3 and 4.

Now the desired r will be constructed by stages I-III as described next. For the construction we reserve a large enough set of proof variables as provisional variables.

Stage I. For each negative family or nonessential positive family, pick a fresh proof variable x and replace all occurrencesin our running example, we get the following.

Stage II. Pick an essential family f, enumerate all the occurrences of rules () ?), which introduce boxes of this family. Let nf be the total number of such rules for f. Replace all boxes of f by the polynomial

where w_i’s are fresh provisional variables. The resulting tree T' is labeled by LP-formulas because all ?'s have been replaced by proof polynomials.

Stage III. Run a process going from the leaves of the tree to its root, which will update a constant specification CS and replace the provisional variables by proof polynomials of the usual variables from stage (I) and constants from CS as shown next. Simultaneously, by induction on the depth of a node in T^' we establish that after the process passes a node the sequent assigned to this node becomes derivable in LP(CS) for the current CS.

Because

in LP(CS),

We declare the sequent

Eventually, we substitute polynomials of nonprovisional variables for all provisional variables and build a realization of the root sequent of the proof tree derivable in LP(CS). Obviously, the realization r built by this procedure is normal.

We conclude the proof of the realization theorem by applying Stage III pro­cedure to our continuing example to realize the provisional variables. In the step

6.3