1:
2: \section{Introduction}
3: \label{intro-sec}
4:
5: This paper explores the proof-theoretic interaction between
6: the goal-directed application of logical inferences and
7: \emph{information-flow}---that is, the possible connections between
8: assumptions and conclusions in proofs. My own starting-point for
9: this exploration was the result of \cite{permute-paper}, that
10: intuitionistic sequent calculi can be formulated so as exhibit the
11: characteristically intuitionistic \emph{modular} information-flow
12: (as underlying the correspondence between proofs and programs
13: \cite{howard:iso}, for example) while nevertheless allowing logical
14: inferences to be applied in any order whatsoever. This raises the
15: question whether it is possible to enforce this kind of modularity
16: \emph{incrementally} during goal-directed proof search. Of course,
17: the well-known flexibility of deduction in nonclassical logics
18: \cite{fitting:tableau,fitting:proof,wallen:nonclassical} is ample
19: motivation for the question.
20:
21: \subsection{Problem Statement}
22: \label{problem-subsec}
23:
24: I begin by delineating the focus of the paper more precisely.
25: I will work with a family of first-order multi-modal logics in this
26: paper. The generalization from intuitionistic logic reflects the
27: utility of more general ways of structuring logical specifications
28: \cite{baldoni/giordano/martelli:modal,baldoni:jlc98}, as well as
29: the broader importance of expressive modality in practical
30: knowledge representation \cite{mccarthy:notes,mccarthy:no}.
31: Qualitatively, what distinguishes the logics I consider (for which
32: formal definitions are provided in Section~\ref{logic-sec}) is that
33: they permit rules of modal inference to be formulated in two
34: equivalent ways
35: \cite{fitting:tableau,fitting:proof,wallen:nonclassical}. I
36: illustrate the alternatives for the case of S4, a logic that we can
37: perhaps regard as the pure modal logic of local and global modular
38: assumptions \cite{giordano/martelli:structuring}.
39:
40: \subsubsection{Structural scope and modularity}
41: \label{structure-subsubsec}
42:
43: The first formulation of modal inference is illustrated by the
44: sequent inference figure below:
45: %
46: \[
47: \derivi{$(\proveslabel\Box)$}
48: {\Gamma^* \proveslabel G, \Delta^*}
49: {\Gamma \proveslabel \Box G, \Delta}
50: \]
51: %
52: Such inferences set up a discipline of structural scope in
53: proofs. Read upward, as a description of proof search, the figure
54: describes how to accomplish generic reasoning about a modal
55: context, such as the conclusion $\Box G$ here. We have to
56: transform the sequent we are considering, by restricting our
57: attention just to the generic modal statements in the sequent.
58: Specifically, $\Gamma^*$ contains the formula occurrences of the
59: form $\Box A$ in $\Gamma$, and $\Delta^*$ contains the formula
60: occurrences of the form $\Diamond A$ in $\Delta$. The effect of
61: the transformation is that we move from our current scope into a
62: new, nested scope in which just generic information is available.
63: Figure~\ref{structure-scope-fig} illustrates all the
64: structurally-scoped S4 sequent inferences that I will draw on in
65: this motivating discussion; I refer the reader to
66: \cite{fitting:proof,wallen:nonclassical} for more
67: details on structurally-scoped proof.
68: %
69: \begin{figure}
70: \[
71: \begin{array}{c}
72: \derivi{$(\proveslabel\Box)$}
73: {\Gamma^* \proveslabel G, \Delta^*}
74: {\Gamma \proveslabel \Box G, \Delta}
75: \\
76: \derivi{$(\Box\proveslabel)$}
77: {\Gamma, G \proveslabel \Delta}
78: {\Gamma, \Box G \proveslabel \Delta}
79: \\
80: \derivi{$(\proveslabel\imp)$}
81: {\Gamma, P \proveslabel G, \Delta}
82: {\Gamma \proveslabel P \imp G, \Delta}
83: \\
84: \derivii{$(\imp\proveslabel)$}
85: {\Gamma \proveslabel G, \Delta}
86: {\Gamma, P \proveslabel \Delta}
87: {\Gamma, G \imp P \proveslabel \Delta}
88: \\
89: \derivii{$(\vee\proveslabel)$}
90: {\Gamma, A \proveslabel \Delta}
91: {\Gamma, B \proveslabel \Delta}
92: {\Gamma, A \vee B \proveslabel \Delta}
93: \\
94: \derivii{$(\proveslabel\wedge)$}
95: {\Gamma \proveslabel A, \Delta}
96: {\Gamma \proveslabel B, \Delta}
97: {\Gamma \proveslabel A \wedge B, \Delta}
98: \\
99: \Gamma, A \proveslabel A, \Delta \;\;\; (\m{Axiom})
100: \end{array}
101: \]
102: \caption{Six inference figures and the axiom for structurally-scoped
103: S4. After \cite{fitting:proof,wallen:nonclassical}. Sequents are
104: multisets of modal formulas; this formulation (though not others
105: that we will consider later) requires a structural rule of
106: contraction. See Section~\ref{logic-sec}.}
107: \label{structure-scope-fig}
108: \end{figure}
109:
110: The ability to define structural scope is intimately connected
111: with the ability to describe modular and local reasoning. In
112: specifying reasoning, we can think of antecedent formulas in
113: sequents as program statements and succedent formulas in
114: sequents as goals. In modal logics with structural scope, a
115: necessary goal $\Box G$ can be seen as a {\it modular} goal
116: because, as enforced by the structurally-scoped inference figure,
117: only program statements of the form $\Box P$ can contribute to its
118: proof. In other words, we cannot use the entire program to prove
119: $G$; rather, we must use a designated \emph{part} of the program:
120: formulas of the form $\Box P$. This is the \emph{module} we use to
121: prove $G$. Multi-modal logic allows us to name modules in a
122: general way \cite{baldoni/giordano/martelli:modal,baldoni:jlc98}.
123:
124: In fragments of logic without the operator $\Diamond$,
125: including S4 translations of intuitionistic formulas in particular,
126: modularity brings \emph{locality}. A goal $\Box(P \imp G)$
127: introduces a {\it local} assumption $P$. The assumption is local
128: in the sense that it can only contribute to the proof of $G$, and
129: cannot contribute to any other goal. We can motivate this locality
130: in logical terms by examining the sequent inferences for
131: $(\proveslabel\Box)$ and $(\proveslabel\imp)$ in combination:
132: %
133: \[
134: \derivi{$(\proveslabel\Box)$}
135: {\derivi{$(\proveslabel\imp)$}
136: {\Gamma^*, P \proves G}
137: {\Gamma^* \proves P \imp G}}
138: {\Gamma \proves \Box (P \imp G), \Delta}
139: \]
140: %
141: Observe that this logical fragment is constructed so that the
142: succedent context $\Delta^*$ above $(\proveslabel\Box)$ is empty,
143: and so we introduce $P$ into a subproof where $G$ is the only goal.
144:
145: Logical modularity and locality underlie the use of the proof
146: theory of modal logic as a declarative framework for structuring
147: specifications, and thereby facilitating their design and reuse
148: \cite{dale:modules,giordano/martelli:structuring,baldoni/giordano/martelli:modal,bgm:framework,baldoni:jlc98}.%
149: %
150: \footnote{
151: The model theory of modal logic can also be used to structure
152: specifications \cite{sakakibara:iclp87}.
153: }
154: %
155: Concretely, a goal that specifies the part of the program to
156: be used in its proof will give rise to the same operational
157: behavior when other parts of the program change. In this paper, I
158: further emphasize that logical modularity and locality provide
159: declarative tools for constraining the complexity of proof search
160: itself. My motivating example is the proof in
161: Figure~\ref{structure-module-fig}, which establishes that the
162: conclusion
163: \[
164: (\Box A) \wedge (\Box C)
165: \]
166: follows from the assumptions
167: \[
168: \Box(A \vee B), \Box(C\vee D), \Box(B \imp A), \Box(D\imp C)
169: \]
170: %
171: \begin{figure}
172: \small
173: \begin{center}
174: \makebox[0in]{
175: $\derivii{$(\proveslabel\wedge)$}
176: {\derivi{$(\proveslabel\Box)$}
177: {\derivi{$(\Box\proveslabel)$}
178: {\derivii{$(\vee\proveslabel)$}
179: {A, \ldots \proves A}
180: {\derivi{$(\Box\proveslabel)$}
181: {\derivii{$(\imp\proveslabel)$}
182: {B, \ldots \proves B, A}
183: {A, \ldots \proves A}
184: {B, B \imp A, \ldots \proves A}}
185: {B, \Box (B \imp A), \ldots \proves A}}
186: {A \vee B, \Box (B \imp A), \ldots \proves A}}
187: {\Box (A \vee B), \Box (B \imp A), \ldots \proves A}}
188: {\Box (A \vee B), \Box (B \imp A), \ldots \proves \Box A}}
189: %
190: {\derivi{$(\proveslabel\Box)$}
191: {\derivi{$(\Box\proveslabel)$}
192: {\derivii{$(\vee\proveslabel)$}
193: {C, \ldots \proves C}
194: {\derivi{$(\Box\proveslabel)$}
195: {\derivii{$(\imp\proveslabel)$}
196: {D, \ldots \proves D, C}
197: {C, \ldots \proves C}
198: {D, D \imp C, \ldots \proves C}}
199: {D, \Box (D \imp C),
200: \ldots \proves C}}
201: {C \vee D, \Box (D \imp C),
202: \ldots \proves C}}
203: {\Box (C \vee D), \Box (D \imp C), \ldots \proves C}}
204: {\Box (C \vee D), \Box (D \imp C), \ldots \proves \Box C}}
205: {\Box (A \vee B), \Box (C \vee D), \Box (B \imp A), \Box (D
206: \imp C) \proves (\Box A) \wedge (\Box C)}
207: $}
208: \end{center}
209: \caption{This structurally-scoped S4 proof shows how the locality of
210: modular assumptions limits the possible interactions in proof.
211: Ellipses mark points in sequents where I have suppressed additional
212: formula occurrences that no longer contribute to the inference.}
213: \label{structure-module-fig}
214: \end{figure}
215:
216: The assumptions in this proof---the program
217: statements---specify two ambiguities. Either $A$ or $B$ holds, and
218: either $C$ or $D$ holds. As part of the specification, we use
219: modal operators to say how to reason with these ambiguities: we
220: have $\Box (A\vee B)$ and $\Box(C \vee D)$. This means that the
221: ambiguities themselves are \emph{generic}; we can use them to
222: perform case analysis at any time. However, when we reason about
223: any particular case, we make \emph{local} assumptions---we will
224: assume $A$ rather than $\Box A$ for example.
225:
226: This specification limits the way case analyses in the proof
227: interact. Consider our goal here: $(\Box A) \wedge (\Box C)$. We
228: must prove each conjunct separately, \emph{using generic
229: information}; that is, each conjunct is proved in its own new
230: nested scope. Thus, in the proof of
231: Figure~\ref{structure-module-fig}, we perform case analysis from
232: $\Box(A \vee B)$ within the nested scope for $\Box A$, and perform
233: case analysis from $\Box(C \vee D)$ within the nested scope for
234: $\Box C$. Observe that the logic dictates the choice for us. For
235: instance, performing case analysis from $\Box(A \vee B)$ within the
236: nested scope for $\Box C$ is useless---the assumption of $A$ and
237: $B$ cannot help here. Importantly, performing case analysis from
238: $\Box(A \vee B)$ at the initial, outermost scope is also useless.
239: Whatever assumptions we make will have to be discarded when we try
240: to prove the conjuncts, and consider only generic information.
241: This specification therefore cordons off the two ambiguities from
242: one another in this proof problem. We have to consider the
243: ambiguities separately.
244:
245: Effectively, it is part of the \emph{meaning} of the
246: specification of Figure~\ref{structure-module-fig} that proofs must
247: be short. A proof in this specification must be a combined record
248: of independent steps, not an interacting record with combined
249: resolutions of ambiguities. To my knowledge, the possibility for
250: this kind of declarative search control in disjunctive modal
251: specifications has not received comment previously. But it seems
252: to me to be one of the most exciting and unique uses for modal
253: logic in representation and problem-solving.
254:
255: \subsubsection{Explicit scope and goal-directed search}
256: \label{explicit-subsubsec}
257:
258: The second formulation of modal reasoning is illustrated by
259: the sequent figure below:
260: %
261: \[
262: \derivi{$(\proveslabel\Box)$}
263: {\Gamma \proves G^{\mu\alpha}, \Delta}
264: {\Gamma \proves \Box G^{\mu}, \Delta}
265: \]
266: %
267: Such inferences institute an explicitly-scoped sequent
268: calculus; each formula is tagged with a label indicating the modal
269: context which it describes. These labels are sequences of terms,
270: each of which corresponds to an inference that changes scope.
271: Superscripts are my notation for labels; above, $\mu$ labels the
272: scope of the succedent formula $\Box G$. To reason about a generic
273: modal formula, we again introduce a new, nested scope in which just
274: generic information is available; we now label the formula with its
275: new scope. Thus above $G$ is labeled $\mu\alpha$; and $\alpha$ is
276: subject to an eigenvariable condition---it cannot occur elsewhere
277: in the sequent---and so represents a generic possibility. At
278: axioms, the scopes of premises and conclusions must match;
279: therefore modal inferences can dispense with destructive
280: transformation of sequents.
281:
282: Figure~\ref{explicit-scope-fig} illustrates the other
283: explicitly-scoped S4 sequent inferences that I will draw on in this
284: motivating discussion.
285: %
286: \begin{figure}
287: \[
288: \begin{array}{c}
289: \derivi{$(\proveslabel\Box)$}
290: {\Gamma \proveslabel G^{\mu\alpha}, \Delta}
291: {\Gamma \proveslabel \Box G^{\mu}, \Delta}
292: \\
293: \derivi{$(\Box\proveslabel)$}
294: {\Gamma, G^{\mu\nu} \proveslabel \Delta}
295: {\Gamma, \Box G^{\mu} \proveslabel \Delta}
296: \\
297: \derivi{$(\proveslabel\imp)$}
298: {\Gamma, P^{\mu} \proveslabel G^{\mu}, \Delta}
299: {\Gamma \proveslabel P \imp G^{\mu}, \Delta}
300: \\
301: \derivii{$(\imp\proveslabel)$}
302: {\Gamma \proveslabel G^{\mu}, \Delta}
303: {\Gamma, P^{\mu} \proveslabel \Delta}
304: {\Gamma, G \imp P^{\mu} \proveslabel \Delta}
305: \\
306: \derivii{$(\vee\proveslabel)$}
307: {\Gamma, A^{\mu} \proveslabel \Delta}
308: {\Gamma, B^{\mu} \proveslabel \Delta}
309: {\Gamma, A \vee B^{\mu} \proveslabel \Delta}
310: \\
311: \derivii{$(\proveslabel\wedge)$}
312: {\Gamma \proveslabel A^{\mu}, \Delta}
313: {\Gamma \proveslabel B^{\mu}, \Delta}
314: {\Gamma \proveslabel A \wedge B^{\mu}, \Delta}
315: \\
316: \Gamma, A^{\mu} \proveslabel A^{\mu}, \Delta \;\;\; (\m{Axiom})
317: \end{array}
318: \]
319: \caption{Six inference figures and the axiom for explicitly-scoped S4.
320: See \cite{fitting:proof,wallen:nonclassical,permute-paper}. The
321: $(\proveslabel\Box)$ inference is subject to an eigenvariable
322: condition that $\alpha$ is new. In the $(\Box\proveslabel)$
323: inference, $\mu\nu$ refers to any sequence of terms that extends
324: $\mu$ by a suffix $\nu$.}
325: \label{explicit-scope-fig}
326: \end{figure}
327: %
328: Explicitly-scoped proof systems have a long history as
329: \emph{prefixed tableaus}; see
330: \cite{fitting:proof,wallen:nonclassical} and references therein.
331: Each label sequence can be viewed as representing a possible world
332: in possible-worlds semantics, so for example the
333: $(\proveslabel\Box)$ inference figure represents a transition from
334: the world named by $\mu$ to a new world $\mu\alpha$ that represents
335: a generic possibility accessible from $\mu$. The more general
336: study of such systems has put them in a new proof-theoretic
337: perspective recently. They are closely related to semantics-based
338: translation systems \cite{ohlbach:translation,nonnengart:ijcai} and
339: \emph{labelled deductive systems}
340: \cite{gabbay:lds,basin/matthews/vigano:jlli98}. I use the term
341: \emph{explicitly-scoped} from \cite{permute-paper} because I
342: continue to emphasize the extent to which the two formulations of
343: reasoning represent the same inferences, just in different ways.
344:
345: The ability to define explicit scope is intimately connected
346: with the ability to carry out goal-directed proof. I adopt the
347: perspective due to \cite{mnps:uniform} that goal-directed proof
348: simply amounts to a specific strategy for constructing sequent
349: calculus deductions. The strategy is first to apply inferences
350: that decompose goals to atoms and then to apply inferences that use
351: a specific program statement to match a specific goal. Proofs that
352: respect this strategy are called \emph{uniform}. On this strategy,
353: logical connectives amount to explicit instructions for search, and
354: this is in fact what lets us view a logical formula concretely as a
355: \emph{program} \cite{mnps:uniform}.
356:
357: Unlike other, more procedural characterizations of algorithmic
358: proof, such as \cite{gabbay:htcs92}, this view largely abstracts
359: away from the exact state of computations during search. The key
360: questions are purely proof-theoretic. In particular, goal-directed
361: proof is possible in a logic if and only if any theorem has a
362: uniform proof. In systems of structural scope, this is not
363: possible, and we must instead restrict our to inference in specific
364: logical fragments, as described for the intuitionistic case in,
365: e.g., \cite{mnps:uniform,harland:jlc93,harland:iccl00}.%
366: %
367: \footnote{
368: A further case of structural control of inference that has
369: attracted particular interest is linear logic, where linear
370: disjunction must be understood to specify synchronization between
371: concurrent processes rather than proof by case analysis; see, e.g.,
372: \cite{andreoli:focusing,hodas/miller:lolli,pym/harland:jlc94,miller:tcs96,kobayashi:tcs99}.
373: The investigation of fragments of linear logic remains essential,
374: as linear logic has no analogue of an explicitly-scoped proof
375: system, and so---unlike intuitionistic logic and modal logic---must
376: be understood as a refinement of classical logic rather than an
377: extension to it \cite{girard:lu}.
378: }
379:
380: By contrast, systems of explicit scope can be lifted by a
381: suitable analogue to the Herbrand-Skolem-G\"odel theorem for
382: classical logic so that \emph{any} pair of unrelated inferences can
383: be interchanged
384: \cite{kleene:permute,wallen:nonclassical,lincoln/shankar:search,permute-paper}.
385: Thus, unlike systems of structural scope, systems of explicit scope
386: permit \emph{general} goal-directed reasoning. If we adopt
387: Miller's characterization of uniform proof for sequent calculi with
388: multiple conclusions \cite{dale:forum,miller:tcs96}, then any modal
389: theorem has a uniform proof in a lifted, explicitly-scoped
390: inference system. Put another way, explicitly-scoped inference
391: assimilates modal proof to classical proof, and we know that
392: uniformity is not really a restriction on classical proof
393: \cite{harland:cl97,nadathur:uniform/classical}. This is why my
394: investigation emphasizes questions of information-flow, such as
395: modularity and locality, rather than questions of goal-directed
396: proof \emph{per se}.
397:
398: I will refer to the proof of Figure~\ref{explicit-search-fig}
399: to illustrate some of the properties of information-flow in
400: goal-directed search.
401: %
402: \begin{figure}
403: \small
404: \begin{center}
405: \begin{tabular}{rl}
406: \fbox{3} &
407: \derivii{$(\imp\proveslabel)$}
408: {\derivii{$(\proveslabel\wedge)$}
409: {\underline{B}, \ldots \proves \ldots, \underline{B}}
410: {\underline{D}, \ldots \proves \ldots, \underline{D}}
411: {B, D, \ldots \proves \underline{B \wedge D}}}
412: {\underline{F}, \ldots \proves \ldots, \underline{F}}
413: {B, D, \underline{(B\wedge D) \imp F}, \ldots \proves \ldots,
414: \underline{F}}
415: \\[2em]
416: \fbox{2} &
417: {\derivii{$(\imp\proveslabel)$}
418: {\derivii{$(\vee\proveslabel)$}
419: {\underline{C}, \ldots \proves \ldots, \underline{C}}
420: {\fbox{3}}
421: {B, \underline{C\vee D}, (B\wedge D) \imp F, \ldots
422: \proves \ldots, \underline{C}, F}}
423: {\underline{F}, \ldots \proves \ldots, \underline{F}}
424: {B, C\vee D, \underline{C \imp F}, (B\wedge D) \imp F \proves
425: \ldots, \underline{F}}}
426: \\[2em]
427: \fbox{1} &
428: \derivii{$(\imp\proveslabel)$}
429: {\derivii{$(\vee\proveslabel)$}
430: {\underline{A}, \ldots \proves \underline{A}, F}
431: {\fbox{2}}
432: {\underline{A \vee B}, C\vee D, C \imp F, (B\wedge D) \imp F \proves \underline{A}, F}}
433: {\underline{F}, \ldots \proves \underline{F}}
434: {A \vee B, C\vee D, \underline{A \imp F}, C \imp F, (B\wedge D)
435: \imp F \proves \underline{F}}
436: \end{tabular}
437: \end{center}
438: \caption{A goal-directed proof in which multiple cases are
439: considered. Each case is displayed in a separate block.}
440: \label{explicit-search-fig}
441: \end{figure}
442: %
443: The proof establishes the conclusion
444: \[
445: F
446: \]
447: from assumptions
448: \[
449: A \vee B, C \vee D, A \imp F, C \imp F, (B \wedge D) \imp F
450: \]
451:
452: First we must get clear on the reasoning
453: Figure~\ref{explicit-search-fig} represents. The assumptions in
454: this proof again specify two ambiguities, $A\vee B$ and $C\vee D$.
455: In modal terms, these are local ambiguities that introduce local
456: assumptions; but actually, Figure~\ref{explicit-search-fig} uses
457: only classical connectives, and this classical reasoning suffices
458: for my discussion here. In Figure~\ref{explicit-search-fig}, the
459: two ambiguities interact to require inference for three separate
460: cases: one case where $A$ is true, one case where $C$ is true, and
461: a final case where $B$ and $D$ are true together. (These cases are
462: laid out separately in Figure~\ref{explicit-search-fig}.) In
463: goal-directed inference, we discover these cases by backward
464: chaining from the main goal $F$ through a series of implications:
465: $A \imp F$, $C \imp F$, and $(B \wedge D) \imp F$.
466:
467: Now we can describe the structure of the proof of
468: Figure~\ref{explicit-search-fig} more precisely. The inference is
469: segmented out into three chunks, one for each case. The chunks are
470: indexed to indicate how they should be assembled into a single
471: proof-tree; the chunk indexed \fbox{3} should appear as a subtree
472: where the index \fbox{3} is used in chunk \fbox{2}, and that chunk
473: should in turn appear as a subtree where the index \fbox{2} is used
474: in chunk \fbox{1}. We could imagine writing out that tree in
475: full---on an ample blackboard! However, the chunks are actually
476: natural units of the proof of Figure~\ref{explicit-search-fig};
477: they are what Loveland calls \emph{blocks}
478: \cite{loveland:nhp,nadathur/loveland:disj}. In general, a
479: \emph{block} of a derivation is a maximal tree of contiguous
480: inferences in which the right subtree of any $(\vee\proveslabel)$
481: inference in the block is omitted. (Check this in
482: Figure~\ref{explicit-search-fig}.) Each block presents reasoning
483: that describes a single case from the specification.
484:
485: Within blocks, we can trace the progress of goal-directed
486: reasoning, as follows. At each step, our attention is directed to
487: a distinguished goal formula---the current goal---and at most one
488: distinguished program formula---the selected statement. For
489: illustration, these distinguished formulas are underlined in each
490: sequent in Figure~\ref{explicit-search-fig}. Logical operations
491: apply only to distinguished formulas; we first decompose the goal
492: down to atomic formulas, then select a program formula and reason
493: from it to establish the current goal.
494:
495: There are two things to notice about this derivation. First,
496: we use a \emph{restart} discipline when handling disjunctive case
497: analysis across blocks \cite{loveland:nhp,nadathur/loveland:disj}.
498: In each new block, the current goal is reset to the original goal
499: $F$ to restart proof search. It is easy to see that it does not
500: suffice, in general, to keep the current goal across blocks; in
501: Figure~\ref{explicit-search-fig}, for example, keeping the current
502: goal would mean continuing to try to prove $A$ after we turn from
503: the case of $A$ to the case of $B$. The more general restart rule
504: is however complete; in fact, the restart rule is a powerful way to
505: extend a goal-directed proof system to logics where a single proof
506: must sometimes analyze the same goal formula in qualitatively
507: different ways
508: \cite{gabbay/reyle:n-prolog,gabbay:n-prolog,gabbay:htcs92}.
509:
510: Second, note when and how newly-assumed disjuncts are used in
511: new blocks. For example, $B$ is assumed in block \fbox{2} but it
512: is not used until block \fbox{3}. By contrast, $D$ is assumed in
513: block \fbox{3} and used immediately there. Following
514: \cite{loveland:nhp}, I will refer to any use of a disjunctive
515: premise in the first block of case analysis where it is assumed as
516: a \emph{cancellation}; I will also say that the inference that
517: introduces the disjunct, and the new block it creates, are
518: \emph{canceled}. The proof of Figure~\ref{explicit-search-fig}
519: cannot be recast in terms of canceled inferences using the sequent
520: rules of Figure~\ref{explicit-scope-fig}. Whichever case of $A\vee
521: B$ or $C\vee D$ is treated first cannot be canceled; the second
522: disjunct of the one must wait to be used until the second disjunct
523: of the other is introduced. This is a gap between Loveland's
524: original Near-Horn Prolog interpreter \cite{loveland:nhp}, which
525: requires cancellations, and the generalized reformulation in terms
526: of sequent calculi given in
527: \cite{nadathur/loveland:disj,nadathur:uniform/classical} and
528: suggested in Figure~\ref{explicit-search-fig}. Loveland suggests
529: that cancellation is just an optimization, but we shall see that
530: modal logic establishes an important proof-theoretic link between
531: cancellation and modularity.
532:
533: \subsubsection{On modular goal-directed proof search}
534: \label{intro-example-sec}
535:
536: As befits alternative proof methods for the same logic,
537: structurally-scoped systems and explicitly-scoped systems are very
538: close. In fact, in the case of intuitionistic logic, they define
539: not just the same theorems but the same proofs \cite{permute-paper}.
540: This correspondence suggests that we use insights about
541: information-flow in structurally-scoped proofs---including the
542: modularity and locality exhibited by
543: Figure~\ref{structure-module-fig}---to restrict goal-directed
544: proof-search in explicitly-scoped systems.
545:
546: In fact, we know from \cite{permute-paper} that we can
547: sometimes enforce a straightforward requirement of locality in
548: explicitly-scoped inferences, as follows. Assume that we have an
549: explicitly-scoped proof system for a logic with modularity and
550: locality, with an eigenvariable condition on $(\proveslabel\Box)$,
551: and we work in a fragment of logic without negation (this again
552: includes the S4 translation of intuitionistic formulas). Then when
553: we consider a sequent of this form in proof-search:
554: \[
555: \Gamma \proves \Delta
556: \]
557: we apply inferences to a formula $P$ in $\Gamma$ only when $P$
558: is labeled with a prefix of a label of a formula in $\Delta$. That
559: is, we can consider inferences on $P^{\mu} \in \Gamma$ only when
560: there is some $G^{\mu\nu} \in \Delta$. The prefix relationship is
561: required for $P$ to eventually contribute to the proof of any
562: $\Delta$ formula. For example here:
563: \[
564: A, B^{\beta}, C^{\gamma}, D^{\delta} \proves E^{\beta}, F^{\gamma}
565: \]
566: We can consider $A$, $B^{\beta}$ or $C^{\gamma}$, but not
567: $D^{\delta}$.
568:
569: This invariant is weaker than one might want or expect for
570: certain kinds of goal-directed search. Specifically, we have seen
571: that when we use goal-directed search as a model for logic
572: programming, we understand the interpreter to be working on at most
573: one goal and one program statement at a time. In this setting, we
574: would like to require that the program statement must be able to
575: contribute to the current goal. However, we must understand the
576: result of \cite{permute-paper} to require only that the current
577: program statement must contribute to \emph{some} goal, not necessarily
578: the \emph{current} one. In addition, we must take into account
579: other, inactive goals, such as the goals that we may potentially
580: restart later in proof search. In the preceding example, even if
581: $E^{\beta}$ were the current goal, we might have to consider
582: reasoning with $C^{\gamma}$ because of the possibility of a restart
583: with $F^{\gamma}$.
584:
585: For most inferences, we can rule out their contribution to
586: inactive goals, on independent grounds. Most inferences from
587: assumptions in goal-directed proofs must contribute to the current
588: goal or not at all. But there is one difficult case, which happens
589: also the most meaningful one. This is the case of disjunction
590: itself, where only one disjunct contributes to the current goal.
591: The other disjunct may contribute to some other goal; we will set
592: up a new proof problem by assuming this disjunct and making some
593: inactive goal active. Modularity and locality suggest that we
594: should be able now to select a goal that our newly-assumed disjunct
595: could contribute to. In other words, if the new disjunct is
596: $P^{\mu}$ the next goal should take the form $G^{\mu\nu}$ with
597: $\mu$ a prefix of $\mu\nu$. Call this a modular restart. The
598: alternative is that there is no relationship of scope between the
599: new disjunct and the next goal.
600:
601: Modular restarts would be quite powerful. For example, they
602: would allow us to capture the declarative search control
603: illustrated in Figure~\ref{structure-module-fig}. In an
604: explicitly-scoped goal-directed proof corresponding to
605: Figure~\ref{structure-module-fig}, the case analysis for
606: $\Box(A\vee B)$ will look like this:
607: \[
608: \derivi{$\Box\proveslabel$}
609: {\derivii{$\vee\proveslabel$}
610: {\underline{A}^{\alpha}, \ldots \proves \underline{A}^{\alpha}, \ldots}
611: {B^{\alpha}, \ldots \proves A^{\alpha}, \ldots}
612: {\underline{A\vee B}^{\alpha}, \ldots \proves \underline{A}^{\alpha}, \ldots}}
613: {\underline{\Box(A \vee B)}, \ldots \proves \underline{A}^{\alpha}, \ldots}
614: \]
615: With modular restarts, we know we must continue to take
616: $A^{\alpha}$ as the current goal in the right top ($B^{\alpha}$)
617: subproof. In effect, we know to build a short proof in which
618: ambiguities are considered independently. We can cut down the
619: space for proof search accordingly---for example, there will be no
620: question of introducing the other ambiguity from $\Box(C\vee D)$ in
621: the new modular block. On the other hand, without modular
622: restarts, we are free to reconsider the initial goal $(\Box A)
623: \wedge (\Box C)$ at this stage; in subsequent search we will
624: reconsider both $\Box(A \vee B)$ and $\Box(C \vee D)$. Thus, even
625: though the logic guarantees that ambiguities do not interact in a
626: proof, we still wind up considering interacting ambiguities in
627: proof search.
628:
629: The main result of this paper is to provide an
630: explicitly-scoped goal-directed proof system in which modular
631: restarts are complete. The proof system has modular restarts
632: because, in the new proof system, any proof can be presented in
633: such a way that all disjunctions are canceled. Each new disjunct
634: $P^{\mu}$ therefore contributes to the proof of the restart goal in
635: the current block, and so we know to choose a restart goal
636: $G^{\mu\nu}$ that the new disjunct could contribute to.
637:
638: It turns out that modular restarts are not automatic; you need
639: to design the policy for disjunctive inference to respect it.
640: Figure~\ref{explicit-search-fig} already makes the problem clear.
641: How can we enforce cancellations here? The sequent rules seem not
642: to allow it. The new idea is simple actually---to allow a new
643: inference figure for disjunction that considers disjuncts out of
644: their textual order:
645: \[
646: \derivii{$\vee\proveslabel*$}
647: {\Gamma, D^{\mu} \proves \Delta}
648: {\Gamma, C^{\mu} \proves \Delta}
649: {\Gamma, C\vee D^{\mu} \proves \Delta}
650: \]
651: This is the direct analogue of the Near-Horn Prolog inference
652: scheme, which can proceed by matching any of the heads of a
653: disjunctive clause at any time \cite{loveland:nhp}. The new
654: sequent rule will allow us to reanalyze the constitution of higher
655: blocks so that, wherever we use the new disjunct in the original
656: proof, we can always reanalyze it as part of the current block.
657: Figure~\ref{explicit-modular-fig} demonstrates this reanalysis for
658: Figure~\ref{explicit-search-fig}.
659: %
660: \begin{figure}
661: \small
662: \begin{center}
663: \begin{tabular}{rl}
664: \fbox{$2'$} &
665: {\derivii{$(\imp\proveslabel)$}
666: {\underline{C}, \ldots \proves \ldots, \underline{C}}
667: {\underline{F}, \ldots \proves \ldots, \underline{F}}
668: {B, C, \underline{C \imp F}, \ldots \proves
669: \ldots, \underline{F}}}
670: \\[2em]
671: \fbox{$3'$} &
672: \derivii{$(\imp\proveslabel)$}
673: {\derivii{$(\proveslabel\wedge)$}
674: {\underline{B}, \ldots \proves \ldots, \underline{B}}
675: {\derivii{$(\vee\proveslabel*)$}
676: {\underline{D}, \ldots \proves \ldots,
677: \underline{D}}
678: {\fbox{$2'$}}
679: {B, \underline{C\vee D}, C\imp F, \ldots \proves \ldots, \underline{D}}}
680: {B, C\vee D, C \imp F, \ldots \proves \underline{B \wedge D}}}
681: {\underline{F}, \ldots \proves \ldots, \underline{F}}
682: {B, C\vee D, C\imp F, \underline{(B\wedge D) \imp F}, \ldots \proves \ldots,
683: \underline{F}}
684: \\[2em]
685: \fbox{1} &
686: \derivii{$(\imp\proveslabel)$}
687: {\derivii{$(\vee\proveslabel)$}
688: {\underline{A}, \ldots \proves \underline{A}, F}
689: {\fbox{$3'$}}
690: {\underline{A \vee B}, C\vee D, C \imp F, (B\wedge D) \imp F \proves \underline{A}, F}}
691: {\underline{F}, \ldots \proves \underline{F}}
692: {A \vee B, C\vee D, \underline{A \imp F}, C \imp F, (B\wedge D)
693: \imp F \proves \underline{F}}
694: \end{tabular}
695: \end{center}
696: \caption{A reanalysis of the proof of Figure~\ref{explicit-search-fig}
697: to enforce cancellations. We rewrite block \fbox{$3'$}, in which
698: $B$ is canceled, to use the new disjunctive inference figure; block
699: \fbox{$3'$} thus becomes the second block after \fbox{1}. At the
700: same time, we introduce a simplified block \fbox{$2'$} which uses
701: the assumption $C$, without disjunction at all.}
702: \label{explicit-modular-fig}
703: \end{figure}
704: %
705: In fact, demonstrating the generality of such reanalysis will
706: prove to be quite involved. Explicitly-scoped inferences with an
707: eigenvariable condition give blocks in modal proofs an inherently
708: hierarchical structure, because of the different modal scopes that
709: are introduced and the local assumptions that are made. Loveland's
710: construction for cancellations, by contrast, assumes that the
711: structure of blocks is flat. Instead, we must use the natural
712: tools of the sequent calculus to develop suitable constructions for
713: reanalyzed inferences.
714:
715: \subsection{The results and their context}
716: \label{tech-overview-subsec}
717:
718: The problem sketched in Section~\ref{problem-subsec} is a pure
719: problem of modal proof. Accordingly, all the proof systems I
720: consider will describe sound and complete inference under the usual
721: Kripke semantics for modal logic \cite{kripke:modal,fitting:proof}.
722: I will not consider interactions of disjunction with
723: negation-by-failure and other operational features of of logic
724: programming proof-search systems. For such issues in disjunctive
725: logic programming, see for example
726: \cite{lobo/minker/raj:disjunction}. Nor will I attempt to describe
727: a minimal model or fixed-point construction in which exactly the
728: consequences of a modal program hold, as in
729: \cite{orgun/wadge:jlp92}.
730:
731: Moreover, my interest is in specific fragments of specific
732: modal logics in particular. \emph{Modularity} and \emph{locality}
733: allow consideration of the logics T, K and K4 in addition to S4,
734: but are not compatible with such logics as S5, temporal logics with
735: symmetric past and future operators \cite{gabbay:87}, the logic of
736: context of \cite{mccarthy/buvac:context} or the modal logic of
737: named addresses of \cite{kobayashi:tcs99}. For example, in S5, if
738: $\Box A$ is true at any world, then $\Box A$ is true at all worlds;
739: thus the logic prohibits making such an assumption locally. To see
740: the problem, observe, for example, that $\Box(\Box A \imp B) \vee
741: \Box A$ is a theorem of S5. Modal proofs in such cases require
742: global restarts \cite{gabbay/olivetti:sl98}. \emph{Locality}
743: further rules out logical fragments with possibility or negation.
744: Such fragments can be used to pose goals about that access
745: otherwise local assumptions, as in the theorem $\Box(A \imp B) \vee
746: \Diamond A$ of all normal modal logics. (Goal-directed proof of
747: this theorem also involves a global restart.) Moreover, such
748: fragments make it more difficult to enforce modularity as well,
749: since they do not permit an eigenvariable condition at
750: $(\proveslabel\Box)$ inferences in goal-directed proofs. My
751: investigation therefore sticks closely to the treatments of logical
752: modularity and locality originally explored in
753: \cite{dale:modules,giordano/martelli:structuring}. Indeed, I
754: continue to restrict implications and universal quantifiers in
755: goals to strict statements of the form $\Box(P\imp G)$ and $\Box
756: \forall x G$.
757:
758: The basic strategy that I adopt is to start with a relatively
759: straightforward proof system, and gradually to narrow the
760: formulation of its inference rules---preserving soundness and
761: completeness with respect to the underlying semantics---until we
762: have a proof system, SCLP, with the desired characteristics, namely
763: goal-directed search and modular restarts. I have been
764: particularly influenced by Lincoln and Shankar's presentation of
765: proof-theoretic results in terms of simple transformations among
766: successive proof systems \cite{lincoln/shankar:search}; and by
767: Andreoli's construction of focusing sequent calculi that embody the
768: discipline of goal-directed proof directly in the form of inference
769: figures \cite{andreoli:focusing}.
770:
771: However, the correct design of the final proof system requires
772: a variety of proof-theoretic ideas about logic programming to be
773: extended, strengthened, and combined with proof-theoretic results
774: about modal logic in a novel way. To describe logic programming,
775: we start with the idea of uniform proof search described in
776: \cite{mnps:uniform} and extended to multiple-conclusion calculi in
777: \cite{dale:forum}. To derive a uniform proof system in the
778: presence of indefinite information in assumptions, however, we can
779: no longer use the familiar quantifier rules used in previous logic
780: programming research, which simply introduce fresh parameters; we
781: must apply a generalization of Herbrand's Theorem
782: \cite{lincoln/shankar:search} and work with quantifier rules that
783: introduce structured terms. The calculus of Herbrand terms, SCL,
784: lifts the explicitly-scoped proof systems considered in
785: Section~\ref{explicit-subsubsec} and
786: \cite{fitting:proof,wallen:nonclassical}. The key property of SCL
787: is that inferences can be freely interchanged. This allows
788: arbitrary proofs to be transformed easily into uniform proofs.
789:
790: The \emph{modular} behavior of this uniform system depends on
791: the further proof-theoretic analyses of path-based sequent calculi
792: adapted, in part, from \cite{permute-paper}. These analyses
793: establish that path representations enforce modularity and locality
794: in the uses of formulas in proofs, even with otherwise classical
795: reasoning. Hence, although path-based calculi obscure the natural
796: modularity of modal inference, they do not eliminate it. I finish
797: with a streamlined uniform proof system that takes advantage of
798: these results; as a consequence, proof search in this calculus can
799: dynamically exploit the local use of modular assumptions.
800:
801: The justification of this new proof system makes much of a
802: strategy originally due to \cite{kleene:permute}, in which the
803: inferences in a proof are reordered so as to satisfy a global
804: invariant. The strategy achieves termination despite generous
805: copying and deepening of inferences by a judicious choice of
806: transformations within a double induction. In our cases, these
807: transformations are guided by the constraints of uniform proof, and
808: by the cancellations of disjunctive assumptions that we know we
809: must maintain in proofs, to achieve modularity. This provides an
810: analogue of Loveland's transformations on restart proofs
811: \cite{loveland:nhp} in the sequent calculus setting.
812:
813: Of course, modal logic is not just a modular logic. Modal
814: logic provides a general, declarative formalism for specifying
815: change over time, the knowledge of agents, and other
816: special-purpose
817: domains~\cite{prior:tense,hintikka:scope,schild:terminology}.
818: Goal-directed systems for modal proof are often motivated by such
819: specifications
820: \cite{cerro:molog,debart:modal/lp,baldoni/giordano/martelli:modal,bgm:framework}.
821: In generalizing goal-directed modal proof to indefinite
822: specifications, SCLP can play an important role in applying modal
823: formalisms to planning, information-gathering and communication
824: \cite{aaai98,jlac00}. Even when content, not modularity, is
825: primary, the modular treatment of disjunction limits the size of
826: proofs and the kinds of interactions that must be considered in
827: proof search. Such constraints are crucial to the use of logical
828: techniques in applications that require automatic assessment of
829: incomplete information, such as planning and natural language
830: generation. The interest of these more general applications helps
831: explain why I pursue this investigation in the full first-order
832: language.
833:
834: \subsection{Outline}
835: \label{outline-subsec}
836:
837: The structure of the rest of this paper is as follows. I
838: begin by presenting first-order multi-modal logic in
839: Section~\ref{logic-sec}. I consider syntax
840: (Section~\ref{syntax-subsec}), semantics
841: (Section~\ref{semantics-subsec}), and finally proof
842: (Section~\ref{proof-subsec}); I describe the explicitly-scoped
843: Herbrand proof system for modal logic that is my starting point.
844: Section~\ref{uniform-proof-subsec} shows that this calculus offers
845: a suitable framework for goal-directed proof because uniform proof
846: search in this calculus is complete.
847:
848: Section~\ref{module-sec} describes and justifies a modular
849: goal-directed proof system, as advertised in
850: Section~\ref{problem-subsec}. I introduce the calculus itself in
851: Section~\ref{final-subsec}, along with key definitions and
852: examples. Then in
853: Sections~\ref{segment-subsec}--\ref{modularity-subsec} I outline
854: how this sequent calculus is derived in stages from the calculus of
855: Section~\ref{logic-sec}. Full details are provided in an appendix.
856:
857: Finally, Section~\ref{assessment-sec} offers a broader
858: assessment of these results. I consider some further optimizations
859: that the new sequent calculus invites in
860: Section~\ref{implementation-subsec}, and briefly conclude in
861: Section~\ref{use-subsec} with some applications of
862: first-order multi-modal inference that the new sequent calculus
863: suggests.
864:
865: \section{First-order multi-modal deduction}
866: \label{logic-sec}
867:
868: I begin by supporting the informal presentation of first-order
869: multi-modal logic from Section~\ref{intro-sec} more explicitly. I
870: will adopt a number of techniques that are individually quite
871: familiar. I allow an arbitrary number of modal operators and a
872: flexible regime for relating different modal operators to one
873: another, following many applied investigations
874: \cite{debart:modal/lp,baldoni/giordano/martelli:modal,bgm:framework,baldoni/giordano/martelli:ld98}.
875: I use prefix terms for worlds and sequent calculus inference,
876: following the comprehensive treatment of the first-order modal
877: logic using prefix terms and analytic tableaux (or, seen
878: upside-down, in the cut-free sequent calculus) of
879: \cite{fitting/mendelsohn}. I factor out reasoning about
880: accessibility into side conditions on inference rules, similar to
881: the proof-theoretic view of \cite{basin/matthews/vigano:jlli98}, in
882: which reasoning about accessibility and boolean reasoning are
883: clearly distinguished. And I use Herbrand terms to reason
884: correctly about parameterized instances of formulas, avoiding the
885: usual eigenvariable condition on quantifier (and modal) rules, as
886: in \cite{lincoln/shankar:search}.
887:
888: Though the techniques are routine, the combination is still
889: somewhat unusual. Research in modal logic---whether the
890: investigation is more mathematical
891: \cite{gore:diss,massacci:1step,massacci:tableau,gore:tableau} or
892: primarily concerns algorithms for proof search
893: \cite{otten/kreitz,beckert/gore:97,schmidt:uni}---is dominated by
894: the study of the propositional logic of a single modal operator (or
895: accessibility relation). Moreover, researchers who have
896: investigated modal logic in a first-order setting have tended to
897: jump directly into a discussion of particular theorem-proving
898: strategies, particularly resolution
899: \cite{jackson:ijcai,wallen:nonclassical,catach:tableau,frisch/scherl:constraint,auffray:equations,nonnengart:ijcai,ohlbach:multimodal}.
900:
901: \subsection{Syntax}
902: \label{syntax-subsec}
903:
904: Our language depends on a \emph{signature} including a
905: suitable set of atomic constants $C$ (and suitable predicate
906: symbols and modalities). We then consider program statements of
907: the syntactic category $D(C)$ and goals of the category $G(C)$
908: defined recursively as in \sref{dialup.syntax}; we refer to the
909: union of these two languages as $L(C)$. \sref{dialup.syntax} makes
910: explicit the conditions observed in
911: Section~\ref{tech-overview-subsec}; there is no possibility or
912: negation, and universal and hypothetical goals must be modal.
913: %
914: \sentence{dialup.syntax}{
915: $\begin{array}[t]{l@{\;::=\;}l}
916: G & A \; | \; \op{m}G \; | \; G \wedge G \; | \; G \vee G \; |
917: \; \op{m}(\forall x G) \; | \; \exists x G \; | \;
918: \op{m}(D\imp G) \\
919: D & A \; | \; \op{m}D \; | \; D \wedge D \; | \; D \vee D
920: \; | \; \forall x D \; | \; \exists x D \; | \; G \imp
921: D
922: \end{array}$
923: }
924: %
925: In \sref{dialup.syntax}, $A$ schematizes an atomic formula;
926: atomic formulas take the form $p_i(a_1,\ldots,a_k)$ where $p_i$ is
927: a predicate symbol of arity $k$ and each $a_i$ is either a variable
928: or an atomic constant in the set $C$. We assume some initial
929: non-empty set of constants $CONST$. But it will be convenient to
930: consider languages in which a countably infinite number of
931: \emph{parameters} are included in the language to supplement the
932: symbols in CONST.
933:
934: In \sref{dialup.syntax}, \op{m} schematizes a modal operator
935: of necessity; intuitively, such modal operators allow a
936: specification to manipulate constrained sources of information.
937: That is, a program statement $\op{m}D$ explicitly indicates that
938: $D$ holds in the constrained source of information associated with
939: the operator $\op{m}$. Conversely, a goal $\op{m}G$ can be
940: satisfied only when $G$ is established by using information
941: from the constrained source associated with $\op{m}$.
942:
943: We will work in a multi-modal logic, in which any finite
944: number $m$ of distinct necessity operators or \emph{modalities} may
945: be admitted. (Necessity operators will also be written as $\Box$
946: or $\Box_i$.) In addition to ordinary program statements, a
947: specification may contain any of the following axiom schemes
948: describing the modalities to be used in program statements and
949: goals:
950: %
951: \sentence{dialup.axioms}{
952: $\begin{array}[t]{ll}
953: \Box_i p \imp p \;\; &
954: \mbox{\emph{veridicality}} \; \verax \\
955: \Box_i p \imp \Box_i \Box_i p \;\; &
956: \mbox{\emph{positive introspection}} \; \piax \\
957: \Box_i p \imp \Box_j p \;\; &
958: \mbox{\emph{inclusion}} \; \incax \\
959: \end{array}$
960: }
961: %
962: These axioms describe the nature of the information that an
963: operator provides, and spell out relationships among the different
964: sources of information in a specification. \verax\ is needed for
965: information that correctly reflects the world; \piax, for
966: information that provides a complete picture of how things might
967: be; and \incax, for a source of information, \m j, that elaborates
968: on information from another source, \m i. Because we use this
969: explicit axiomatization, we can take the names of the modal
970: operators as arbitrary.
971:
972: We appeal to the usual notions of \emph{free} and \emph{bound}
973: occurrences of variables in formulas; we likewise invoke the
974: \emph{depth} of a formula---the largest number of nested logical
975: connectives in it.
976:
977: \subsection{Semantics}
978: \label{semantics-subsec}
979:
980: As is standard, we describe the models for the modal language
981: in two steps. The first step is to set up \emph{frames} that
982: describe the structure of any model; a full model can then be
983: obtained by combining a frame with a way of assigning
984: interpretations to formulas in a frame.
985:
986: \begin{definition}[Frame]
987: \label{frame-def}
988: A \emph{frame} consists of a tuple $\langle \worlds, \access,
989: \domain\rangle$ where: \worlds\ is a non-empty set of
990: \emph{possible worlds}; $\access$ names a family of $m$ binary
991: \emph{accessibility} relations on \worlds, a relation $\access_i$
992: for each modality $i$; and \domain\ is a \emph{domain function}
993: mapping members of \worlds\ to non-empty sets.
994: \end{definition}
995:
996: Within the frame ${\cal F}$, the function \domain\ induces a
997: set $\domain({\cal F})$, called the \emph{domain of the frame}, as
998: $\cup \{ \domain(w) \; | \; w \in \worlds \}$. In order to
999: simplify the treatment of constant symbols, it is also convenient
1000: to define a set of objects that all the domains of the different
1001: possible worlds have in common, the \emph{common domain of the
1002: frame} ${\cal F}$: $\cdomain({\cal F}) = \cap \{ \domain(w) \; | \;
1003: w \in \worlds \}$. We effectively insist that $\cdomain({\cal F})$
1004: be non-empty as well, since CONST is non-empty and each symbol in
1005: CONST must be interpreted by an element of $\cdomain({\cal F})$.
1006:
1007: The intermediate level of frames is useful in characterizing
1008: the meanings of modal operators and modal quantification. In
1009: particular, simply by putting constraints on $\access_i$ or on
1010: \domain\ at the level of frames, we can obtain representative
1011: classes of models in which certain general patterns of inference
1012: are validated. The constraints we will avail ourselves of are
1013: introduced in Definition~\ref{r-prop-def}.
1014:
1015: \begin{definition}
1016: \label{r-prop-def}
1017: Let $\langle \worlds, \access, \domain\rangle$ be a
1018: \emph{frame}. We say the frame is:
1019: %
1020: \begin{itemize}
1021: \item
1022: \emph{reflexive} at $i$ if $w \access_i w'$ for every $w \in
1023: \worlds$;
1024: \item
1025: \emph{transitive} at $i$ if, for any $w,w'' \in \worlds$, $w
1026: \access_i w''$ whenever there is a $w' \in \worlds$ such that $w
1027: \access_i w'$ and $w' \access_i w''$;
1028: \item
1029: \emph{narrowing} from $i$ to $j$ if $w \access_j w'$ implies
1030: $w \access_i w'$ for all $w, w' \in \worlds$;
1031: \item
1032: \emph{increasing domain} if for all $w, w' \in \worlds$,
1033: $\domain(w) \subseteq \domain(w')$ whenever there is some
1034: accessibility relationship $w \access_i w'$.
1035: \end{itemize}
1036: \end{definition}
1037:
1038: Our scheme for using the constraints of
1039: Definition~\ref{r-prop-def} depends on establishing a regime for
1040: the $m$ modalities in the language, describing the inferences that
1041: should relate them. The regime is defined as follows.
1042: %
1043: \begin{definition}[Regime]
1044: A \emph{regime} is a tuple $\langle \types, \inclusions,
1045: \dconstraint\rangle$, where: \types\ is a function mapping each
1046: modality into one of the symbols K, K4, T and S4; $\inclusions$ is
1047: a (strict) partial order on the modalities; and $\dconstraint$ is
1048: the symbol \emph{increasing}.
1049: \end{definition}
1050: %
1051: The reader will recognize the symbols in the image of \types\
1052: as the classic names for modal logics of a single modality. $S4$
1053: is for modalities that are subject to \piax\ and \verax. $T$ is
1054: for modalities that are subject just to \verax. $K4$ is for
1055: modalities that are subject just to \piax. $K$ is modalities
1056: subject to neither axiom. The interactions specified by \incax\
1057: are determined by the partial order on modalities: $j \leq i$ when
1058: $\Box_i p \imp \Box_j p$. This meaning for these symbols can be
1059: enforced by considering only frames that \emph{respect} the given
1060: \emph{regime}.
1061: %
1062: \begin{definition}[Respect]
1063: Let ${\cal F} = \langle\worlds, \access, \domain\rangle$ be a
1064: frame, and let ${\cal S} = \langle \types, \inclusions,
1065: \dconstraint\rangle$ be a regime. We say ${\cal F}$
1066: \emph{respects} ${\cal S}$ whenever the following conditions are
1067: met for all modalities $i$ and $j$:
1068: \begin{itemize}
1069: \item
1070: If $\types(i)$ is T or S4 then $\access_i$ is
1071: reflexive.
1072: \item
1073: If $\types(i)$ is K4 or S4 then
1074: $\access_i$ is transitive.
1075: \item
1076: If $j \leq i$ according to \inclusions\ then ${\cal F}$ is
1077: narrowing from $i$ to $j$.
1078: \item
1079: If \dconstraint\ is \emph{increasing}, then ${\cal
1080: F}$ is increasing domain.
1081: \end{itemize}
1082: \end{definition}
1083:
1084: From now on, we assume that some regime ${\cal S} =
1085: \langle\types, \inclusions,\dconstraint\rangle$ is fixed, and
1086: restrict our attention to frames that respect ${\cal S}$.
1087: Informally, now, a model consists of a frame together with an
1088: interpretation.
1089: %
1090: \begin{definition}[Interpretation]
1091: \valuation\ is an \emph{interpretation} in a frame $\langle
1092: \worlds, \access, \domain \rangle$ if \valuation\ satisfies these
1093: two conditions:
1094: %
1095: \begin{enumerate}
1096: \item
1097: \valuation\ assigns to each $n$-place relation symbol $p_i$ and
1098: each possible world $w \in \worlds$ some $n$-ary relation on the
1099: domain of the frame $\domain({\cal F})$.
1100: \item
1101: \valuation\ assigns to each constant symbol $c$ some element
1102: of the common domain of the frame $\cdomain({\cal F})$.
1103: \end{enumerate}
1104: \end{definition}
1105: %
1106: Thus we can define a \emph{model} over ${\cal S}$ thus:
1107:
1108: \begin{definition}[Model]
1109: A first-order $k$-\emph{modal model} over a regime ${\cal S}$
1110: is a tuple $\langle \worlds, \access, \domain, \valuation \rangle$
1111: where $\langle\worlds,\access, \domain \rangle$ is a frame that
1112: respects ${\cal S}$ and $\valuation$ is an interpretation in
1113: $\langle\worlds,\access,\domain\rangle$.
1114: \end{definition}
1115:
1116: To define truth in a model, we need the usual notion of
1117: assignments and variants:
1118: %
1119: \begin{definition}[Assignment]
1120: Let ${\cal M} = \langle\worlds, \access, \domain,
1121: \valuation\rangle$ be a model (that respects the regime ${\cal
1122: S}$). An \emph{assignment} in ${\cal M}$ is a mapping $g$ that
1123: assigns to each variable $x$ some member $g(x)$ of the domain of
1124: the frame of the model ${\cal
1125: D}(\langle\worlds,\access,\domain\rangle)$.
1126: \end{definition}
1127: %
1128: In proofs, we interpret formulas not just in the ordinary
1129: language $L(C)$ with a given set of modalities, relations,
1130: constants and variables, but in an expanded language \mbox{$L(C\cup
1131: P)$} which also includes a set $P$ of first-order
1132: \emph{parameters}; we will want to use the same models for this
1133: interpretation. Over $L(C\cup P)$, we suppose that an assignment
1134: in ${\cal M}$ also assigns some member $g(p)$ of the domain of the
1135: frame of ${\cal M}$ to each parameter $p$ in $P$.
1136: %
1137: \begin{definition}[Variants]
1138: Let $g$ and $g'$ be two assignments in a model ${\cal M} =
1139: \langle\worlds,\access,\domain,\valuation\rangle$; $g'$ is an
1140: \emph{$x$-variant of $g$ at a world $w\in\worlds$} if $g$ and $g'$
1141: agree on all variables except possibly for $x$ and $g'(x) \in
1142: \domain(w)$.
1143: \end{definition}
1144:
1145: \begin{definition}[Truth in a model]
1146: Let ${\cal M} =
1147: \langle\worlds,\access,\domain,\valuation\rangle$ be a model. Then
1148: the formula $A$ is \emph{true at world $w$ of model ${\cal M}$ on
1149: assignment $g$}---written ${\cal M}, w \forces_g A$---just in case
1150: the clause below selected by syntactic structure of $A$ is
1151: satisfied:
1152: %
1153: \begin{itemize}
1154: \item
1155: $A$ is $p_i(t_1,\ldots,t_n)$: Then ${\cal M}, w \forces_g A$
1156: just in case $\langle e_1,\ldots e_n \rangle \in
1157: \valuation(p_i,w)$, where for each $t_i$, $e_i$ is
1158: $\valuation(t_i)$ if $t_i$ is a constant and $g(t_i)$ otherwise.
1159: \item
1160: $A$ is $B_1 \wedge B_2$: Then ${\cal M}, w \forces_g A$ just
1161: in case both ${\cal M}, w \forces_g B_1$ and ${\cal M}, w \forces_g
1162: B_2$.
1163: \item
1164: $A$ is $B_1 \vee B_2$: Then ${\cal M}, w \forces_g A$ just in
1165: case either ${\cal M}, w \forces_g B_1$ or ${\cal M}, w \forces_g
1166: B_1$.
1167: \item
1168: $A$ is $\Box_i B$: Then ${\cal M}, w \forces_g A$ just in case
1169: for every $w' \in \worlds$, if $w \access_i w'$ then ${\cal M}, w'
1170: \forces_g B$.
1171: \item
1172: $A$ is $\forall x B$: Then ${\cal M}, w \forces_g A$ just in
1173: case for every $x$-variant $g'$ of $g$ at $w$, ${\cal M}, w
1174: \forces_{g'} B$.
1175: \item
1176: $A$ is $\exists x B$: Then ${\cal M}, w \forces_g A$ just in
1177: case there is some $x$-variant $g'$ of $g$ at $w$ with ${\cal
1178: M}, w \forces_{g'} B$.
1179: \end{itemize}
1180: \end{definition}
1181:
1182: By a \emph{sentence} we mean a formula of $L($CONST$)$ in
1183: which no variables occur free. For any sentence $A$, model ${\cal
1184: M}$ and world $w$ of ${\cal M}$, a simple induction on depth
1185: guarantees that ${\cal M}, w \forces_g A$ for some assignment $g$
1186: in ${\cal M}$ exactly when ${\cal M}, w \forces_g A$ for all
1187: assignments $g$ in ${\cal M}$. In this case, we can write simply
1188: ${\cal M}, w \forces A$ and say that $A$ is \emph{true in ${\cal
1189: M}$ at $w$}.
1190:
1191: \begin{definition}[Valid] \label{valid-def}
1192: Let $A$ be a sentence and ${\cal M} = \langle \worlds,
1193: \access, \domain, \valuation \rangle$ be a model. $A$ is
1194: \emph{valid in ${\cal M}$} if for every world $w \in \worlds$,
1195: ${\cal M}, w \forces A$. $A$ is \emph{valid} (on the regime
1196: $\langle\types, \inclusions,\dconstraint\rangle$) if $A$ is valid
1197: in any model ${\cal M}$ that respects the regime.
1198: \end{definition}
1199:
1200: \subsection{Proof theory}
1201: \label{proof-subsec}
1202:
1203: We now present our basic deductive system---a cut-free
1204: path-based sequent calculus for multi-modal deduction which uses
1205: Herbrand terms to reason correctly about parameterized instances of
1206: formulas. Since this calculus represents our basic \emph{lifted
1207: sequent calculus} for modal logic, we refer to it as SCL here. Our
1208: starting point is Theorem~\ref{sem-thrm} that SCL provides a sound
1209: and complete characterization of valid formulas.
1210:
1211: SCL has the advantage that inferences can be freely
1212: interchanged, allowing arbitrary proofs to be transformed easily
1213: into goal-directed proofs; we show in Theorem~\ref{eager-thrm},
1214: presented in Section~\ref{uniform-proof-subsec}, how to obtain
1215: goal-directed proofs in this calculus. The very same flexibility
1216: of inference, however, means that this calculus neither respects
1217: nor represents the potential of modal inference to give proofs an
1218: explicitly modular structure.
1219:
1220: The basic constituent in SCL is a \emph{tracked, prefixed
1221: formula}. The formulas extend the basic languages $D(C)$ and
1222: $G(C)$ of definitions and goals defined in \sref{dialup.syntax} by
1223: allowing additional terms---representing arbitrary witnesses of
1224: first order quantifiers, and arbitrary transitions of modal
1225: accessibility among possible worlds---to be introduced into
1226: formulas for the purposes of proof. We begin by assuming two
1227: countable sets of symbols: a set $H$ of \emph{first-order Herbrand
1228: functions} and $\Upsilon$ of \emph{modal Herbrand functions}. We
1229: can now define sets $P_H$ of \emph{first-order Herbrand terms},
1230: $\kappa_{\Upsilon}$ of \emph{modal Herbrand terms}, and
1231: ${\Pi(\kappa_{\Upsilon})}$ of \emph{Herbrand prefixes} by mutual
1232: recursion:
1233: %
1234: \begin{definition}[Herbrand terms and prefixes]
1235: Assume that $t_0$ is a Herbrand prefix and let
1236: $t_1,\ldots,t_n$ be a sequence (possibly empty), where each $t_i$
1237: is either an element of $C$, a first-order Herbrand term, or a
1238: Herbrand prefix. Then if $h$ is a first-order Herbrand function
1239: then $h(t_0,t_1,\ldots,t_n)$ is a \emph{first-order Herbrand term}.
1240: If $\eta$ is a modal Herbrand function then
1241: $\eta(t_0,t_1,\ldots,t_n)$ is a \emph{modal Herbrand term}. A
1242: \emph{Herbrand prefix} is any finite sequence of modal Herbrand
1243: terms.
1244: \end{definition}
1245: %
1246: The rationale behind the use of a Herbrand term $h(X)$ at an
1247: existential inference $R$ goes like this. At existential
1248: inferences, we need to reason about a generic individual. We need
1249: to have a suitable representation for a generic individual for $R$.
1250: Regardless of the order in which inferences are applied in a
1251: sequent deduction, there will be some parameters that must occur in
1252: the sequent where $R$ applies. For example, some parameters must
1253: appear here as a result of the instantiations that must take place
1254: in deriving the formula to which $R$ applies. We must be sure that
1255: the individual we introduce for $R$ is different from all these
1256: parameters. The terms $X$ which are supplied as an argument to the
1257: Herbrand term $h(X)$ identify these parameters indirectly. The
1258: structure $h(X)$ therefore serves as a placeholder for a new
1259: parameter that could be chosen to be different from each of the
1260: terms in $X$. The structure $h(X)$ thus packs all the information
1261: required to allow the inferences in the proof to be reordered and
1262: an appropriate parameter chosen so that the inference at $R$ is
1263: truly generic.
1264:
1265: In modal deduction, of course, we need generic individuals at
1266: modal inferences as well as existential ones. Modal Herbrand
1267: inference therefore requires that we introduce Herbrand terms to
1268: describe transitions among possible worlds and Herbrand prefixes to
1269: name possible worlds, in addition to introducing first-order
1270: Herbrand terms to represent first-order parameters. In this case,
1271: the arguments $X$ to Herbrand terms must mix first-order Herbrand
1272: terms and Herbrand prefixes, since logical formulas can encode
1273: dependencies among first-order and modal parameters.
1274:
1275: A \emph{prefixed formula} is now an expression of the form
1276: $A^{\mu}$ with $A$ a formula and $\mu$ a Herbrand prefix---we use
1277: $D(C\cup P_H)^{\Pi(\kappa_{\Upsilon})}$ and $G(C\cup
1278: P_H)^{\Pi(\kappa_{\Upsilon})}$ to refer to prefixed definitions and
1279: prefixed goals. For Herbrand calculi, formulas must also be
1280: \emph{tracked} to indicate the sequence of instantiations that has
1281: taken place in the derivation of the formula.
1282: %
1283: \begin{definition}[Tracked expressions]
1284: If $E$ denotes the expressions of some class, then the
1285: \emph{tracked expressions} of that class are expressions of the
1286: form $e_I$ where $e$ is an expression of $E$ and $I$ is a
1287: finite sequence (possibly empty) of elements of $C\cup P_H \cup
1288: \Pi(\kappa_{\Upsilon})$.
1289: \end{definition}
1290: %
1291: We say that a tracked expression $e_I$ \emph{tracks} a term
1292: $t$ just in case $t$ occurs as a subterm of some term in $I$.
1293:
1294: In order to reason correctly about multiple modal operators,
1295: we need to keep track of the kinds of accessibility that any modal
1296: transition represents. To endow the system with correct
1297: first-order reasoning on increasing domains, we also need to keep
1298: track of the worlds where first-order terms are introduced. We
1299: use the following notation to record these judgments: $\mu/\nu:i$
1300: indicates that world $\nu$ is accessible from world $\mu$ by
1301: the accessibility relation for modality $i$; and $t:\mu$ indicates
1302: that the entity associated with term $t$ exists at world $\mu$.
1303:
1304: It is convenient to keep track of this information by
1305: anticipating the restricted reasoning required for our fragment
1306: $L(C)$ and exploiting the structure of Herbrand terms, as follows.
1307: It is clear that there are countably many first-order Herbrand
1308: terms, Herbrand prefixes, and formulas in \mbox{$L(C\cup P_H)$}.
1309: We can therefore describe a correspondence as follows. If $A$ is a
1310: formula of the form $\forall x B$ or $\exists x B$ and $u$ is a
1311: natural number, we define a corresponding first-order Herbrand
1312: function $h^u_A$ so that each first-order Herbrand function is
1313: $h_A$ for some $A$ and no first-order Herbrand function is $h^u_A$
1314: and $h^v_B$ for distinct $A$ and $B$ or distinct $u$ and $v$.
1315: Likewise, if $A$ is a formula of the form $\Box_i B$ and $u$ is a
1316: natural number, we define a corresponding modal Herbrand function
1317: $\eta^u_A$ so that each modal Herbrand function is $\eta^u_A$ for
1318: some $A$ and no modal Herbrand function is $\eta^u_A$ and
1319: $\eta^v_B$ for distinct $A$ and $B$ or distinct $u$ and $v$.
1320: (Indexing Herbrand functions by natural numbers means that adapting
1321: a Herbrand proof to respect an eigenvariable condition can be as
1322: simple as reindexing its Herbrand functions.) Now we have:
1323: %
1324: \begin{definition}[Herbrand typings]
1325: A \emph{Herbrand typing for the language} $L(C\cup P_H)$
1326: (under a correspondence as just described) is a set $\Xi$ of
1327: statements, each of which takes one of two forms:
1328: %
1329: \begin{enumerate}
1330: \item
1331: $\mu/\mu \eta:i$ where: $\mu$ is a Herbrand prefix and $\eta$ is a
1332: modal Herbrand term of the form $\eta^u_A(\mu,\ldots)$ and $A$ is
1333: $\Box_i B$.
1334:
1335: \item
1336: $t: \mu$ where $t$ is a first-order Herbrand term of the form
1337: $h(\mu,\ldots)$.
1338: \end{enumerate}
1339: %
1340: A sequence of modal and first-order Herbrand terms $X$
1341: determines a Herbrand typing $\Xi_X$, consisting of the
1342: appropriate $\mu/\mu\eta:i$ for each modal Herbrand term $\eta$
1343: that occurs in $X$ (possibly as a subterm) and the appropriate
1344: $h:\mu$ for each first-order Herbrand term $h$ that occurs in $X$
1345: (possibly as a subterm).
1346: \end{definition}
1347: %
1348: \begin{definition}[Typings] \label{transition-def}
1349: Suppose that $\Xi$ is a Herbrand typing over a language $L(C
1350: \cup P)^{\Pi(\kappa)}$, and that ${\cal S} = \langle \types,
1351: \inclusions, \m{increasing} \rangle$ is a modal regime. We define
1352: the relation that $E$ is a \emph{derived typing} from $\Xi$ with
1353: respect to ${\cal S}$, written ${\cal S}, \Xi \triangleright E$, as
1354: the smallest relation satisfying the following conditions:
1355: %
1356: \begin{itemize}
1357: \item
1358: $(K)$. ${\cal S}, \Xi \triangleright \mu/\nu:i$ if
1359: $\mu/\nu:i \in \Xi$.
1360: \item
1361: $(T)$. ${\cal S}, \Xi \triangleright \mu/\mu:i$ if
1362: $\types(i)$ is T or S4, and $\mu$ occurs in $\Xi$.
1363: \item
1364: $(4)$. ${\cal S}, \Xi \triangleright \mu/\nu:i$ if
1365: $\mu/\mu':i \in \Xi$, ${\cal S}, \Xi \triangleright
1366: \mu'/\nu:i$, and $\types(i)$ is K4 or S4.
1367: \item
1368: $(\m{Inc})$. ${\cal S}, \Xi \triangleright \mu/\nu:i$ if
1369: ${\cal S}, \Xi \triangleright \mu/\nu:j$ and $j \leq i$
1370: according to \inclusions.
1371: \item
1372: $(V)$. ${\cal S}, \Xi \triangleright t:\mu$ if $t:\mu \in
1373: \Xi$.
1374: \item
1375: $(I)$. ${\cal S}, \Xi \triangleright t:\nu$ if ${\cal S},
1376: \Xi \triangleright \mu/\nu:i$ for some $i$ and ${\cal S}, \Xi
1377: \triangleright t:\mu$.
1378: \end{itemize}
1379: \end{definition}
1380: %
1381: Inspection of these rules shows that ${\cal S},\Xi
1382: \triangleright \mu/\nu:i$ only if $\nu$ and $\mu$ occur in $\Xi$.
1383: Moreover, given these rules, an easy induction on the length of typing
1384: derivations gives that ${\cal S},\Xi \triangleright \mu/\nu:i$ only
1385: if $\nu = \mu \nu'$ for some prefix $\nu'$. Thus, suppose that ${\cal
1386: S},\Xi \triangleright \mu/\nu:i$ for some Herbrand typing $\Xi$:
1387: each step in the derivation must concern some prefix of $\nu$ and thus
1388: ${\cal S},\Xi_{\nu} \triangleright \mu/\nu:i$. These invariants permit
1389: some simplifications in reasoning in the fragment $L(C\cup P)$ over more
1390: expressive modal regimes containing other modal operators and other uses
1391: of connectives.
1392:
1393: These definitions allow us to describe the modal Herbrand
1394: sequent calculus precisely. This calculus, SCL, is given in
1395: Definition~\ref{seq-calc-def-1}. Note that for this fragment of
1396: modal logic, it suffices to consider sequents of the form $\Delta
1397: \proves \Gamma$, where $\Delta$ is a multiset of prefixed
1398: definitions (from $D(C\cup P_H)^{\Pi(\kappa_{\Upsilon})}$), and
1399: $\Gamma$ is a multiset of prefixed goals (from $G(C\cup
1400: P_H)^{\Pi(\kappa_{\Upsilon})}$). Note also that ${\cal S},\Xi
1401: \triangleright \mu/\nu:i$ only if $\nu$ is of the form $\mu\nu'$.
1402: %
1403: \begin{definition}[Herbrand sequent calculus] \label{seq-calc-def-1}
1404: For basic first-order multi-modal Herbrand deductions in our
1405: fragment over a regime ${\cal S}$, we will use the sequent rules
1406: defined here, which comprise the system SCL. The rules consist of
1407: an axiom rule and recursive rules---each recursive rule relates a
1408: \emph{base} sequent below to one or more \emph{spur} sequents
1409: above; it applies to the base in virtue of an occurrence of a
1410: distinguished tracked, prefixed formula in the sequent; we refer to
1411: this as the \emph{principal expression} or simply the
1412: \emph{principal} of the inference. Similarly, each of the sequent
1413: rules introduces new expressions onto each spur, which we refer to
1414: as the \emph{side expressions} of the rule. We will also refer to
1415: the two named expression occurrences at axioms as the
1416: \emph{principal expressions} or \emph{principals} of the axiom.
1417: Now we have:
1418: \begin{enumerate}
1419: \item
1420: axiom---$A$ atomic:
1421: \[
1422: {\Delta, A^{\mu}_X \proves \Gamma, A^{\mu}_Y}
1423: \]
1424: \item
1425: conjunctive:
1426: \[
1427: \derivi{$(\wedge\proveslabel)$}
1428: {\Delta, A\wedge B^{\mu}_X,
1429: A^{\mu}_X, B^{\mu}_X \proves \Gamma}
1430: {\Delta, A\wedge B^{\mu}_X \proves \Gamma}
1431: \]
1432: \[
1433: \derivi{$(\proveslabel\vee)$}
1434: {\Delta \proves \Gamma, A\vee B^{\mu}_X,
1435: A^{\mu}_X, B^{\mu}_X}
1436: {\Delta \proves \Gamma, A\vee B^{\mu}_X}
1437: \]
1438: \[
1439: \derivi{$(\proveslabel\imp)$}
1440: {\Delta, A^{\mu}_X \proves \Gamma, A\imp B^{\mu}_X,
1441: B^{\mu}_X}
1442: {\Delta \proves \Gamma, A\imp B^{\mu}_X}
1443: \]
1444: \item
1445: disjunctive:
1446: \[
1447: \derivii{$(\proveslabel\wedge)$}
1448: {\Delta \proves \Gamma, A\wedge B^{\mu}_X,
1449: A^{\mu}_X}
1450: {\Delta \proves \Gamma, A\wedge B^{\mu}_X,
1451: B^{\mu}_X}
1452: {\Delta \proves \Gamma, A\wedge B^{\mu}_X}
1453: \]
1454: \[
1455: \derivii{$(\vee\proveslabel)$}
1456: {\Delta, A\vee B^{\mu}_X,
1457: A^{\mu}_X \proves \Gamma}
1458: {\Delta, A\vee B^{\mu}_X,
1459: B^{\mu}_X \proves \Gamma}
1460: {\Delta, A\vee B^{\mu}_X \proves \Gamma}
1461: \]
1462: \[
1463: \derivii{$(\imp\proveslabel)$}
1464: {\Delta, A\imp B^{\mu}_X \proves
1465: A^{\mu}_X, \Gamma}
1466: {\Delta, A\imp B^{\mu}_X,
1467: B^{\mu}_X \proves \Gamma}
1468: {\Delta, A\imp B^{\mu}_X \proves \Gamma}
1469: \]
1470: \item
1471: possibility---where $\eta$ is $\eta^u_{\Box_i A}(\mu,X)$ for
1472: some $u$:
1473: \[
1474: \derivi{$(\proveslabel\Box)$}
1475: {\Delta \proves \Gamma, \Box_i A^{\mu}_X, A^{\mu\eta}_{X,\mu\eta}}
1476: {\Delta \proves \Gamma, \Box_i A^{\mu}_X}
1477: \]
1478: \item
1479: necessity---subject to the side condition ${\cal S}, \Xi_{\nu}
1480: \triangleright \mu/\mu\nu:i$:
1481: \[
1482: \derivi{$(\Box\proveslabel)$}
1483: {\Delta, \Box_i A^{\mu}_X,
1484: A^{\mu\nu}_{X,\mu\nu} \proves \Gamma}
1485: {\Delta, \Box_i A^{\mu}_X \proves \Gamma}
1486: \]
1487: \item
1488: existential---subject to the side condition that $h$ is
1489: $h^u_B(\mu,X)$ for $B^{\mu}_X$ the principal of the rule (either
1490: $\exists x A$ or $\forall x A$) and some $u$:
1491: \[
1492: \derivi{$(\exists\proveslabel)$}
1493: {\Delta,
1494: \exists x A^{\mu}, A[h/x]^{\mu}_{X,h} \proves \Gamma}
1495: {\Delta, \exists x A^{\mu}_X \proves \Gamma}
1496: \;\;\;\;\;\;\;\;\;\;\;\;\;\;
1497: \derivi{$(\proveslabel\forall)$}
1498: {\Delta \proves \Gamma,
1499: \forall x A^{\mu}_X, A[h/x]^{\mu}_{X,h}}
1500: {\Delta \proves \Gamma, \forall x A^{\mu}_X}
1501: \]
1502: \item
1503: universal---subject to the side condition ${\cal S},
1504: \Xi_{t,\mu} \triangleright t:\mu$:
1505: \[
1506: \derivi{$(\forall\proveslabel)$}
1507: {\Delta, \forall x A^{\mu}_X, A[t/x]^{\mu}_{X,t}
1508: \proves \Gamma}
1509: {\Delta, \forall x A^{\mu}_X \proves \Gamma}
1510: \;\;\;\;\;\;\;\;\;\;\;\;\;\;
1511: \derivi{$(\proveslabel\exists)$}
1512: {\Delta \proves \Gamma,
1513: \exists x A^{\mu}_X, A[t/x]^{\mu}_{X,t}}
1514: {\Delta \proves \Gamma, \exists x A^{\mu}_{X}}
1515: \]
1516: \end{enumerate}
1517: \end{definition}
1518: %
1519: A ${\cal S}$-proof or ${\cal S}$-derivation for a sequent $\Delta
1520: \proves \Gamma$ is a tree built by application of these inference
1521: figures (in such a way that any side conditions are met for regime
1522: ${\cal S}$), with instances of the axiom as leaves and with the sequent
1523: $\Delta \proves \Gamma$ at the root. A tree similarly constructed
1524: except for containing some arbitrary sequent \m S as a leaf is a
1525: \emph{derivation from} \m S.
1526:
1527: I state the correctness theorem for this proof theory in a way
1528: that highlights the continuity with previous work on modal logic,
1529: particularly \cite{fitting:proof}.
1530: %
1531: \begin{thrm}[Soundness and Completeness]\label{sem-thrm}
1532: Suppose there is an ${\cal S}$-proof for a sequent $\proves
1533: A$. Then $A$ is valid. Conversely, if there is no ${\cal
1534: S}$-proof for the sequent $\proves A$ then there is a model ${\cal
1535: M}$ (that respects ${\cal S}$) and world $w$ such that ${\cal M}, w
1536: \not \forces A$.
1537: \end{thrm}
1538: %
1539: I merely sketch a proof here, which involves simply applying
1540: the standard techniques of
1541: \cite{fitting:proof,lincoln/shankar:search}. It is convenient to
1542: prove an intermediate result, using slightly modified sequent
1543: calculus SCE which imposes an eigenvariable condition on the
1544: possibility and existential rules---$u$ must be new. We can show
1545: the soundness of SCE by adapting the arguments presented in
1546: \cite[2.3]{fitting:proof} and \cite[5.3]{fitting/mendelsohn}.
1547: Meanwhile, we can follow \cite{fitting:proof} in developing the
1548: completeness argument in terms of \emph{analytic consistency
1549: properties} for the modal language. This argument can be seen as a
1550: formalization of the motivation for sequent calculi in the
1551: systematic search for models. Now, modal formulas may be satisfied
1552: only in infinite models, so the completeness theorem effectively
1553: requires us to consider infinite sequences of applications of
1554: sequent rules. In moving to infinite sets in this way, we must
1555: formally move from deductions, viewed as syntactic objects, to a
1556: more abstract, algebraic characterization of sets of modal
1557: formulas.
1558:
1559: We can now establish the correctness of SCL by syntactic
1560: methods, which relate SCL proofs to SCE proofs. Suppose $\Gamma$
1561: and $\Delta$ contains sentences of $L($CONST$)$ (labeled with the
1562: empty prefix). Completeness is immediate: if there is an SCE proof
1563: for $\Gamma \proves \Delta$, that very proof is also an SCL proof
1564: of $\Gamma \proves \Delta$. Conversely, the soundness theorem says
1565: that if there is an SCL proof of $\Gamma \proves \Delta$, then
1566: there is an SCE proof for $\Gamma \proves \Delta$. We establish
1567: this by simply adapting the general Herbrand theorem of
1568: \cite{lincoln/shankar:search} to SCE. The idea behind the
1569: soundness result is that the structure of Herbrand terms provides
1570: enough information to reconfigure an SCL proof (by an inductive
1571: process of interchanges of inference, like that considered next in
1572: Section~\ref{uniform-proof-subsec}) so that equivalents of the
1573: eigenvariable conditions are enforced. The SCL proof may then be
1574: reindexed to respect SCE's eigenvariable requirements. $\qed$
1575:
1576: \subsection{Permutability of inference and uniform proofs}
1577: \label{uniform-proof-subsec}
1578:
1579: Our syntactic methods for reasoning about derivations exploit
1580: \emph{permutability of inference}---the general ability to
1581: transform derivations so that inferences are interchanged
1582: \cite{kleene:permute}. To develop the notion of permutability of
1583: inference, we need to make some observations about the SCL sequent
1584: rules. First, the reasoning that is performed in subderivations is
1585: reasoning about subformulas (and vice versa). That is, in any spur
1586: sequent, the occurrence of the principal expression and the side
1587: expression all correspond to---or as we shall say, \emph{are based
1588: in}---the occurrence of the principal expression in the base
1589: sequent. Likewise, each of the remaining expressions in the spur
1590: \emph{are based in} an occurrence of an identical expression in the
1591: base. Here, as in \cite{kleene:permute}, we are assuming an
1592: \emph{analysis} of each inference to specify this correspondence in
1593: the case where the same expression has multiple occurrences in the
1594: base or in a spur. Thus, our proof techniques, where they involve
1595: copying derivations, sometimes involve (implicit) reanalyses of
1596: inferences.
1597:
1598: Now, in any derivation, the spur of one inference serves as the
1599: base for an \emph{adjacent} inference or an axiom. We can therefore
1600: associate any tracked prefixed formula occurrence $E$ in any sequent in
1601: the derivation with the occurrence in the root (or \emph{end-sequent})
1602: which $E$ is based in. A similar notion can relate inferences, as
1603: follows. Suppose $O$ is the inference at the root of a (sub)derivation,
1604: and $L$ is another inference in the (sub)derivation. Then $L$ \emph{is
1605: based in} an expression $E$ in the spur of $O$ if the principal
1606: expression of $L$ is based in $E$; $L$ \emph{is based in} $O$ itself if
1607: $E$ is a side expression of $O$. An important special case is that of
1608: an axiom based in an inference $O$. In effect, such an axiom marks a
1609: contribution that inference $O$ contributes to completing the deduction.
1610:
1611: To define interchanges of inference, we appeal to the two
1612: basic operations of \emph{contraction} and \emph{weakening}, which
1613: we cast as transformations on proofs. (In other proof systems,
1614: contraction and weakening may be introduced as explicit
1615: \emph{structural rules}.)
1616: %
1617: \begin{lemma}[Weakening]
1618: Let ${\cal D}$ be an SCL proof, let $\Delta_0$ be a finite
1619: multiset of tracked prefixed definitions and let $\Gamma_0$ be a
1620: finite multiset of tracked prefixed goals (in the same language as
1621: ${\cal D}$). Denote by $\Delta_0+{\cal D}+\Gamma_0$ a derivation
1622: exactly like ${\cal D}$, except that where any node in ${\cal D}$
1623: carries $\Delta \proves \Gamma$, the corresponding node in
1624: $\Delta_0+{\cal D}+\Gamma_0$ carries $\Delta,\Delta_0 \proves
1625: \Gamma, \Gamma_0$. (When $\Delta_0$ or $\Gamma_0$ is empty, we
1626: drop the corresponding $+$ from the notation.) Then
1627: $\Delta_0+{\cal D}+\Gamma_0$ is also an SCL proof.
1628: \end{lemma}
1629: %
1630: \begin{lemma}[Contraction]
1631: Let ${\cal D}$ be an SCL proof whose root carries $\Delta \proves
1632: \Gamma, E, E$. Then we can construct an SCL proof ${\cal D}'$ whose
1633: root carries $\Delta \proves \Gamma, E$, whose height is at most the
1634: height of ${\cal D}$ and where there is a one-to-one correspondence
1635: (also preserving order of inferences) that takes any inference of ${\cal
1636: D}'$ to an inference with the same principal and side expressions in
1637: ${\cal D}$. We can likewise transform an SCL proof ${\cal D}$ whose
1638: root carries $\Delta, E, E \proves \Gamma$ into an SCL proof ${\cal D}'$
1639: whose root carries $\Delta, E \proves \Gamma$.
1640: \end{lemma}
1641: %
1642: These lemmas follow from straightforward induction on the
1643: structure of derivations. These consequences continue to hold,
1644: suitably adapted, for the intermediate proof systems that we will
1645: construct from SCL in later sections.
1646:
1647: Now consider two adjacent inferences in a derivation, a base
1648: inference $R$ and an inference $S$ (whose base is a spur of $R$).
1649: If $S$ is not based in $R$, we may replace the derivation rooted at
1650: the base of $R$ by a new derivation of the same end-sequent in
1651: which $S$ applies at the root, $R$ applies adjacent, and the
1652: remaining subderivations are copied from the original derivation
1653: (but possibly weakened to reflect the availability of additional
1654: logical premises). Performing such a replacement constitutes an
1655: interchange of rules $R$ and $S$ and demonstrates the permutability
1656: of $R$ over $S$; see \cite{kleene:permute}. SCL is formulated so
1657: that any such pair of inferences may be exchanged in this way.
1658:
1659: We also observe that we can correctly introduce an
1660: abbreviation for goal occurrences of \mbox{$\Box_i(A\imp B)$} by a
1661: single formula $(\m A >_i \m B)$ and the consolidation of
1662: corresponding inferences $(\proveslabel\Box_i)$ and
1663: $(\proveslabel\imp)$ into a single figure $(\proveslabel>_i)$,
1664: while retaining unrestricted interchange of inference. Again when
1665: the inference applies to principal $A^{\mu}_X$, the figure is
1666: formulated using $\eta$ for $\eta^u_A(\mu,X)$ as:
1667: %
1668: \[
1669: \derivi{$\proveslabel>_i$}
1670: {\Gamma, \m A^{\mu\eta}_{X,\mu\eta} \proves
1671: \m B^{\mu\eta}_{X,\mu\eta}, \m A>_i\m B^{\mu}_X, \Delta}
1672: {\Gamma \proves \m A >_i \m B^{\mu}_X, \Delta}
1673: \]
1674: %
1675: We will refer to the calculus using $(\proveslabel>_i)$ in
1676: place of $(\proveslabel\Box_i)$ and $(\proveslabel\imp)$ as SCLI,
1677: and consider SCLI in the sequel.
1678:
1679: \cite{dale:forum,miller:tcs96} uses Definition
1680: \ref{uniform-def} to characterize \emph{abstract logic programming
1681: languages}.
1682: %
1683: \begin{definition} \label{uniform-def}
1684: A cut-free sequent proof ${\cal D}$ is {\em uniform} if for for
1685: every subproof ${\cal D}'$ of ${\cal D}$ and for every non-atomic
1686: formula occurrence \m B in the right-hand side of the end-sequent of
1687: ${\cal D}'$ there is a proof ${\cal D}''$ that is equal to ${\cal D}'$
1688: up to a permutation of inferences and is such that the base inference in
1689: ${\cal D}''$ introduces the top-level logical connective of \m B.
1690: \end{definition}
1691: %
1692: \begin{definition} \label{alp-def}
1693: A logic with a sequent calculus proof system is an {\em
1694: abstract logic programming language} if restricting to uniform
1695: proofs does not lose completeness.
1696: \end{definition}
1697: %
1698: It is easy to show that the sequent calculi SCL and SCLI are
1699: abstract logic programming languages in this sense. In fact, by
1700: this definition \emph{every} SCL or SCLI derivation is uniform.
1701:
1702: To anticipate our analysis of permutability in later sections,
1703: let us introduce the notion of an \emph{eager} derivation in SCL
1704: or SCLI.
1705: %
1706: \begin{definition} \label{delay-def}
1707: Consider a derivation ${\cal D}$ containing a right inference
1708: \m R that applies to principal $E$. \m R is {\em delayed} exactly
1709: when there is a subderivation ${\cal D}'$ of ${\cal D}$ where:
1710: ${\cal D}'$ contains R; ${\cal D}'$ has a left inference $L$ at the
1711: root; and the principal $E$ of $R$ is based in an occurrence of $E$
1712: in the end-sequent of ${\cal D}'$.
1713: \end{definition}
1714: %
1715: Consider this schematic diagram of such a subderivation ${\cal
1716: D}'$:
1717: \[
1718: \begin{derive}{
1719: \vdots
1720: }
1721: \derivitem{$R$}{
1722: \begin{array}{c}\ldots E \ldots \\
1723: \downarrow
1724: \end{array}}
1725: \derivitem{$L$}{
1726: \ldots E \ldots
1727: }
1728: \end{derive}
1729: \]
1730: On an intuitive conception of a sequent proof as a record of
1731: proof search constructed from root upwards, \m R is delayed in that
1732: we have waited in ${\cal D}$ to apply \m R until after consulting
1733: the program by applying \m L, when we might have applied \m R
1734: earlier. Thus, we will also say in the circumstances of
1735: Definition~\ref{delay-def} that $R$ is delayed \emph{with respect
1736: to} $L$.
1737: %
1738: \begin{definition} \label{eager-def}
1739: ${\cal D}$ is {\em eager} exactly when it contains no delayed
1740: applications of right rules.
1741: \end{definition}
1742: %
1743: By transforming any derivation ${\cal D}$ into an eager
1744: derivation ${\cal D}'$ by permutations of inferences, we make it
1745: clear that reasoning about goals can always precede reasoning with
1746: program statements, and thereby provide a starting point for
1747: further analysis of goal-directed proof search.
1748:
1749: \begin{thrm} \label{eager-thrm}
1750: Any SCL(I) derivation ${\cal D}$ is equal to an eager derivation
1751: ${\cal D}'$ up to permutations of inferences.
1752: \end{thrm}
1753: %
1754: The {\bf proof} follows \cite[Theorem 2]{kleene:permute}. A
1755: double induction transforms each derivation into an eager one; the
1756: inner induction rectifies the final rule of a derivation whose
1757: subderivations are eager by an interchange of inferences (and
1758: induction) \cite[Lemma 10]{kleene:permute}; the outer one rectifies
1759: a derivation by rectifying the furthest violation from the root
1760: (and induction). See Appendix~\ref{eager-proof-sec}. $\qed$
1761:
1762: \section{Modular goal-directed proof search}
1763: \label{module-sec}
1764:
1765: \subsection{Overview}
1766: \label{final-subsec}
1767:
1768: Eager derivations do not make a satisfactory specification for
1769: goal-directed proof in a logic programming sense, because they do
1770: not embody a particularly directed search strategy. For one thing,
1771: eager derivations are free to work in parallel on different
1772: disjuncts of a goal using different program statements; in logic
1773: programming we want \emph{segments} in which a single program
1774: statement and a single goal is in force. Moreover, eager derivations
1775: can reuse work across separate case analyses; in logic programming
1776: we want \emph{blocks} where particular cases are investigated
1777: separately. Finally, because of their classical formulation, eager
1778: derivations do not enforce or exploit any modularity in their
1779: underlying logic. Our task is to remedy these faults of eager
1780: derivations.
1781:
1782: Our result takes the form of an alternative sequent calculus
1783: SCLP which is equivalent to SCL. SCLP enforces a strictly
1784: goal-directed proof search through the structure of its inferences.
1785: First, SCLP sequents take the form
1786: \[
1787: \Gamma; U \proves V; \Delta
1788: \]
1789: We understand $\Gamma$ to specify the global program and
1790: $\Delta$ to specify the global restart goals; both are multisets of
1791: tracked, prefixed formulas. $U$ is at most one tracked, prefix
1792: formula, representing the current program statement; $V$ is at most
1793: one tracked, prefixed formula, representing the current goal.
1794:
1795: Logical rules apply only to the current program statement and
1796: the current goal. In addition, if there is a current program
1797: statement $U$ then the current goal $V$ must be an atomic formula.
1798: Thus, the interpreter first breaks the goal down into its
1799: components. Once an atomic goal is derived, the program is
1800: consulted; the selected program statement is decomposed and matched
1801: against the current goal by applicable logical rules. The form of
1802: the $(\imp\proveslabel)$ figure ensures that the interpreter
1803: continues to work on at most one goal at any time; this gives SCLP
1804: proofs their segment structure. Meanwhile, the form of the
1805: $(\vee\proveslabel)$ figures specify no current goal in its second
1806: case. The new current goal can then be chosen flexibly from
1807: possible restart goals. This gives SCLP proofs their block
1808: structure.
1809:
1810: The new inferences are presented in
1811: Definition~\ref{lp-seq-fig-a} and~\ref{lp-seq-fig-b}.
1812: Definition~\ref{lp-seq-fig-a} shows the rules for decomposing
1813: program statements; Definition~\ref{lp-seq-fig-b} shows the rules
1814: for decomposing goals.
1815: %
1816: \begin{definition}[Logic programming calculus---programs] \label{lp-seq-fig-a}
1817: The following inference figures describe the logic programming
1818: sequent calculus SCLP as it applies to program statements.
1819: \begin{enumerate}
1820: \item
1821: axiom---$A$ atomic:
1822: \[
1823: \Gamma ; \m A^{\nu} \proves \m A^{\nu} ; \Delta
1824: \]
1825: \item
1826: decision (program consultation)---again $A$ atomic:
1827: \[
1828: \derivi{decide}
1829: {\Gamma, \m P^{\mu}_X ; \m P^{\mu}_X
1830: \proves \m A^{\nu}_Y ; \Delta}
1831: {\Gamma, \m P^{\mu}_X ;
1832: \proves \m A^{\nu}_Y ; \Delta}
1833: \]
1834: \item
1835: conjunctive:
1836: \[
1837: \derivi{$\wedge\proveslabel_{\s L}$}
1838: {\Gamma ; \m P^{\mu}_X \proves
1839: \m A^{\nu}_Y ; \Delta}
1840: {\Gamma ; \m P\wedge\m Q^{\mu}_X \proves
1841: \m A^{\nu}_Y ; \Delta}
1842: \]
1843: \[
1844: \derivi{$\wedge\proveslabel_{\s R}$}
1845: {\Gamma ; \m Q^{\mu}_X \proves
1846: \m A^{\nu}_Y ; \Delta}
1847: {\Gamma ; \m P\wedge\m Q^{\mu}_X \proves
1848: \m A^{\nu}_Y ; \Delta}
1849: \]
1850: \item
1851: disjunctive:
1852: \[
1853: \derivii{$\vee\proveslabel_{\s L}$}
1854: {\Gamma ; \m P^{\mu}_X \proves \m A^{\nu}_Y ; \Delta}
1855: {\Gamma, \m Q^{\mu}_X ; \proves ; \Delta}
1856: {\Gamma ; \m P \vee \m Q^{\mu}_X \proves \m A^{\nu}_Y ; \Delta}
1857: \]
1858: \[
1859: \derivii{$\vee\proveslabel_{\s R}$}
1860: {\Gamma ; \m Q^{\mu}_X \proves \m A^{\nu}_Y ; \Delta}
1861: {\Gamma, \m P^{\mu}_X ; \proves ; \Delta}
1862: {\Gamma ; \m P \vee \m Q^{\mu}_X \proves \m A^{\nu}_Y ; \Delta}
1863: \]
1864: \item
1865: implication:
1866: \[
1867: \derivii{$\imp\proveslabel$}
1868: {\Gamma ; \proves \m Q^{\mu}_X ; \Delta }
1869: {\Gamma ; \m P^{\mu}_X \proves
1870: \m A^{\nu}_Y ; \Delta}
1871: {\Gamma ; \m Q \imp \m P^{\mu}_X \proves
1872: \m A^{\nu}_Y ; \Delta}
1873: \]
1874: \item
1875: necessity---subject to the side condition that there is a
1876: typing derivation ${\cal S}, \Xi_{\nu} \triangleright
1877: \mu/\mu\nu:i$:
1878: \[
1879: \derivi{$\Box_{\s i}\proveslabel$}
1880: {\Gamma ; \m P^{\mu\nu}_{X,\mu\nu}
1881: \proves \m A^{\nu'}_Y ; \Delta}
1882: {\Gamma, \Box_{\s i} \m P^{\mu}_X
1883: \proves \m A^{\nu'}_Y ; \Delta}
1884: \]
1885: \item
1886: existential---subject to the side condition that $h$ is
1887: $h^u_{\exists x P}(\mu,X)$ for some $u$:
1888: \[
1889: \derivi{$\exists\proveslabel$}
1890: {\Gamma ; \m P[\m h/\m x])^{\mu}_{X,h}
1891: \proves \m A^{\nu}_Y ; \Delta}
1892: {\Gamma ; \exists \m x. \m P^{\mu}_X
1893: \proves \m A^{\nu}_Y ; \Delta}
1894: \]
1895: \item
1896: universal---subject to the side condition that there is a
1897: typing derivation ${\cal S}, \Xi_{t,\mu} \triangleright t:\mu$:
1898: \[
1899: \derivi{$\forall\proveslabel$}
1900: {\Gamma ; \m P[\m t/\m x]^{\mu}_{X,t}
1901: \proves \m A^{\nu}_Y ; \Delta}
1902: {\Gamma ; \forall \m x. \m P^{\mu}_X
1903: \proves \m A^{\nu}_Y ; \Delta}
1904: \]
1905: \end{enumerate}
1906: \end{definition}
1907:
1908: \begin{definition}[Logic programming calculus---goals] \label{lp-seq-fig-b}
1909: The following inference figures describe the logic programming
1910: sequent calculus SCLP as it applies to goals.
1911: \begin{enumerate}
1912: \item
1913: restart:
1914: \[
1915: \derivi{restart}
1916: {\Gamma ;
1917: \proves \m G^{\nu}_X ; \m G^{\nu}_X, \Delta}
1918: {\Gamma ;
1919: \proves ; \m G^{\nu}_X, \Delta}
1920: \]
1921: \item
1922: conjunctive goals:
1923: \[
1924: \derivii{$\proveslabel\wedge$}
1925: {\Gamma ; \proves \m F^{\mu}_X ; \Delta}
1926: {\Gamma ; \proves \m G^{\mu}_X ; \Delta}
1927: {\Gamma ; \proves \m F \wedge \m G^{\mu}_X ; \Delta}
1928: \]
1929: \item
1930: disjunctive goals:
1931: \[
1932: \derivi{$\proveslabel\vee_{\s L}$}
1933: {\Gamma ; \proves \m F^{\mu}_X ; \Delta}
1934: {\Gamma ; \proves \m F \vee \m G^{\mu}_X ; \Delta}
1935: \]
1936: \[
1937: \derivi{$\proveslabel\vee_{\s R}$}
1938: {\Gamma ; \proves \m G^{\mu}_X ; \Delta}
1939: {\Gamma ; \proves \m F \vee \m G^{\mu}_X ; \Delta}
1940: \]
1941: \item
1942: necessary goals---where $\eta$ is $\eta^u_A(\mu,X)$ for
1943: $A^{\mu}_X$ the principal of the rule and for some $u$ for which
1944: $\eta^u_A$ does not occur in $\Delta$ or $\Gamma$:
1945: \[
1946: \derivi{$\proveslabel\Box_{\s i}\imp$}
1947: {\Gamma, \m F^{\mu\eta}_{X,\mu\eta} ; \proves
1948: \m G^{\mu\eta}_{X,\mu\eta} ; \m G^{\mu\eta}_{X,\mu\eta}, \Delta}
1949: {\Gamma ; \proves \m F \bimp_i \m G^{\mu}_X ; \Delta}
1950: \]
1951: \[
1952: \derivi{$\proveslabel\Box_{\s i}$}
1953: {\Gamma ; \proves
1954: \m G^{\mu\eta}_{X,\eta} ; \m G^{\mu\eta}_{X,\mu\eta}, \Delta }
1955: {\Gamma ; \proves
1956: \Box_{\s i} \m G^{\mu}_X ; \Delta}
1957: \]
1958: \item
1959: universal goals---subject to the side condition that $h$ is
1960: $h^u_{\forall x G}(\mu,X)$ for some $u$:
1961: \[
1962: \derivi{$\proveslabel\forall$}
1963: {\Gamma ; \proves \m G[\m h/\m x]^{\mu}_{X,h} ; \Delta}
1964: {\Gamma ; \proves
1965: \forall \m x. \m G^{\mu}_X ; \Delta}
1966: \]
1967: \item
1968: existential goals---subject to the side condition that there is a
1969: typing derivation ${\cal S}, \Xi_{t,\mu} \triangleright t:\mu$:
1970: \[
1971: \derivi{$\proveslabel\exists$}
1972: {\Gamma ; \proves
1973: \m G[\m t/\m x]^{\mu}_{X,t} ; \Delta}
1974: {\Gamma ; \proves
1975: \exists \m x. \m G^{\mu}_X ; \Delta}
1976: \]
1977: \end{enumerate}
1978: \end{definition}
1979:
1980: Inspection of the figures of Definitions~\ref{lp-seq-fig-a}
1981: and~\ref{lp-seq-fig-b} reveals the following generalization of
1982: modularity and locality: in any derivation, the label of the
1983: current program statement must be a prefix of the label of the
1984: current goal. Moreover, goal labels are always extended with novel
1985: symbols, because of the eigenvariable condition in the
1986: $(\proveslabel\Box)$ figure. Inductively, these facts determine a
1987: strong invariant---consider a block beginning with a restart
1988: inference whose spur is
1989: \[
1990: \Gamma; \proves G^{\nu}_X ; \Delta
1991: \]
1992: and consider any expression $P^{\mu}_Y$ in $\Gamma$. If $\mu$
1993: is not a prefix of $\nu$, then $\mu$ will not be a prefix of the
1994: label of any goal formula in the block. Thus $P^{\mu}_Y$ cannot be
1995: used in the block. (Compare \cite[Lemma 2]{permute-paper}.)
1996:
1997: This is why the (restart) rule of SCLP can be made modular, so
1998: that it limits the work that is reanalyzed to the scope of the
1999: ambiguity just introduced. We must simply show that the new
2000: disjunct will contribute to its restart goal. In particular,
2001: define canceled blocks as in Definition~\ref{canceled-def}.
2002: %
2003: \begin{definition}[Linked] \label{link-def}
2004: An expression $E$ in a sequent in an SCLU derivation ${\cal
2005: D}$ is \emph{linked} if the principal formula of an axiom in the
2006: same block of ${\cal D}$ as that sequent is based in $E$. An
2007: inference \m R is \emph{linked} in ${\cal D}$ if some side
2008: expression of $R$ is linked in each spur of $R$. A derivation or
2009: block is \emph{linked} iff all of the inferences in it are linked.
2010: \end{definition}
2011: %
2012: \begin{definition}[Canceled]\label{canceled-def}
2013: A block is \emph{canceled} if it contains the root of ${\cal
2014: D}$, or if the side expression $E$ of the $(\vee\proveslabel)$
2015: inference whose spur is the root of the block is linked.
2016: \end{definition}
2017: %
2018: Thus a canceled block includes a use of any disjunctive case
2019: introduced in the block. The key fact about SCLP is that it
2020: suffices to consider only canceled blocks in proof search.
2021: %
2022: \begin{thrm}
2023: \label{lp-sequent-thrm}
2024: Let $\Gamma$ and $\Delta$ be multisets of tracked prefixed
2025: expression in which each formula is tracked by the empty set and
2026: prefixed by the empty prefix. There is a proof of $\Gamma \proves
2027: \Delta$ in SCL exactly when there is a proof of $\Gamma; \proves
2028: ;\Delta$ in SCLP in which every block is canceled.
2029: \end{thrm}
2030: %
2031: The discussion of the following subsections represents an
2032: outline of the proof of this result. The strategy is to transform
2033: eager proofs from SCL to SCLP by a series of refinements of sequent
2034: rules that make the logic programming strategy explicit. We give
2035: force to the idea that the interpreter has a current goal and
2036: current program statement, in Section~\ref{segment-subsec}. Then
2037: we create blocks for case analysis, in Section~\ref{block-subsec}.
2038: Finally, we enforce modularity, in Section~\ref{modularity-subsec}.
2039: See also Appendix~\ref{lp-proof-sec}.
2040:
2041: Figure~\ref{sclp-fig} shows how the proof of
2042: Figure~\ref{explicit-modular-fig} is recast in SCLP.
2043: %
2044: \begin{figure}
2045: \small
2046: \begin{center}
2047: \begin{tabular}{rl}
2048: \fbox{$2'$} &
2049: {\derivi{(restart)}
2050: {\derivi{(decide)}
2051: {\derivii{$(\imp\proveslabel)$}
2052: {\derivi{(decide)}
2053: {\ldots; C \proves C; F}
2054: {\ldots, C; \proves C; F}}
2055: {\ldots; F \proves F; F}
2056: { C, \ldots; C \imp F \proves F;F}}
2057: { C \imp F, C \ldots; \proves F;F}}
2058: {A \vee B, C\vee D, A \imp F, C \imp F, (B\wedge D)
2059: \imp F, B, C; \proves ;F}}
2060: \\[2em]
2061: \fbox{$3'$} &
2062: \derivi{(restart)}
2063: {\derivi{(decide)}
2064: {\derivii{$(\imp\proveslabel)$}
2065: {\derivii{$(\proveslabel\wedge)$}
2066: {\derivi{(decide)}
2067: {\ldots; B \proves B; F}
2068: {B, \ldots; \proves B; F}}
2069: {\derivi{(decide)}
2070: {\derivii{$(\vee\proveslabel_R)$}
2071: { \ldots; D \proves D; F}
2072: {\fbox{$2'$}}
2073: { \ldots; C \vee D \proves D;F}}
2074: {C\vee D, \ldots; \proves D;F}}
2075: {C\vee D, B, \ldots; \proves B\wedge D;F}}
2076: {\ldots; F \proves F; F}
2077: {C\vee D, B, \ldots; (B\wedge D) \imp F \proves F;F}}
2078: {C\vee D, (B\wedge D) \imp F, B, \ldots; \proves F;F}}
2079: {A \vee B, C\vee D, A \imp F, C \imp F, (B\wedge D)
2080: \imp F, B; \proves ;F}
2081: \\[2em]
2082: \fbox{1} &
2083: \derivi{(restart)}
2084: {\derivi{(decide)}
2085: {\derivii{$(\imp\proveslabel)$}
2086: {\derivi{(decide)}
2087: {\derivii{$(\vee\proveslabel_L)$}
2088: {\ldots; A \proves A; F}
2089: {\fbox{$3'$}}
2090: {\ldots; A \vee B \proves A; F}}
2091: {A \vee B, \ldots; \proves A;F}}
2092: {\ldots; F \proves F; F}
2093: {A \vee B, \ldots; A \imp F \proves F;F}}
2094: {A \vee B, A \imp F, \ldots; \proves F;F}}
2095: {A \vee B, C\vee D, A \imp F, C \imp F, (B\wedge D)
2096: \imp F; \proves ;F}
2097: \end{tabular}
2098: \end{center}
2099: \caption{The SCLP presentation of the proof of
2100: Figure~\ref{explicit-modular-fig}.}
2101: \label{sclp-fig}
2102: \end{figure}
2103: %
2104: Figure~\ref{sclp-fig} extends
2105: Figure~\ref{explicit-modular-fig} to make the bookkeeping of
2106: goal-directed proof explicit. In Figure~\ref{sclp-fig}, the
2107: informal underline of Figure~\ref{explicit-modular-fig} is gone,
2108: and instead the current goal and the current program statement are
2109: displayed at distinguished positions in sequents. New (restart)
2110: and (decide) inferences mark the consideration of new goals and new
2111: program statements. Of course, the logical content of the two
2112: inferences is identical. Applying Definition~\ref{canceled-def},
2113: block \fbox{1} is canceled because it contains the root; there is
2114: no new disjunct to discharge here. Block \fbox{$3'$} is canceled:
2115: the inference whose spur is the root of block \fbox{$3'$} is the
2116: $(\vee\proveslabel_L)$ and its side expression is an occurrence of
2117: $B$, the new disjunct in the block. This occurrence is linked in
2118: the block because of the leftmost axiom $\ldots;B\proves B;F$ which
2119: is based in it; the inference $(\vee\proveslabel_L)$ is linked in
2120: the block for the same reason. Similarly block \fbox{$2'$} is
2121: canceled because the new disjunct $C$ (the side expression of the
2122: $(\vee\proveslabel_R)$ inference whose spur is the root of block
2123: \fbox{$2'$}) contributes to the leftmost axiom $\ldots;C\proves
2124: C;F$ in the block.
2125:
2126: Figure~\ref{sclp-fig2} shows how the proof of
2127: Figure~\ref{structure-module-fig} is recast in SCLP.
2128: %
2129: \begin{figure}
2130: \small
2131: \begin{center}
2132: \begin{tabular}{rl}
2133: \fbox{5} &
2134: \derivi{(restart)}
2135: {\derivi{(decide)}
2136: {\derivi{$(\Box\proveslabel)$}
2137: {\derivii{$(\imp\proveslabel)$}
2138: {\derivi{(decide)}
2139: {\ldots; B^{\alpha} \proves
2140: B^{\alpha}; \ldots}
2141: {\ldots, B^{\alpha} ; \proves
2142: B^{\alpha}; \ldots}}
2143: {\ldots; A^{\alpha} \proves
2144: A^{\alpha}; \ldots}
2145: {B^{\alpha}, \ldots; B \imp A^{\alpha} \proves
2146: A^{\alpha} ; \ldots}}
2147: {B^{\alpha}, \ldots; \Box (B \imp A) \proves
2148: A^{\alpha} ; \ldots}}
2149: {\Box (B \imp A), B^{\alpha} ; \proves A^{\alpha} ; \ldots}}
2150: {\Box (A \vee B), \Box (B \imp A), \Box (C \vee D), \Box (D
2151: \imp C), B^{\alpha}; \proves ; A^{\alpha}, (\Box A) \wedge (\Box C)}
2152: \\[2em]
2153: \fbox{6} &
2154: \derivi{(restart)}
2155: {\derivi{(decide)}
2156: {\derivi{$(\Box\proveslabel)$}
2157: {\derivii{$(\imp\proveslabel)$}
2158: {\derivi{(decide)}
2159: {\ldots; D^{\beta} \proves
2160: D^{\beta}; \ldots}
2161: {\ldots, D^{\beta} ; \proves
2162: D^{\beta}; \ldots}}
2163: {\ldots; C^{\beta} \proves
2164: C^{\beta}; \ldots}
2165: {D^{\beta}, \ldots; D \imp C^{\beta} \proves
2166: C^{\beta} ; \ldots}}
2167: {D^{\beta}, \ldots; \Box (D \imp C) \proves
2168: C^{\beta} ; \ldots}}
2169: {\Box (D \imp C), D^{\beta} ; \proves C^{\beta} ; \ldots}}
2170: {\Box (A \vee B), \Box (B \imp A), \Box (C \vee D), \Box (D
2171: \imp C), D^{\beta}; \proves ; C^{\beta}, (\Box A) \wedge (\Box C)}
2172: \\[2em]
2173: \fbox{4} &
2174: \derivi{(restart)}
2175: {\derivii{$(\proveslabel\wedge)$}
2176: {\derivi{$(\proveslabel\Box)$}
2177: {\derivi{(decide)}
2178: {\derivi{$(\Box\proveslabel)$}
2179: {\derivii{$(\vee\proveslabel_L)$}
2180: {\ldots; A^{\alpha} \proves A^{\alpha};
2181: \ldots}
2182: {\fbox{5}}
2183: {\ldots; A \vee B^{\alpha} \proves
2184: A^{\alpha}; \ldots}}
2185: {\ldots; \Box(A \vee B) \proves A^{\alpha}; \ldots}}
2186: {\Box (A \vee B), \ldots ;
2187: \proves A^{\alpha}; \ldots}}
2188: {\Box (A \vee B), \ldots ; \proves \Box A; \ldots}}
2189: %
2190: {\derivi{$(\proveslabel\Box)$}
2191: {\derivi{(decide)}
2192: {\derivi{$(\Box\proveslabel)$}
2193: {\derivii{$(\vee\proveslabel_L)$}
2194: {\ldots; C^{\beta} \proves C^{\beta};
2195: \ldots}
2196: {\fbox{6}}
2197: {\ldots; C \vee D^{\beta} \proves
2198: C^{\beta}; \ldots}}
2199: {\ldots; \Box(C \vee D) \proves C^{\beta}; \ldots}}
2200: {\Box (C \vee D), \ldots ;
2201: \proves C^{\beta}; \ldots}}
2202: {\Box (C \vee D), \ldots ; \proves \Box C; \ldots}}
2203: {\Box (A \vee B), \Box (C \vee D), \ldots ; \proves
2204: (\Box A) \wedge (\Box C); \ldots}}
2205: {\Box (A \vee B), \Box (B \imp A), \Box (C \vee D), \Box (D
2206: \imp C) ; \proves ; (\Box A) \wedge (\Box C)}
2207: \end{tabular}
2208: \end{center}
2209: \caption{The SCLP presentation of the proof of
2210: Figure~\ref{structure-module-fig}. We suppress tracking of
2211: formulas and hide the internal structure of Herbrand terms.}
2212: \label{sclp-fig2}
2213: \end{figure}
2214: %
2215: The most dramatic change here is that the inferences of
2216: Figure~\ref{sclp-fig2} are segmented out into three blocks.
2217: Another change is the discipline of explicit scope; we introduce a
2218: suitable term $\alpha$ to represent the generic context in which we
2219: prove $\Box A$ and another suitable term $\beta$ to represent the
2220: generic context in which we prove $\Box C$. Correspondingly, we
2221: transition to $\alpha$ in using $\Box(A\vee B)$ and transition to
2222: $\beta$ in using $\Box(C\vee D)$. In the (restarts) of \fbox{5}
2223: and \fbox{6} the changes interact. In \fbox{5} we pick the modular
2224: restart $A^{\alpha}$ in order to permit a contribution by the new
2225: assumption $B^{\alpha}$. In \fbox{6} we pick the modular restart
2226: $C^{\beta}$ in order to permit a contribution by the new assumption
2227: $D^{\beta}$.
2228:
2229: \subsection{Segment structure}
2230: \label{segment-subsec}
2231:
2232: Our first task is to formalize goal-directed search that
2233: directs attention to a single goal at a time. To distinguish such
2234: goals, we begin with a trick that for now is purely
2235: formal---introducing an \emph{articulated} SCLI. We represent
2236: assumptions as a pair $\Pi ; \Gamma$ with $\Pi$ encoding the global
2237: program and $\Gamma$ encoding local program statements; eventually
2238: local statements will be processed only in the current segment and
2239: then discarded. (Compare the similar notation and treatment from
2240: \cite{girard:lu}.) Similarly, we represent goals as a pair $\Delta
2241: ; \Theta$, with $\Theta$ encoding the restart goals and $\Delta$
2242: encoding the local goals; ultimately, we will also describe
2243: inference rules which will discard $\Delta$ between segments. With
2244: this representation, principal formulas of logical rules are local
2245: formulas, in $\Gamma$ or $\Delta$; so are the side formulas---with
2246: these exceptions: the $(\proveslabel\Box)$ and
2247: $(\proveslabel\bimp)$ rules augment $\Pi$ instead of $\Gamma$ (when
2248: they add a new program statement) and $\Theta$ instead of $\Delta$
2249: (when they add new restart goals).
2250:
2251: New (decide) and (restart) rules keep this change general;
2252: they allow a global formula---a program statement or restart goal---to
2253: be selected and added to the local state.
2254: %
2255: \[
2256: \begin{array}{l@{\hspace{1in}}l@{\hspace{1in}}}
2257: \derivi{(decide)}
2258: {\Pi, \m A^{\mu}_X ; \Gamma, \m A^{\mu}_X
2259: \proves \Delta ; \Theta}
2260: {\Pi, \m A^{\mu}_X ; \Gamma
2261: \proves \Delta ; \Theta}
2262: &
2263: \derivi{(restart)}
2264: {\Pi ; \Gamma
2265: \proves \Delta, \m G^{\mu}_X ; \Theta, \m G^{\mu}_X}
2266: {\Pi ; \Gamma
2267: \proves \Delta ; \Theta, \m G^{\mu}_X}
2268: \end{array}
2269: \]
2270: %
2271: \begin{lemma}[Articulation] \label{articulation-lemma}
2272: Every SCLI deduction can be converted into an articulated SCLI
2273: deduction with an end-sequent of the form $\Pi; \proves ;\Theta$ in such
2274: a way that if the initial derivation is eager then so is the resulting
2275: derivation (and vice versa).
2276: \end{lemma}
2277: %
2278: {\bf Proof}. Straightforward structural induction. $\qed$
2279:
2280: The next step is to introduce an inference figure
2281: $(\imp\proveslabel^S)$ that imposes a \emph{segment} structure on
2282: derivations, thus:
2283: \[
2284: \derivii{$(\imp\proveslabel^S)$}
2285: {\Pi ;
2286: \proves \m A^{\mu}_X, \Delta ; \Theta}
2287: {\Pi ;
2288: \Gamma, \m A \imp \m B^{\mu}_X, \m B^{\mu}_X
2289: \proves \Delta ; \Theta}
2290: {\Pi ; \Gamma,
2291: \m A \imp \m B^{\mu}_X
2292: \proves \Delta ; \Theta}
2293: \]
2294: %
2295: \begin{definition}[Segment]
2296: A \emph{segment} in a derivation ${\cal D}$ is a maximal tree
2297: of contiguous inferences in which the left subtree of any
2298: $(\imp\proveslabel^S)$ inference is omitted.
2299: \end{definition}
2300: %
2301: The distinctive feature of the $(\imp\proveslabel^S)$ figure
2302: is that the local results inferred from the program are discarded
2303: in the subderivation where the new goal is introduced. In an eager
2304: derivation, this will begin a new segment where first the new goal
2305: will be considered and then a new program statement will be
2306: selected to establish that goal.
2307:
2308: We will define two calculi using $(\imp\proveslabel^S)$. The
2309: first, SCLS, eliminates the $(\imp\proveslabel)$ inference of the
2310: articulated SCLI and instead has $(\imp\proveslabel^S)$. The
2311: second, SCLV, is a calculus like the articulated SCLI but also
2312: allows $(\imp\proveslabel^S)$; $(\imp\proveslabel)$ and
2313: $(\imp\proveslabel^S)$ can appear anywhere in an SCLV derivation.
2314: We introduce SCLV to facilitate the incremental transformation of
2315: articulated SCLI proofs into SCLS proofs.
2316:
2317: \begin{lemma} \label{segment-lemma}
2318: An eager articulated SCLI derivation whose end-sequent is of the
2319: form
2320: \[
2321: \Pi ; \proveslabel \Delta ; \Theta
2322: \]
2323: can be transformed to an eager SCLS derivation of the same
2324: end-sequent.
2325: \end{lemma}
2326:
2327: \textbf{Proof.} We proceed with an inductive construction
2328: that eliminates $(\imp\proveslabel)$ inferences in favor of
2329: $(\imp\proveslabel^S)$ inferences one at a time. See
2330: Appendix~\ref{segment-proof-subsec}. $\qed$
2331:
2332: \subsection{Block structure}
2333: \label{block-subsec}
2334:
2335: We now revise how we perform case analysis from assumptions.
2336: We introduce new rules where all local work is discarded in the
2337: subderivation written on the right. This corresponds to a sequent
2338: of the form $\Pi; \proves ;\Theta$. In addition, some
2339: \emph{global} work may be discarded in the right subderivation;
2340: this helps clarify the structure of derivations. Accordingly,
2341: there may be additional formula occurrences $\Pi'$ and $\Theta'$ in
2342: the base sequent that are not copied up to the right subderivation.
2343: Finally, the right subderivation may address either the (textually)
2344: first disjunct or the second disjunct. This leads to the two
2345: inference figures below.
2346: \[
2347: \begin{array}{c}
2348: \derivii{$\vee\proveslabel^B_L$}
2349: {\Pi, \Pi' ; \Gamma, \m A \vee \m B^{\mu}, \m A^{\mu}
2350: \proves \Delta ; \Theta, \Theta'}
2351: {\Pi, \m B^{\mu} ; \proves ; \Theta}
2352: {\Pi, \Pi' ; \Gamma, \m A \vee \m B^{\mu}
2353: \proves \Delta ; \Theta, \Theta'} \\
2354: \derivii{$\vee\proveslabel^B_R$}
2355: {\Pi, \Pi' ; \Gamma, \m A \vee \m B^{\mu}, \m B^{\mu}
2356: \proves \Delta ; \Theta, \Theta'}
2357: {\Pi, \m A^{\mu} ; \proves ; \Theta}
2358: {\Pi, \Pi' ; \Gamma, \m A \vee \m B^{\mu}
2359: \proves \Delta ; \Theta, \Theta'}
2360: \end{array}
2361: \]
2362: We call these inferences \emph{blocking} $(\vee\proveslabel)$
2363: inferences, or $(\vee\proveslabel^B)$ inferences. We will appeal
2364: to two calculi in which these inferences appear. The first, SCLU,
2365: permits both ordinary $(\vee\proveslabel)$ and
2366: $(\vee\proveslabel^B)$ inferences, without restriction. SCLU is
2367: convenient for describing transformations between proofs. The
2368: second, SCLB, permits $(\vee\proveslabel^B)$ inferences but not
2369: ordinary $(\vee\proveslabel)$ inferences.
2370:
2371: Blocks are more than just boundaries in the proof; they
2372: provide a locus for enforcing modularity. We will ensure that a
2373: disjunct contributes inferences to the new block where it is
2374: introduced. Thanks to this contribution, we can narrow down the
2375: choice of goals to restart in a modular way.
2376:
2377: This result is made possible only by maintaining the right
2378: structure as we introduce $(\vee\proveslabel^B)$ inferences. We
2379: use path prefixes to make explicit connections between program
2380: statements and any goals that they help establish. The key notions
2381: are \emph{spanning}, \emph{simplicity} and \emph{balance} for
2382: sequents. Spanned, simple and balanced sequents represent a
2383: consistent evolution of the state of proof search, which records a
2384: full set of restart goals and the corresponding assumptions, with
2385: no redundancy.
2386: %
2387: \begin{definition}[Carrier]
2388: The \emph{carrier} of a non-empty Herbrand prefix $\mu\eta$ is
2389: $B^{\mu\eta}_{X,\mu\eta}$ if $\eta$ is $\eta^u_{A\bimp_i B}(\mu,X)$
2390: and otherwise, when $\eta$ is $\eta^u_{\Box_i A}(\mu,X)$, is
2391: $A^{\mu\eta}_{X,\mu\eta}$.
2392: \end{definition}
2393: %
2394: \begin{definition}[Spanned]
2395: Say one multiset of tracked prefixed formulas, $\Pi$, is {\em
2396: spanned} by another, $\Theta$, if for every expression occurrence
2397: $A^{\mu}_X$ in $\Pi$ and every non-empty prefix $\nu$ of $\mu$
2398: there is an occurrence of the carrier of $\nu$ in $\Theta$. It is
2399: easy to see there is a minimal set $\Theta$ that spans $\Pi$ and
2400: that such $\Theta$ spans itself. A sequent $\Pi; \Gamma \proves
2401: \Delta; \Theta$ is \emph{spanned} if $\Pi$ is spanned by $\Theta$,
2402: $\Gamma$ is spanned by $\Theta$, $\Delta$ is spanned by $\Theta$
2403: and $\Theta$ is spanned by $\Theta$. A derivation or block is
2404: \emph{spanned} if every sequent in it is spanned.
2405: \end{definition}
2406: %
2407: \begin{definition}[Simple]
2408: A multiset $\Psi$ is \emph{simple} if no expression occurs multiple
2409: times in $\Psi$; a sequent of the form $\Pi; \Gamma \proves \Delta;
2410: \Theta$ is \emph{simple} if $\Pi$ and $\Theta$ are simple. A derivation
2411: or block is \emph{simple} iff every sequent in it is simple.
2412: \end{definition}
2413: %
2414: \begin{definition}[Balanced]
2415: A pair of multisets of tracked, prefixed formulas $\Pi, \Theta$
2416: is \emph{balanced} if
2417: %
2418: \begin{itemize}
2419: \item
2420: for any $\eta = \eta^u_{B\bimp_i C}(\mu,X)$, $\eta$ occurs in
2421: $\Theta$ exactly when the expression $B^{\mu\eta}_{X,\mu\eta}$
2422: occurs in $\Pi$ and exactly when the expression
2423: $C^{\mu\eta}_{X,\mu\eta}$ occurs in $\Theta$; and
2424: \item
2425: for any $\eta = \eta^u_{\Box A}(\mu,X)$, $\eta$ occurs in
2426: $\Theta$ exactly when the expression $A^{\mu}_{X,\mu\eta}$ occurs
2427: in $\Theta$.
2428: %
2429: \end{itemize}
2430: A sequent $\Pi; \Gamma \proves \Delta; \Theta$ is
2431: \emph{balanced} if the pair $\Pi, \Theta$ is balanced. A block or
2432: derivation is \emph{balanced} if every sequent in the block is
2433: balanced.
2434: \end{definition}
2435:
2436: We use the notion of an \emph{isolated block} to obtain an
2437: even stronger characterization of proof search that proceeds in a
2438: well-regimented way. In an isolated block, the only expressions
2439: preserved across a blocking inference are those that are in some
2440: sense intrinsic to the restart problem created by that inference.
2441: Specifically, each nested block must begin with the same
2442: end-sequent as the outer block, except for additional program
2443: statements that have to be added in order to introduce the
2444: newly-assumed disjunct, and the further goal and program statements
2445: required to obtain a balanced and spanned sequent.
2446: %
2447: \begin{definition}[Isolated]
2448: Let ${\cal D}$ be an SCLU derivation, and let ${\cal B}$ be a
2449: block of ${\cal D}$. Write the end-sequent of ${\cal B}$ as $\Pi;
2450: \Gamma \proves \Delta; \Theta$ and consider the right subproof of
2451: some $(\vee\proveslabel^B)$ inference $L$ at the boundary of ${\cal
2452: B}$ has an end-sequent of the form $\Pi', E; \proves ; \Theta'$.
2453: The \emph{exported} expressions in $\Pi'$, $\Pi'_e$, consist of the
2454: occurrences of expressions $F$ in $\Pi'$ such that either is $F$
2455: based in an occurrence of $F$ in $\Pi$ or is based in an occurrence
2456: of $F$ as the side expression of an inference in which $E$ is also
2457: based.
2458:
2459: ${\cal B}$ is \emph{isolated} if the right subproof of each
2460: $(\vee\proveslabel^B)$ inference $L$ at the boundary of ${\cal B}$
2461: has an end-sequent of the form $\Pi', E; \proves ; \Theta'$ meeting
2462: the following conditions: $E$ is the side-expression of $L$;
2463: $\Theta'$ is the minimal multiset of expressions which spans
2464: $\Pi'_e, E, \Theta$ and includes $\Theta$; and $\Pi'$ is the
2465: smallest multiset including $\Pi'_e, E$ for which $\Pi', \Theta'$
2466: is balanced. ${\cal D}$ is \emph{isolated} iff every block of
2467: ${\cal D}$ is isolated.
2468: \end{definition}
2469: %
2470: Isolation allows us to keep close tabs on the uses of formulas
2471: within blocks, which is important for establishing modularity later. In
2472: particular, isolation provides a key notion in formalizing the obvious
2473: fact that an inference that makes no contribution to an SCLU derivation
2474: can be omitted.
2475:
2476: Finally at this stage, we refine the form of proofs which we
2477: are willing to count as goal-directed. Now it will often happen
2478: that, while each block of a derivation may be eager, the derivation
2479: as a whole will not be eager. As observed in
2480: \cite{nadathur/loveland:disj}, derivations with blocks can
2481: nevertheless be seen as eager throughout by reconstructing the
2482: (restart) rule as backchaining against the negation of a subgoal.
2483: But we will simply consider \emph{blockwise eager} derivations from
2484: now on.
2485: %
2486: \begin{definition}[Blockwise delayed]
2487: \m R is \emph{blockwise delayed} exactly when there is a tree
2488: of contiguous inferences ${\cal D}'$ within a single block of
2489: ${\cal D}$ where: ${\cal D}'$ contains R; ${\cal D}'$ has a left
2490: inference $L$ at the root; and the principal $E$ of $R$ is based in
2491: an occurrence of $E$ in the end-sequent of ${\cal D}'$.
2492: \end{definition}
2493: %
2494: \begin{definition}[Blockwise eager]
2495: {\cal D} is {\em blockwise eager} exactly when it contains no
2496: blockwise delayed applications of right rules.
2497: \end{definition}
2498:
2499: Obviously, we can use weakening to transform an SCLB or SCLU
2500: derivation into a SCLS derivation, so the blocking inference
2501: figures are sound. The completeness of SCLB is a consequence of
2502: Lemma~\ref{block-lemma}.
2503: %
2504: \begin{lemma} \label{block-lemma}
2505: We are given a blockwise eager SCLS derivation ${\cal D}$ whose
2506: end-sequent is spanned and balanced and takes the form:
2507: \[
2508: \Pi ; \proves ; \Theta
2509: \]
2510: We transform ${\cal D}$ into a blockwise eager SCLB derivation
2511: in which every block is canceled, linked, isolated, simple,
2512: balanced and spanned.
2513: \end{lemma}
2514: %
2515: \textbf{Proof.} We can transform individual blocks to achieve
2516: a streamlined form, which already implicitly reflects the logic
2517: programming search strategy of focused search on particular goals
2518: and program statements. By pursuing a suitable ordering strategy
2519: as we inductively repeat this inductive transformation, we can
2520: create the desired SCLB proofs with an overall modular block
2521: structure. See Appendix~\ref{block-proof-subsec}. $\qed$
2522:
2523: \subsection{Modularity}
2524: \label{modularity-subsec}
2525:
2526: We now derive SCLP from SCLB. SCLP proofs can be rewritten to
2527: SCLB rules by a weakening transformation. Conversely, rewriting
2528: SCLB proofs to SCLP proofs is accomplished by induction on the
2529: structure of proofs. The transformation is possible because
2530: multiple formulas in sequents are needed only for passing
2531: ambiguities and work done across branches in the search; this is
2532: ruled out by the use of $(\vee\proveslabel^{\s B}_{\s L})$,
2533: $(\vee\proveslabel^{\s B}_{\s R})$ and $(\imp\proveslabel^{\s S})$.
2534: %
2535: \begin{lemma} \label{lp-seq-lemma}
2536: Given a blockwise eager SCLB derivation ${\cal D}$, with
2537: end-sequent
2538: \[
2539: \Pi; \proves ;\Theta
2540: \]
2541: in which every block is linked, simple and spanned, we
2542: can construct a corresponding SCLP derivation of the same
2543: end-sequent in which every block remains linked.
2544: \end{lemma}
2545: %
2546: \textbf{Proof.} By induction on the structure of proofs. See
2547: Appendix~\ref{modularity-proof-subsec}. $\qed$
2548:
2549: \section{Assessment and conclusions}
2550: \label{assessment-sec}
2551:
2552: To execute modal specifications requires leveraging both the
2553: flexibility of efficient classical theorem-proving and the
2554: distinctive modularity of modal logic. This is a significant
2555: problem because the two are at odds. On the one hand, flexible
2556: search strategies impose no constraints on the relationships among
2557: inferences. By ignoring modularity, they can leave open
2558: inappropriate possibilities for search. On the other hand,
2559: brute-force modular systems may place such strong constraints on
2560: the order in which search must proceed that it becomes impossible
2561: to guide that search in a predictable, goal-directed way. In this
2562: paper, we have explored one strategy for balancing the flexibility
2563: of classical goal-directed search with the modularity of modal
2564: logic. This strategy culminates in the development of a modular
2565: logic programming sequent calculus SCLP.
2566:
2567: \cite{my-thesis} describes a preliminary implementation of
2568: proof search in SCLP as a logic programming interpreter \dialup. I
2569: close by summarizing \emph{how}
2570: (Section~\ref{implementation-subsec}) and no less importantly
2571: \emph{why} (Section~\ref{use-subsec}) I developed this
2572: implementation.
2573:
2574: \subsection{Implementation}
2575: \label{implementation-subsec}
2576:
2577: An effective implementation of SCLP requires further
2578: treatments of \emph{unification} and \emph{search control}.
2579:
2580: In general, to implement first-order sequent calculus proof
2581: search, we must \emph{lift} the inference figures. That is, we
2582: adapt the inferences that require instantiation to specific terms so
2583: that they introduce \emph{logic variables} instead. As we
2584: construct the proof, we accumulate \emph{constraints} on the values
2585: of these variables---for example, we get constraints when an axiom
2586: link in the proof requires two formulas to be identical. In the
2587: lifted system, each proof we find represents the set of ground
2588: proofs that you get by replacing the variables with values that
2589: satisfy the constraints. Lifting is the essence of the resolution
2590: procedure \cite{robinson:resolution} but can be regarded as a
2591: general metatheoretical strategy.
2592: \cite{lincoln/shankar:search,voronkov:constraint} offer
2593: particularly general discussions of this strategy at its most
2594: sophisticated.
2595:
2596: For first-order modal inference in prefixed calculi, lifting
2597: introduces two kinds of logic variables, and two corresponding
2598: kinds of constraints. First-order quantifiers introduce logic
2599: variables over individuals, subject to the familiar constraints
2600: that give rise to term unification problems. Modal inferences,
2601: meanwhile, introduce logic variables over prefixes, subject to path
2602: equations. This leads to specialized problems of equational
2603: unification; good solutions are known for the general setting of
2604: multi-modal logic; see for example
2605: \cite{auffray:equations,debart:modal/lp,otten/kreitz,schmidt:uni}.
2606:
2607: The logical fragment of SCLP makes path equations particularly
2608: simple. Inspection of the SCLP proof rules shows that, at any
2609: point in proof search, we have enough path constraints to determine
2610: \emph{ground} substitutions for all the path variables in the
2611: sequent except possibly for variables in the current program
2612: statement that are about to be unified with a goal. In many cases,
2613: this makes path equations easy to solve---a compact representation
2614: of all possible solutions can be computed in polynomial time. The
2615: details are beyond the scope of this paper, but see
2616: \cite{my-thesis}.
2617:
2618: Search control is the other issue. An implementation has to
2619: make commitments about what statements to try and what rules to use
2620: to process those statements. The fact that SCLP program and goal
2621: statements are labeled with ground prefixes means that we can
2622: easily test that a statement's label is a prefix of the goal label
2623: before attempting to match the statement and the goal. We can also
2624: identify an atomic subformula of the statement nondeterministically
2625: as the \emph{head}, and commit to match that head with the goal.
2626: Before doing so, we can for example test that the head and the goal
2627: share the same predicate symbol.
2628:
2629: In the case of disjunction, we also want to make sure that we
2630: avoid reporting duplicate proofs, despite the duplicate rules for
2631: disjunction that we have. Loveland considers a number of
2632: heuristics for this \cite{loveland:nhp}, and we expect that they
2633: apply in SCLP as well as in Near-Horn Prolog. But here is another
2634: heuristic. As motivated in Section~\ref{intro-example-sec},
2635: $(\vee\proveslabel_R)$ is required only for cancellation. When we
2636: use it, we expect to cancel an assumption (like $B$ in
2637: Figure~\ref{explicit-modular-fig}) that could not be canceled
2638: otherwise. We can make this precise: $(\vee\proveslabel_R)$ should
2639: only be used in a restart block, and the assumption that is
2640: canceled in that block ought not to be used in the subsequent
2641: restart block initiated by the $(\vee\proveslabel_R)$ inference.
2642: Otherwise, we will independently construct an alternative proof
2643: that uses $(\vee\proveslabel_L)$ instead. Naturally, the kind of
2644: block analysis illustrated in the proof of
2645: Theorem~\ref{lp-sequent-thrm} can be used to show that this
2646: restriction is complete.
2647:
2648: \subsection{Applications in modal representation}
2649: \label{use-subsec}
2650:
2651: In classical logic, indefinite information is a bit exotic.
2652: Rather than developing an indefinite specification, we much prefer
2653: to collect the additional information required to describe the
2654: world in a precise, definite way. This is not true at all with
2655: modal specifications. Modal specifications get much of their
2656: interest from their ability to contrast different perspectives or
2657: sources of information. What one source of information represents
2658: with specific, definite information, another source represents with
2659: abstract, indefinite information. Computation from modal
2660: specifications involves the coordinated exchange of information
2661: between these sources.
2662:
2663: In particular, problems of \emph{planning} \cite{aaai98} and
2664: problems of \emph{communication} \cite{jlac00} depend on indefinite
2665: modal specifications. In planning, one agent, the
2666: \emph{scheduler}, has to allocate a task to another agent, the
2667: \emph{executive}. (The executive may just be the scheduler at a
2668: later point in time!) It is unrealistic to expect that the
2669: scheduler will know \emph{exactly} what the executive \emph{will}
2670: do; this almost certainly requires information that is not
2671: available to the scheduler. Rather, the scheduler should merely
2672: know what the executive \emph{can} do. This means that, to be
2673: useful, the scheduler must have an \emph{indefinite} modal
2674: specification that abstractly describes the information that will
2675: be available to the executive. For examples, see
2676: \cite{moore:action,morgenstern:preconditions,scherl/levesque:knowledge,davis:preconditions}
2677: as well as \cite{aaai98}.
2678:
2679: In communication, the task of one agent, the \emph{speaker},
2680: is to formulate an utterance that allows another agent, the
2681: \emph{hearer}, to answer a question. There are many cases where
2682: the speaker does not have enough information to answer the question
2683: directly. However, the speaker can still design an utterance that
2684: allows the hearer to infer the right answer, because the hearer
2685: knows something the speaker does not. Concretely, a user of a
2686: computer interface might want to know what action to take next.
2687: The right answer might be for the user to type \emph{jdoe} into a
2688: certain text box. The speaker might know to say \emph{enter your
2689: user ID}, even if the speaker does not know what the user ID is.
2690: Again, the speaker can make such choices meaningfully only from an
2691: indefinite modal specification that says what the hearer knows
2692: abstractly but not definitely. See \cite{jlac00} for a worked-out
2693: formal case study.
2694:
2695: \appendix
2696:
2697: \section{Proof of Theorem~\ref{eager-thrm}}
2698: \label{eager-proof-sec}
2699:
2700: \noindent
2701: \emph{ Any SCL(I) derivation ${\cal D}$ is equal to an eager
2702: derivation ${\cal D}'$ up to permutations of inferences.}
2703:
2704: The proof depends on a generalization of delayed inferences,
2705: which we can term \emph{misplaced} inferences since we intend to
2706: eliminate them. We assume an overall derivation ${\cal D}$, and
2707: consider a right inference \m R that applies to principal $E$ within
2708: some subderivation ${\cal D}'$ of ${\cal D}$.
2709: %
2710: \begin{definition} \label{misplace-def}
2711: We say a right inference $R$ is \emph{right-based} on an
2712: inference $R'$ in ${\cal D}$ if $R = R'$ or $R$ is based on $R'$
2713: and every inference on which $R$ is based above and including $R'$
2714: is a right inference. Then \m R is {\em misplaced} in ${\cal D}'$
2715: exactly when there are inferences $M$ and $R'$ in ${\cal D}'$ such
2716: that, in ${\cal D}$, $M$ is based on an inference $L$, $R$ is
2717: right-based on $R'$, and $R'$ is delayed with respect to $L$.
2718: \end{definition}
2719: %
2720: In this case we will also say $R$ is misplaced \emph{with
2721: respect to} $M$. We can abstract a key case of misplaced
2722: inferences by the following schematic derivation:
2723: \[
2724: \begin{derive}{}
2725: \derivitem{$R$}{}
2726: \derivitem{$M$}{
2727: \makebox[0in][r]{\parbox{2in}{\begin{singlespace}
2728: Right inferences and inferences $R$ not based in
2729: \end{singlespace}}}
2730: \left\{
2731: \makebox[1in][c]{$\vdots$}
2732: \right.
2733: }
2734: \derivitem{$R'$}{
2735: \makebox[0in][r]{\parbox{2in}{
2736: \begin{singlespace}$R'$ delayed wrt $L$ \\ ($M$ based in $L$)
2737: \end{singlespace}}}
2738: \left\{
2739: \makebox[1in][c]{$\begin{array}{c}\ldots E \ldots \\
2740: \downarrow
2741: \end{array}$} \right.}
2742: \derivitem{$L$}{
2743: \ldots E \ldots
2744: }
2745: \end{derive}
2746: \]
2747: %
2748: This schematic derivation shows informally how \emph{misplaced
2749: inferences} help provide an inductive characterization of the
2750: inferences that stand in the way of obtaining an eager derivation.
2751: In an eager derivation, it will be impossible for $R$ to appear
2752: above $L$. For $R'$ cannot be delayed with respect to $L$, but
2753: once $R'$ and $L$ are interchanged, we will obtain a new delayed
2754: inference that $R$ is based in, until finally we must interchange
2755: $L$ and $R$. Of course, to do this, we must first interchange $R$
2756: with the \emph{misplaced} inferences, such as $M$, which stand
2757: between $R$ and $L$ and cannot themselves be interchanged with $L$
2758: because they are based in $L$.
2759:
2760: Observe that the relation $R$ is misplaced with respect to $M$
2761: is asymmetrical. To see this, suppose $R$ is misplaced with
2762: respect to $M$. By definition, $R$ is right-based on $R'$ which is
2763: delayed with respect to a left inference $L$ on which $M$ is based.
2764: Meanwhile, for $M$ to be misplaced with respect to $R$, by
2765: definition, we must have $M$ right-based on $M'$ and $R$ based in
2766: some left rule $L_R$. Any such $M'$ would have to be based in $L$
2767: since no left inferences intervene between $M$ and $M'$; $M'$ must
2768: thus appear \emph{inside} a schematic like that above. At the same
2769: time, since no left inferences intervene between $R$ and $R'$, $R'$
2770: would have to be based in any such $L_R$, which must thus appear
2771: \emph{outside} such a schematic, closer to the root of the overall
2772: derivation. Accordingly, any such $L_R$ must occur closer to the
2773: root of ${\cal D}$ than $L$; meanwhile the principal of $M'$ is
2774: introduced further from the root than $L$. So we will not have
2775: $M'$ delayed with respect to $L_R$.
2776:
2777: Call $R$ \emph{badly misplaced} in ${\cal D}'$ if $R$ is
2778: misplaced with respect to $M$ and $M$ occurs closer to the root
2779: than $R$. A subderivation ${\cal D}'$ with no badly misplaced
2780: inferences will be called \emph{good}. An overall good
2781: derivation is also eager, since any delayed inference is badly
2782: misplaced.
2783:
2784: We can now present the proof in full using a lemma.
2785: %
2786: \begin{lemma}
2787: \label{lp-local-eager-lemma}
2788: Consider a subderivation ${\cal D}'$ of an overall derivation
2789: ${\cal D}$, with the property that ${\cal D}'$ has good immediate
2790: subderivations and that ${\cal D}'$ ends in inference $M$.
2791: From ${\cal D}'$ we can construct a derivation with the same
2792: end-sequent that is good.
2793: \end{lemma}
2794: %
2795: {\bf Proof.} The assumption that the immediate subderivations
2796: of ${\cal D}'$ are good is a very powerful one. For suppose that
2797: some inference is badly misplaced with respect to some other in
2798: ${\cal D}'$. Then we can only have some rule $R$ badly misplaced
2799: with respect to $M$---anything else would contradict that
2800: assumption.
2801:
2802: In fact, we can show that some such $R$ must be adjacent to
2803: $M$. Consider an inference $S$ that intervenes between $R$ and
2804: $M$: we will show that $S$ must be badly misplaced with respect to
2805: $M$ too. By the definition of misplaced, $M$ is based on some left
2806: rule $L$ in ${\cal D}$, $R$ is right-based on $R'$, and $R'$ is
2807: delayed with respect to $L$. Now consider the inferences that $S$
2808: is based on above $L$. If any of these is a left inference $L'$,
2809: or $S$ is itself a left inference, then $R$ is also misplaced with
2810: respect to $S$---indeed, badly misplaced. This contradicts the
2811: assumption that the subderivations of ${\cal D}'$ are good. So
2812: none of these inferences can be a left inference, which means $S$
2813: is a right inference that is right-based on some inference $S'$
2814: above $L$. $S'$ must be delayed with respect to $L$. Hence $S$ is
2815: badly misplaced with respect to $M$.
2816:
2817: Now we can proceed after \cite[Lemma 10]{kleene:permute}.
2818: Define the \emph{grade} of ${\cal D}'$ as the number of badly
2819: misplaced inferences in ${\cal D}'$. We show by induction on the
2820: grade that ${\cal D}'$ can be transformed to a good one.
2821:
2822: The base case is a derivation of grade 0. This case has ${\cal
2823: D}'$ itself good. Thus, suppose the lemma holds for derivations of
2824: grade \m g, and consider ${\cal D}'$ of grade $\m g+1$. By the
2825: argument just given, one immediate subderivation---call it ${\cal
2826: D}''$---must end with an inference $\m R$ which is badly misplaced
2827: with respect to $M$. Such an $R$ of course cannot be based in $M$,
2828: so we interchange inferences $R$ and $M$. In the result, the
2829: subderivation(s) ending in $M$ satisfy the condition of the lemma
2830: with grade \m g or less. By applying the induction hypothesis, we
2831: can replace these subderivations with good ones. By asymmetry, $M$
2832: is not now badly misplaced with respect to $R$, nor can any of the
2833: other inferences be badly misplaced with respect to $R$, since they
2834: were not so in the original derivation. It follows that the result
2835: is a good derivation. $\qed$
2836:
2837: Now, continuing the proof of Theorem~\ref{eager-thrm}, define
2838: the \emph{reluctance} of ${\cal D}$ to be the number of rule
2839: applications \m R such that the subderivation ${\cal D}_R$ of
2840: ${\cal D}$ rooted in $R$ is not good. We proceed by induction on
2841: reluctance. If reluctance is zero, ${\cal D}$ is itself good.
2842:
2843: Now suppose the theorem holds for derivations of reluctance \m
2844: d, and consider ${\cal D}$ of reluctance $\m d+1$. Since ${\cal
2845: D}$ is finite, there must be a highest inference $R$ such that some
2846: inference is badly misplaced with respect to $R$ in the
2847: subderivation ${\cal D}_R$ rooted at $R$. This ${\cal D}_{\s R}$
2848: satisfies the condition of Lemma~\ref{lp-local-eager-lemma}.
2849: Therefore this ${\cal D}_{\s R}$ can be replaced with a
2850: corresponding eager derivation, giving a new derivation of smaller
2851: reluctance. The induction hypothesis then shows that the resulting
2852: derivation can be made eager. $\qed$
2853:
2854: \section{Proof of Theorem~\ref{lp-sequent-thrm}}
2855: \label{lp-proof-sec}
2856:
2857: \emph{Let $\Gamma$ and $\Delta$ be multisets of tracked
2858: prefixed expressions in which each formula is tracked by the empty
2859: set and prefixed by the empty prefix. There is a proof of $\Gamma
2860: \proves \Delta$ in SCL exactly when there is a proof of $\Gamma;
2861: \proves ;\Delta$ in SCLP in which every block is canceled.}
2862:
2863: \textbf{Proof.} As observed already in
2864: Section~\ref{uniform-proof-subsec}, there is an SCL proof of
2865: $\Gamma \proves \Delta$ exactly when there is an SCLI proof of
2866: $\Gamma \proves \Delta$. By Theorem~\ref{eager-thrm} of
2867: Section~\ref{uniform-proof-subsec}, there is an SCLI proof of
2868: $\Gamma \proves \Delta$ exactly when there is an \emph{eager} SCLI
2869: proof of $\Gamma \proves \Delta$. By
2870: Lemma~\ref{articulation-lemma}, there is an eager SCLI proof of
2871: $\Gamma \proves \Delta$ exactly when there is an eager articulated
2872: SCLI proof of $\Gamma; \proves ;\Delta$. And by
2873: Lemma~\ref{segment-lemma}, there is an eager articulated SCLI proof
2874: of $\Gamma; \proves ;\Delta$ exactly when there is an eager SCLS
2875: proof of $\Gamma; \proves ;\Delta$.
2876:
2877: Continuing through the argument, By the Contraction Lemma, we
2878: may assume without loss of generality that $\Gamma; \proves
2879: ;\Delta$ is a simple sequent. We know from its lack of prefixes
2880: that the sequent $\Gamma; \proves; \Delta$ is also spanned and
2881: balanced. By Lemma~\ref{block-lemma} of
2882: Section~\ref{block-proper-subsubsec}, then, there is an eager SCLS
2883: proof of $\Gamma; \proves ;\Delta$ exactly when there is a
2884: blockwise eager SCLB derivation of $\Gamma; \proves ;\Delta$ in
2885: which every block is canceled, linked, isolated, simple, balanced
2886: and spanned. And by Lemma~\ref{lp-seq-lemma}, there is a blockwise
2887: eager SCLB derivation of $\Gamma; \proves ;\Delta$ in which every
2888: block is canceled, linked, isolated, simple, balanced and spanned
2889: exactly when there is an SCLP derivation of $\Gamma; \proves
2890: ;\Delta$ in which every inference is linked. And if every
2891: inference is linked, every block is canceled. $\qed$
2892:
2893: \subsection{Proof of Lemma~\ref{segment-lemma}}
2894: \label{segment-proof-subsec}
2895:
2896: We show in this section that an articulated SCLI proof with
2897: end-sequent $\Pi; \proves ;\Theta$ corresponds to an SCLS proof
2898: with end-sequent $\Pi; \proves ;\Theta$, and vice versa. In fact,
2899: to transform SCLS to articulated SCLI we have a simple structural
2900: induction which replaces $(\imp\proveslabel^S)$ with
2901: $(\imp\proveslabel)$ using the weakening lemma; the soundness of
2902: SCLS over SCLI then follows by Lemma~\ref{articulation-lemma}.
2903: Thus, here we are primarily concerned with completeness of a new
2904: sequent inference figure.
2905:
2906: The use of $(\imp\proveslabel^S)$ in eager derivations ensures
2907: that the processing of each new goal refers directly to global
2908: program statements. To formalize this idea, we introduce the
2909: notion of a \emph{fresh} inference.
2910: %
2911: \begin{definition}[Fresh]
2912: Let ${\cal D}$ be an SCLV derivation. An inference $R$ in
2913: ${\cal D}$ is \emph{fresh} exactly when $R$ is a right inference
2914: and the path from $R$ to the root never follows the left spur of
2915: any $(\imp\proveslabel)$ inference.
2916: \end{definition}
2917: %
2918: \begin{lemma}
2919: \label{new-imp-ncxt-lemma}
2920: Let ${\cal D}$ be an eager SCLV derivation with an end-sequent of
2921: the form
2922: \[
2923: \Pi ; \proveslabel \Delta ; \Theta
2924: \]
2925: and consider a subderivation ${\cal D}'$ of ${\cal D}$ rooted
2926: in a fresh inference \m R. Then the end-sequent of ${\cal
2927: D}'$ also has the form
2928: \[
2929: \Pi' ; \proveslabel \Delta' ; \Theta'
2930: \]
2931: for some $\Pi'$, $\Delta'$ and $\Theta'$.
2932: \end{lemma}
2933: %
2934: {\bf Proof.} Suppose otherwise, and consider a maximal ${\cal
2935: D}'$ whose end-sequent contains a non-empty multiset of local
2936: statements $\Gamma$. We can describe ${\cal D}'$ equivalently as
2937: the subderivation of ${\cal D}$ that is rooted in a lowest fresh
2938: inference $R$ when the end-sequent of ${\cal D}$ contains some
2939: local statements. $R$ cannot be the first inference of ${\cal D}$,
2940: so there must be an inference \m S in ${\cal D}$ immediately below
2941: \m R. If \m S is a left rule, then the fact that ${\cal D}$ is
2942: eager leads to a contradiction. $R$ must be based in $S$, or else
2943: $R$ will be delayed. This means $S$ is an implication inference;
2944: but given that $R$ is fresh, \m R must appear along the branch of
2945: $(\imp\proveslabel^S)$ without local statements. Meanwhile, if \m
2946: S is a right rule, it follows from the formulation of the rules
2947: that if the end-sequent of ${\cal D}_{\s R}$ has non-empty local
2948: statements then the end-sequent of ${\cal D}_{\s L}$ must also.
2949: This contradicts the assumption that \m R is first. $\qed$
2950:
2951: Now we proceed with the proof of Lemma~\ref{segment-lemma}.
2952: We assume an eager SCLV derivation ${\cal D}$ with such an
2953: end-sequent; we show that we can transform it into an eager SCLS
2954: derivation ${\cal D}'$ with the same end-sequent. The proof is by
2955: induction on the number of occurrences of $(\imp\proveslabel)$
2956: inferences in ${\cal D}$.
2957:
2958: In the base case, there are no $(\imp\proveslabel)$ inferences
2959: and ${\cal D}'$ is just ${\cal D}$.
2960:
2961: Suppose the claim holds for derivations where
2962: $(\imp\proveslabel)$ is used fewer than $n$ times, and suppose
2963: ${\cal D}$ is a derivation in which $(\imp\proveslabel)$ is used \m
2964: n times. Choose an inference \m L of $(\imp\proveslabel)$ with no
2965: other $(\imp\proveslabel)$ inference closer to the root of ${\cal
2966: D}$; we must rewrite the left subderivation at $L$ to match the
2967: $(\imp\proveslabel^S)$ inference figure. We distinguish a
2968: subderivation ${\cal D}'$ of ${\cal D}$ as a function of $L$ and
2969: draw on the inferences in ${\cal D}'$ to replace this
2970: subderivation---in particular, we identify ${\cal D}'$ as the
2971: largest subderivation of ${\cal D}$ containing $L$ but no right
2972: inferences or segment boundaries below $L$.
2973:
2974: Using Lemma~\ref{new-imp-ncxt-lemma}, we develop a schema of
2975: ${\cal D}'$ thus:
2976: \[
2977: \setlength{\localjunklength}{1.5em}
2978: \deriviitheni{}
2979: {\raisebox{\baselinestretch\localjunklength}{$L$}}
2980: {\begin{array}{c}
2981: {\cal D}^A \\
2982: \Pi; \Gamma, A\imp B^{\mu}_X
2983: \proveslabel A^{\mu}_X, \Delta; \Theta
2984: \end{array}}
2985: {\begin{array}{c}
2986: {\cal D}^B \\
2987: \Pi; \Gamma, A\imp B^{\mu}_X, B^{\mu}_X
2988: \proveslabel \Delta; \Theta
2989: \end{array}}
2990: {{\cal D}^L
2991: \left\{
2992: \centerbox{$\begin{array}{c}
2993: \Pi; \Gamma, A\imp B^{\mu}_X
2994: \proves \Delta; \Theta \\
2995: \vdots \\
2996: \Pi; \proves \Delta; \Theta
2997: \end{array}$}
2998: \right.}
2999: {\mbox{(Segment boundary or right rule)}}
3000: \]
3001: We suppose \m L applies to an expression $\m A \imp \m
3002: B^{\mu}_X$; the left subderivation of $L$, ${\cal D}^A$ adds the
3003: goal $A$; the right, ${\cal D}^B$, uses the assumption $B$. The
3004: subderivation of ${\cal D}'$ from the end-sequent of \m L abstracts
3005: the left inferences performed elsewhere in this segment (and any
3006: subgoals that these inferences trigger). We notate this tree of
3007: inferences ${\cal D}^L$. By Lemma~\ref{new-imp-ncxt-lemma}, ${\cal
3008: D}'$ ends with a sequent of the form $\Pi ; \proves \Delta ;
3009: \Theta$. Because of the form of the intervening rules, we have the
3010: same succedent $\Delta; \Theta$ at $L$, as well as the same global
3011: statements $\Pi$.
3012:
3013: We use ${\cal D}^L$ to construct an eager SCLS derivation
3014: ${\cal A}$ corresponding to ${\cal D}^A$; we will substitute the
3015: result for the left subtree at $L$ to revise $L$ to fit the
3016: $(\imp\proveslabel^S)$ figure. In outline, the derivation we aim
3017: for is an eager SCLS version of:
3018: \[
3019: \derivi{}
3020: {{\cal D}^A}
3021: {{\cal D}^L + A^{\mu}_X}
3022: \]
3023: The problem is that if ${\cal D}^A$ is rooted in a right
3024: inference to $A$, we will not obtain an eager derivation when we
3025: reassemble $L$. The SCLS derivation ${\cal A}$ we use is actually
3026: constructed by recursion on the structure of ${\cal D}^A$, applying
3027: this kind of transformation at appropriate junctures. At each
3028: stage, we call the subderivation of ${\cal D}^A$ we are considering
3029: ${\cal D}'^A$.
3030:
3031: For the base case, this subderivation is an axiom, and we
3032: construct this subderivation as a result. If ${\cal D}'^A$ ends in
3033: a right rule, the construction proceeds inductively by constructing
3034: corresponding subderivations and recombining them by the same right
3035: rule. With a right inference here, the resulting derivation must
3036: be eager since the subderivations are eager.
3037:
3038: If ${\cal D}'^A$ ends in a left inference, the construction is
3039: not inductive. We observe that ${\cal D}'^A$ has an end-sequent of
3040: the form
3041: \[
3042: \Pi, \Pi' ; \proves \Delta, \Delta'; \Theta, \Theta'
3043: \]
3044: (The inventory of expressions can only be expanded, and that
3045: only in certain places, as we follow right inferences to reach
3046: ${\cal D}'^A$.) So we first weaken ${\cal D}^L$ by the needed
3047: additional expressions---$\Pi'$ on the left and $\Delta'$ (locally)
3048: and $\Theta'$ (globally) on the right; then we identify the open
3049: leaf in ${\cal D}^{\s L}$ with ${\cal D}'^A$, obtaining a larger
3050: derivation ${\cal D}_I$ defined as:
3051: \[
3052: \derivi{}
3053: {{\cal D}'^A}
3054: {\Pi' + {\cal D}'^L + A^{\mu}_X + \Delta'; \Theta'}
3055: \]
3056: Any delayed inference in ${\cal D}_I$ would in fact be delayed
3057: in ${\cal D}'^A$, so this is an eager derivation. The result has,
3058: moreover, fewer than $n$ $(\imp\proveslabel)$ inferences, since it
3059: omits at least $L$ from ${\cal D}'$. Then the induction hypothesis
3060: applies to give the needed SCLS derivation ${\cal A}$.
3061:
3062: Given the derivation ${\cal A}$ so constructed, we substitute
3063: ${\cal A}$ for ${\cal D}^A$ in ${\cal D}$. The result ${\cal D}^*$ is
3064: an eager derivation; ${\cal D}^*$ contains an $(\imp\proveslabel^S)$
3065: inference corresponding to $L$ and therefore contains fewer than \m n
3066: uses of $(\imp\proveslabel)$. The induction hypothesis applies to
3067: transform ${\cal D}^{*}$ to the needed overall derivation. $\qed$
3068:
3069: \subsection{Proof of Lemma~\ref{block-lemma}}
3070: \label{block-proof-subsec}
3071:
3072: \subsubsection{Replacing Herbrand terms}
3073: \label{replace-subsubsec}
3074:
3075: To begin, it is convenient to observe that the use of indexed
3076: Herbrand terms allows us to rename Herbrand terms in a proof under
3077: certain conditions.
3078: %
3079: \begin{lemma}[Substitution] \label{renaming-lemma}
3080: Let ${\cal D}$ be an SCLU derivation with end-sequent
3081: \[
3082: \Pi; \proves ; \Theta
3083: \]
3084: in which no Herbrand terms or Herbrand prefixes appear;
3085: consider a spanned simple subderivation ${\cal D}'$ in which a
3086: modal Herbrand function $\eta^u_A$ occurs in some sequent, but does
3087: not occur in the end-sequent. Let $\eta^v_A$ be a Herbrand
3088: function that does not occur in ${\cal D}$. Then we can construct
3089: a proof ${\cal D}^*$ containing corresponding inferences in a
3090: corresponding order to ${\cal D}$ but in which Herbrand terms and
3091: Herbrand prefixes are adjusted so that $\eta^v_A$ is used in place
3092: of $\eta^u_A$ precisely in the subderivation corresponding to
3093: ${\cal D}'$.
3094: \end{lemma}
3095: %
3096: The \textbf{proof} is by induction on the structure of
3097: derivations. A complex substitution may be required, because the
3098: Herbrand calculus may require not only the replacement of
3099: $\eta^u_A$ itself but also the replacement of Herbrand terms that
3100: depend indirectly on $\eta^u_A$. It is convenient to begin by
3101: replacing any first-order Herbrand term not introduced by a
3102: $(\exists\proveslabel)$ or $(\proveslabel\forall)$ inference by a
3103: distinguished constant $c_0$---starting with leaves of the
3104: derivation and working downward. This replacement is to ensure
3105: that each first-order and modal Herbrand term in ${\cal D}$ is
3106: determined from an expression in the end-sequent of ${\cal D}$ by a
3107: finite number of steps of inference. We continue with the
3108: systematic replacement of $\eta^u_A$ and its dependents. In both
3109: cases, the form of ${\cal D}$ ensures that a finite substitution
3110: can systematically rename all these Herbrand terms as required. We
3111: use the fact that each sequent is simple and spanned to extend this
3112: substitution inductively upward. Because each sequent is spanned
3113: the substitution does not need to be extended at
3114: $(\Box\proveslabel)$ inferences; because each sequent is simple the
3115: substitution can be extended freshly at $(\proveslabel\Box)$ and
3116: $(\proveslabel\bimp)$ inferences. Finally, the form of first-order
3117: Herbrand terms ensures that a finite extension of the substitution
3118: suffices for $(\proveslabel\exists)$ and $(\forall\proveslabel)$
3119: inferences. $\qed$.
3120:
3121: \subsubsection{Rectifying blocks}
3122: \label{rect-subsubsec}
3123:
3124: The transformation of individual blocks appeals to the
3125: following definition of \emph{required} elements of proofs.
3126: %
3127: \begin{definition}[Required]
3128: Given a derivation ${\cal D}$ with end-sequent
3129: \[
3130: \Pi; \Gamma \proves \Delta; \Theta
3131: \]
3132: we say that an expression occurrence $E$ in $\Theta$ or $\Pi$
3133: is \emph{required} iff either it is linked or some block in ${\cal
3134: D}$ is adjacent to the root block and has an end-sequent
3135: \[
3136: \Pi'; \proves ; \Theta'
3137: \]
3138: in which $\Pi'$ or $\Theta'$ contains an expression occurrence
3139: based in $E$.
3140: \end{definition}
3141: %
3142: \begin{lemma}[Rectification] \label{linking-lemma}
3143: We are given a blockwise eager SCLU derivation ${\cal D}$ such
3144: that: every block in ${\cal D}$ is canceled and isolated; every block in
3145: ${\cal D}$ other than the root is spanned, linked, balanced and simple;
3146: and the end-sequent of ${\cal D}$ is balanced. We transform ${\cal D}$
3147: to an SCLU derivation ${\cal D}'$ in which every block is canceled,
3148: linked, isolated, balanced and simple and every block other than the
3149: root is spanned. Every block in ${\cal D'}$ other than the root block
3150: is identical to a block of ${\cal D}$; and the inferences in the root
3151: block of ${\cal D}$ correspond to inferences in the same order in ${\cal
3152: D}$ (and so ${\cal D}'$ is blockwise eager). If the end-sequent of
3153: ${\cal D}$ is spanned then ${\cal D}'$ is spanned and isolated.
3154: \end{lemma}
3155: %
3156: \textbf{Proof.} We describe a transformation that establishes the
3157: following inductive property given ${\cal D}$. There are simple
3158: multisets $\Pi_M \subseteq \Pi$ and $\Theta_M \subseteq\Theta$, together
3159: with multisets $\Gamma' \subseteq \Gamma$ and $\Delta' \subseteq \Delta$
3160: such that: any $\Theta'$ that spans $\Pi_M$ includes $\Theta_M$; and for
3161: any simple $\Pi'$ with $\Pi_M \subseteq \Pi' \subseteq \Pi$ and any
3162: simple $\Theta'$ with $\Theta' \subseteq \Theta$ such that $\Pi'$ and
3163: $\Theta'$ are spanned by $\Theta'$ and the pair $\Pi', \Theta'$ is
3164: balanced, there is a ${\cal D}'$ in which every block is canceled,
3165: linked, balanced, balanced and simple, with end-sequent:
3166: \[
3167: \Pi'; \Gamma' \proves \Delta'; \Theta'
3168: \]
3169: In this ${\cal D}'$, each expression in $\Gamma'$ is linked; each
3170: expression in $\Delta'$ is linked; each $\Pi_M$ expression that occurs
3171: in $\Pi'$ is required and each $\Theta_M$ expression that occurs in
3172: $\Theta'$ is linked. Every block in ${\cal D'}$ other than the root
3173: block is identical to a block of ${\cal D}$; and the inferences in the
3174: root block of ${\cal D}$ correspond to inferences in the same order in
3175: ${\cal D}$. Finally, if $\Gamma'$ and $\Delta'$ are spanned by
3176: $\Theta'$ then ${\cal D}'$ is spanned; if ${\cal D}$ is linked then
3177: ${\cal D}'$ contains all the axioms of ${\cal D}$.
3178:
3179: At axioms, for ${\cal D}$ of
3180: \[
3181: \Pi; \Gamma, A^{\mu}_X \proves A^{\mu}_Y, \Delta; \Theta
3182: \]
3183: $\Pi_M$ and $\Theta_M$ are empty, while $\Gamma' = A^{\mu}_X$ and
3184: $\Delta' = A^{\mu}_X$. Assume we are given simple $\Pi'$ from $\Pi$ and
3185: simple $\Theta'$ from $\Theta$ with $\Pi'$ and $\Theta'$ spanned by
3186: $\Theta'$. We construct ${\cal D}'$ of
3187: \[
3188: \Pi'; A^{\mu}_X \proves A^{\mu}_Y; \Theta'
3189: \]
3190: If $A^{\mu}_X$ is spanned by $\Theta'$, this axiom is spanned too;
3191: the remaining conditions are immediate.
3192:
3193: At inferences, consider as a representative case
3194: $(\vee\proveslabel)$. ${\cal D}$ ends:
3195: \[
3196: \derivii{}
3197: {\begin{array}{c}
3198: {\cal D}_1 \\
3199: \Pi; \Gamma, A\vee B^{\mu}_X, A^{\mu}_X \proves
3200: \Delta; \Theta
3201: \end{array}}
3202: {\begin{array}{c}
3203: {\cal D}_2 \\
3204: \Pi; \Gamma, A\vee B^{\mu}_X, B^{\mu}_X \proves
3205: \Delta; \Theta
3206: \end{array}}
3207: {\Pi; \Gamma, A\vee B^{\mu}_X \proves
3208: \Delta; \Theta}
3209: \]
3210: The blocks of ${\cal D}_1$ and ${\cal D}_2$ either contain the root
3211: or are blocks from ${\cal D}$; the Herbrand prefixes in the end-sequents
3212: of ${\cal D}_1$ and ${\cal D}_2$ occur with the same distribution as in
3213: ${\cal D}$. Therefore we can apply the induction hypothesis to get
3214: $\Pi_{M1}$, $\Theta_{M1}$, $\Gamma_1'$ and $\Delta_1'$ for ${\cal D}_1$;
3215: we can apply it to get $\Pi_{M2}$, $\Theta_{M2}$, $\Gamma_2'$ and
3216: $\Delta_2'$ for ${\cal D}_2$. To transform ${\cal D}$ itself, we
3217: perform case analysis on $\Gamma_1'$ and $\Gamma_2'$.
3218:
3219: If $\Gamma_1'$ does not contain an occurrence of $A^{\mu}_X$, then
3220: $\Pi_M = \Pi_{M1}$, $\Theta_M = \Theta_{M1}$, $\Gamma' = \Gamma_1'$ and
3221: $\Delta' = \Delta_1'$; ${\cal D}_1'$ suffices to carry through the
3222: induction hypothesis.
3223:
3224: Similarly, if $\Gamma_2'$ does not contain an occurrence of
3225: $B^{\mu}_X$, then $\Pi_M = \Pi_{M2}$, $\Theta_M = \Theta_{M2}$, $\Gamma'
3226: = \Gamma_2'$ and $\Delta' = \Delta_2'$; ${\cal D}_2'$ suffices to carry
3227: through the induction hypothesis.
3228:
3229: Otherwise, we will set up $\Pi_M = \Pi_{M1} \cup \Pi_{M2}$ and
3230: $\Theta_M = \Theta_{M1} \cup \Theta_{M2}$ (as sets); by the inductive
3231: characterization of $\Pi_{M1}$, $\Pi_{M2}$, $\Theta_{M1}$ and
3232: $\Theta_{M2}$, any $\Theta'$ that spans both $\Pi_{M2}$ and $\Pi_{M2}$
3233: includes both $\Theta_{M1}$ and $\Theta_{M2}$. We also set up $\Gamma'$
3234: as the multiset containing at least one occurrence of $A\vee B^{\mu}_X$
3235: and as many expression occurrences of any expression as either are found
3236: in $\Gamma_1' \backslash A^{\mu}_X$ or are found in $\Gamma_2'
3237: \backslash B^{\mu}_X$; we set up $\Delta'$ as the multiset containing as
3238: many expression occurrences of any expression as are found in either
3239: $\Delta_1'$ or $\Delta_2'$.
3240:
3241: To continue, we now consider simple $\Pi'$ from $\Pi$ and simple
3242: $\Theta'$ from $\Theta$ such that $\Pi_{M1} \subseteq \Pi'$, $\Pi_{M2}
3243: \subseteq \Pi'$, $\Pi'$ and $\Theta'$ are spanned by $\Theta'$, and the
3244: pair $\Pi', \Theta'$ is balanced. We know that $\Theta'$ includes
3245: $\Theta_M$. We can apply the inductive property to transform ${\cal
3246: D}_1$ and ${\cal D}_2$ into derivations with the inductive property:
3247: \[
3248: \begin{array}{c}
3249: {\cal D}_1' \\
3250: \Pi'; \Gamma_1' \proves \Delta_1'; \Theta'
3251: \end{array}
3252: \;\;\;\;\;\;\;
3253: \begin{array}{c}
3254: {\cal D}_2' \\
3255: \Pi'; \Gamma_2' \proves \Delta_2'; \Theta'
3256: \end{array}
3257: \]
3258: We weaken \emph{the lowest block} of ${\cal D}_1'$ on the left
3259: by the expressions in $\Gamma^+$ and not already in $\Gamma'$ and
3260: on the right by the expressions in $\Delta^+$ and not already in
3261: $\Delta'$, giving ${\cal D}_1^+$. We similarly weaken the lowest
3262: block of ${\cal D}_2'$ on the left by the expressions in $\Gamma^+$
3263: and not already in $\Gamma'_2$ and on the right by the expressions
3264: in $\Delta^+$ and not already in $\Delta'_2$, giving ${\cal
3265: D}_2^+$. Only the lowest blocks are affected by the weakening
3266: transformations, so other blocks remain canceled, linked, spanned,
3267: isolated and simple; the lowest block in each case remains
3268: canceled. The lowest blocks also remain linked since no inferences
3269: are added; and they remain simple (and balanced) because no
3270: weakening occurs in the global areas. Construct ${\cal D}'$ as
3271: \[
3272: \derivii{}
3273: {\begin{array}{c}
3274: {\cal D}_1^+ \\
3275: \Pi'; \Gamma^+, A^{\mu}_X \proves \Delta^+; \Theta'
3276: \end{array}}
3277: {\begin{array}{c}
3278: {\cal D}_2^+ \\
3279: \Pi'; \Gamma^+, B^{\mu}_X \proves
3280: \Delta^+; \Theta'
3281: \end{array}}
3282: {\Pi'; \Gamma^+ \proves
3283: \Delta^+; \Theta'}
3284: \]
3285: The end-sequent is simple and balanced so the root block is simple
3286: and balanced; the inference is linked since $A^{\mu}_X$ and $B^{\mu}_X$
3287: are linked in the subderivations, so the root block is linked. The root
3288: block remains canceled as always.
3289:
3290: Any $\Pi_M$ expression is required here because it is required
3291: either in ${\cal D}_1^+$ in virtue of its membership in $\Pi_{M1}$ or in
3292: ${\cal D}_2^+$ in virtue of its membership in $\Pi_{M2}$; likewise any
3293: $\Theta_M$ expression is linked here because it is linked either in
3294: ${\cal D}_1^+$ in virtue of its membership in $\Theta_{M1}$ or in ${\cal
3295: D}_2^+$ in virtue of its membership in $\Theta_{M2}$. Thus, except for
3296: the spanning conditional, we have shown everything we need
3297: of this ${\cal D}'$.
3298:
3299: Finally, then, if $\Gamma'$ and $\Delta'$ is spanned by $\Theta'$,
3300: $\Delta_1'$ and $\Delta_2'$ are spanned by $\Theta'$ and $\Gamma_1'$ and
3301: $\Gamma_2'$ are spanned by $\Theta'$ in the resulting (spanned)
3302: subderivations ${\cal D}_1'$ and ${\cal D}_2'$. This shows that the
3303: end-sequent of ${\cal D}'$ is also spanned, so ${\cal D}'$ itself is
3304: spanned.
3305:
3306: This reasoning is representative of the construction required also
3307: for $(\wedge\proveslabel)$, $(\exists\proveslabel)$,
3308: $(\forall\proveslabel)$, $(\proveslabel\wedge)$, $(\proveslabel\vee)$,
3309: $(\proveslabel\exists)$, $(\proveslabel\forall)$, (decide) and
3310: (restart). It applies also for $(\imp\proveslabel^S)$, with the obvious
3311: caveat that we do not weaken the left subderivation to match local left
3312: expressions, since the form of the $(\imp\proveslabel^S)$ inference
3313: requires there to be none.
3314:
3315: Next we have $(\vee\proveslabel^B)$; we consider the
3316: representative case of $(\vee\proveslabel^B_L)$. ${\cal D}$ ends:
3317: \[
3318: \derivii{}
3319: {\begin{array}{c}
3320: {\cal D}_1 \\
3321: \Pi_0, \Pi; \Gamma, A\vee B^{\mu}_X, A^{\mu}_X \proves
3322: \Delta; \Theta_0, \Theta
3323: \end{array}}
3324: {\begin{array}{c}
3325: {\cal D}_2 \\
3326: \Pi_0, B^{\mu}_X; \proves
3327: \Theta_0
3328: \end{array}}
3329: {\Pi_0, \Pi; \Gamma, A\vee B^{\mu}_X \proves
3330: \Delta; \Theta_0, \Theta}
3331: \]
3332: We treat this specially to respect the block boundary before ${\cal
3333: D}_2$. In particular, we apply the induction hypothesis to ${\cal D}_1$
3334: (as we may since its end-sequent has the same distribution of Herbrand
3335: prefixes as does that of ${\cal D}$), to get $\Pi_{M1}$, $\Theta_{M1}$,
3336: $\Gamma_1'$ and $\Delta_1'$. If $A^{\mu}_X$ does not occur in
3337: $\Gamma_1'$, we let $\Pi_M = \Pi_{M1}$, $\Theta_M = \Theta_{M1}$,
3338: $\Gamma' = \Gamma_1'$ and $\Delta' = \Delta_1'$; any derivation ${\cal
3339: D}_1'$ constructed from appropriate $\Pi'$ and $\Theta'$ suffices to
3340: carry through the induction hypothesis.
3341:
3342: Otherwise, we get $\Pi_M = \Pi_{M1} \cup \Pi_{e0}$ (as a set),
3343: $\Theta_M = \Theta_{M1}$; any $\Theta'$ that spans $\Pi_M$ also
3344: spans $\Pi_{M1}$ and so includes $\Theta_M$. $\Delta' = \Delta_1'$
3345: and $\Gamma'$ contains $\Gamma_1'$ with the occurrence of
3346: $A^{\mu}_X$ removed, together with an occurrence of $A\vee
3347: B^{\mu}_X$ if $\Gamma_1'$ does not already contain such an
3348: expression.
3349:
3350: Assume simple $\Pi'$ with $\Pi_M \subseteq \Pi' \subseteq \Pi$ and
3351: simple $\Theta'$ with $\Theta' \subseteq \Theta$ with $\Pi'$ and
3352: $\Theta'$ spanned by $\Theta'$ and the pair $\Pi', \Theta'$ balanced.
3353: As before, we must have $\Theta_M$ included in $\Theta'$. We therefore
3354: obtain ${\cal D}_1'$ by the inductive property; we then weaken ${\cal
3355: D}_1'$ locally within the lowest block by $A\vee B^{\mu}_X$ on the left
3356: if necessary, to obtain a good derivation ${\cal D}_1^*$.
3357:
3358: The needed ${\cal D}'$ is now constructed as:
3359: \[
3360: \derivii{}
3361: {\begin{array}{c}
3362: {\cal D}_1^* \\
3363: \Pi'; \Gamma', A^{\mu}_X \proves
3364: \Delta' ; \Theta'
3365: \end{array}}
3366: {\begin{array}{c}
3367: {\cal D}_2 \\
3368: \Pi_0, B^{\mu}_X ; \proves
3369: \Theta_0
3370: \end{array}}
3371: {\Pi'; \Gamma' \proves \Delta' ; \Theta'}
3372: \]
3373: We first argue that the construction instantiates the
3374: $(\vee\proveslabel^B_L)$ inference rule. Every Herbrand prefix in
3375: $\Pi_{0e}$ and $B^{\mu}_X$ occurs in $\Pi'$ or $\Gamma'$, so
3376: $\Pi_{0e}$ and $B^{\mu}_X$ are spanned by $\Theta'$. But because
3377: the root block in ${\cal D}$ is isolated, $\Pi_{0e}$ and
3378: $B^{\mu}_X$ are spanned minimally by $\Theta_0$. Thus $\Theta_0
3379: \subseteq \Theta'$. $\Pi_{0e} \subseteq \Pi_M$ by construction; by
3380: isolation $\Pi_0$ is the smallest set such that the pair of $\Pi_0,
3381: \Theta_0$ is balanced. But since $\Pi', \Theta'$ is balanced,
3382: $\Pi_0 \subseteq \Pi'$.
3383:
3384: Now we show that ${\cal D}'$ so constructed has the needed
3385: properties. The end-sequent is simple and balanced so the root block is
3386: simple and balanced. The inference is linked: $A^{\mu}_X$ is linked in
3387: ${\cal D}_1'$ by the induction hypothesis; $B^{\mu}_X$ is linked in
3388: ${\cal D}_2$ because ${\cal D}_2$ begins a new block which by assumption
3389: is canceled. The root block remains canceled as always. Any $\Pi_M$
3390: expression is required here because either a corresponding expression
3391: $\Pi_{0e}$ in the new block at the left subderivation is based on it, or
3392: because it is required in ${\cal D}_1'$. Every $\Theta_M$ is linked
3393: because it is linked in ${\cal D}_1^*$.
3394:
3395: Finally, if $\Gamma'$ and $\Delta'$ are spanned by $\Theta'$, then
3396: $\Delta_1'$ and $\Gamma_1'$ are spanned by $\Theta_1'$. The new
3397: subderivation ${\cal D}_1'$ is therefore spanned by the inductive
3398: property; this ensures that the overall derivation is spanned.
3399:
3400: Next consider $(\Box\proveslabel)$. ${\cal D}$ ends:
3401: \[
3402: \derivi{}
3403: {\begin{array}{c}
3404: {\cal D}_1 \\
3405: \Pi; \Gamma, \Box_i A^{\mu}_X, A^{\mu\nu}_{X,\mu\nu}
3406: \proves \Delta; \Theta
3407: \end{array}}
3408: {\Pi; \Gamma, \Box_i A^{\mu}_X
3409: \proves \Delta; \Theta}
3410: \]
3411: As always, we apply the induction hypothesis to ${\cal D}_1$ (as we
3412: may since the Herbrand prefixes on $\Pi$ and $\Theta$ formulas remain
3413: the same) to obtain $\Pi_{M1}$, $\Theta_{M1}$, $\Gamma_1'$ and
3414: $\Delta_1'$. If $A^{\mu\nu}_{X,\mu\nu}$ does not occur in $\Gamma_1'$,
3415: we let $\Pi_M = \Pi_{M1}$, $\Theta_M = \Theta_{M1}$, $\Gamma' =
3416: \Gamma_1'$ and $\Delta' = \Delta_1'$; any subderivation ${\cal D}_1'$
3417: obtained by the inductive property suffices to witness the inductive
3418: property for ${\cal D}$.
3419:
3420: Otherwise we obtain $\Gamma'$ by extending $\Gamma_1'$ by the
3421: principal expression $\Box_i A^{\mu}_X$ if necessary and
3422: eliminating the side expression $A^{\mu\nu}_{X,\mu\nu}$; $\Pi_M =
3423: \Pi_{M1}$, $\Theta_M = \Theta_{M1}$ and $\Delta' = \Delta_1'$.
3424: (Since these are common to the subderivation, any $\Pi'$ that spans
3425: $\Pi_M$ includes $\Theta_M$.) Now we consider $\Pi'$ with $\Pi_M
3426: \subseteq \Pi' \subseteq \Pi$ and $\Theta'$ with $\Theta' \subseteq
3427: \Theta$, $\Pi'$ and $\Theta'$ spanned by $\Theta'$ and the pair
3428: $\Pi', \Theta'$ balanced. As always, we have $\Theta_M \subseteq
3429: \Theta'$. We obtain ${\cal D}_1'$ using $\Pi'$ and $\Theta'$, and
3430: weaken the lowest block by local formulas; calling the result
3431: ${\cal D}_1^+$, we can produce ${\cal D}'$ by the following
3432: construction:
3433: \[
3434: \derivi{}
3435: {\begin{array}{c}
3436: {\cal D}_1^+ \\
3437: \Pi'; \Gamma', A^{\mu\nu}_{X,\mu\nu}
3438: \proves \Delta'; \Theta'
3439: \end{array}}
3440: {\Pi'; \Gamma'
3441: \proves \Delta'; \Theta'}
3442: \]
3443: Everything is largely as before. The key new reasoning comes
3444: when we assume that $\Gamma'$ and $\Delta'$ are spanned by
3445: $\Theta'$. We must argue that $\Gamma', A^{\mu\nu}_{X,\mu\nu}$ is
3446: in fact spanned by $\Theta'$. Since $A^{\mu\nu}_{X,\mu\nu}$ is
3447: linked in ${\cal D}^+_1$, there must be an axiom in this block
3448: which is based in $A^{\mu\nu}_{X,\mu\nu}$; indeed, since the
3449: expression occurs as a local antecedent, this axiom must occur
3450: within the segment. This axiom must pair expressions prefixed by a
3451: path $\mu'$ where $\mu\nu$ is a prefix of $\mu'$. But because
3452: ${\cal D}'$ remains blockwise eager, no inferences apply to
3453: $\Delta'$ or $\Theta'$ formulas within the segment (nor can they in
3454: this fragment augment the $\Delta'$ or $\Theta'$ formulas within
3455: the segment); therefore some $\Delta'$ expression is associated
3456: with Herbrand prefix $\mu'$. But since $\Delta'$ is spanned by
3457: $\Theta'$, we have that every prefix of $\mu'$ is associated with
3458: some $\Theta'$ expression; so every prefix of $\mu\nu$ is
3459: associated with some $\Theta'$ expression. Thus ${\cal D}_1^+$ is
3460: spanned and in turn ${\cal D}'$ is spanned.
3461:
3462: We have one last representative class of inferences in ${\cal D}$:
3463: $(\proveslabel\Box)$ and $(\proveslabel\bimp)$. We illustrate with the
3464: case where ${\cal D}$ ends in $(\proveslabel\bimp)$:
3465: \[
3466: \derivi{}
3467: {\begin{array}{c}
3468: {\cal D}_1 \\
3469: \Pi, A^{\mu\eta}_{X,\mu\eta}; \Gamma \proves
3470: \Delta, A\bimp_i B^{\mu}_X ;
3471: \Theta, B^{\mu\eta}_{X,\mu\eta}
3472: \end{array}}
3473: {\Pi; \Gamma \proves
3474: \Delta, A\bimp_i B^{\mu}_X;
3475: \Theta}
3476: \]
3477: We begin by applying the induction hypothesis to ${\cal D}_1$ (as
3478: we can, given the symmetric extension of $\Pi$ and $\Theta$ by labeled
3479: expressions). We obtain $\Theta_{M1}$, $\Pi_{M1}$, $\Gamma_1'$ and
3480: $\Delta_1'$; we consider alternative cases in response to $\Theta$ and
3481: $\Theta_{M1}$. First we suppose $B^{\mu\eta}_{X,\mu\eta} \not\in
3482: \Theta$. It follows by our assumption about ${\cal D}$ that
3483: $A^{\mu\eta}_{X,\mu\eta} \not\in \Pi$ either, nor does $\eta$ occur in
3484: $\Theta$. For this case, we start by defining an overall $\Pi_M$ and
3485: $\Theta_M$: $\Theta_M$ is $\Theta_{M1}$ with any occurrence of
3486: $B^{\mu\eta}_{X,\mu\eta}$ eliminated; $\Pi_M$ is $\Pi_{M1}$ with any
3487: occurrence of $A^{\mu\eta}_{X,\mu\eta}$ eliminated. $\Pi_M$ contains no
3488: occurrences of $\mu\eta$, since $\Pi$ does not; thus given the inductive
3489: property of $\Theta_{M1}$ and $\Pi_{M1}$, any $\Theta'$ that spans
3490: $\Pi_M$ spans $\Theta_M$. We define $\Gamma'$ and $\Delta'$ so that
3491: $\Gamma' = \Gamma_1'$ and $\Delta'$ contains $\Delta_1'$ together with
3492: an occurrence of $A\bimp_i B^{\mu}_X$, provided $\Delta_1'$ does not
3493: already contain one and $B^{\mu\eta}_{X,\mu\eta} \in \Theta_{M1}$ or
3494: $A^{\mu\eta}_{X,\mu\eta} \in \Pi_{M1}$. So, assume we are given simple
3495: $\Pi'$ with $\Pi_M \subseteq \Pi' \subseteq \Pi$ and simple $\Theta'$
3496: with $\Theta' \subseteq \Theta$ (and so $\Theta_M \subseteq \Theta'$)
3497: such that $\Pi'$ and $\Theta'$ are spanned by $\Theta'$ and the pair
3498: $\Pi', \Theta'$ is balanced.
3499:
3500: We consider whether $B^{\mu\eta}_{X,\mu\eta} \in \Theta_{M1}$ or
3501: $A^{\mu\eta}_{X,\mu\eta} \in \Pi_{M1}$. If neither, we apply the
3502: induction hypothesis to ${\cal D}_1$ for the case that $\Theta_1'$ is
3503: $\Theta'$ and $\Pi_1'$ is $\Pi'$. The resulting derivation ${\cal
3504: D}_1'$ serves as ${\cal D}'$.
3505:
3506: Otherwise, $B^{\mu\eta}_{X,\mu\eta} \in \Theta_{M1}$ or
3507: $A^{\mu\eta}_{X,\mu\eta} \in \Pi_{M1}$; we apply the inductive property
3508: of ${\cal D}_1$ for the case that $\Theta_1'$ is $\Theta',
3509: B^{\mu\eta}_{X,\mu\eta}$ and $\Pi_1'$ is $\Pi', A^{\mu\eta}_{X,\mu\eta}$
3510: (clearly $\Pi_1'$ and $\Theta_1'$ are spanned by $\Theta_1'$ assuming
3511: $\Pi'$ and $\Theta'$ are spanned by $\Theta'$; the pair $\Pi_1',
3512: \Theta_1'$ is also balanced given its symmetric extension). If
3513: $B^{\mu\eta}_{X,\mu\eta} \in \Theta_{M1}$, by the inductive property it
3514: is linked. If $A^{\mu\eta}_{X,\mu\eta} \in \Pi_{M1}$, it is required,
3515: but we shall show that it is in fact linked. By the definition of being
3516: required, the other possibility is that there is a block adjacent to the
3517: root block of ${\cal D}_1'$ with end-sequent
3518: \[
3519: \Pi'', E; \proves \Theta''
3520: \]
3521: in which the $(\vee\proveslabel^B)$ inference $R$ that bounds the
3522: block is based in $E$ and $\Pi'', E$ or $\Theta''$ contains an
3523: expression occurrence based in $A^{\mu\eta}_{X,\mu\eta}$. But since the
3524: original block is isolated in the original ${\cal D}$, it is $E$ that
3525: must be based in $A^{\mu\eta}_{X,\mu\eta}$. But then $R$ is based in
3526: $A^{\mu\eta}_{X,\mu\eta}$ and $R$ is linked: in particular its side
3527: expression in the left spur) must be linked; so
3528: $A^{\mu\eta}_{X,\mu\eta}$ is linked too.
3529:
3530: Thus we can weaken ${\cal D}_1'$ in its lowest block if necessary
3531: by $A\bimp_i B^{\mu}_{X}$ as a local right formula (in $\Gamma$),
3532: producing ${\cal D}_1^+$; ${\cal D}_1^+$ remains good by the same
3533: argument as the earlier cases. Thus we can construct ${\cal D}'$ as:
3534: \[
3535: \derivi{}
3536: {\begin{array}{c}
3537: {\cal D}_1^+ \\
3538: \Pi', A^{\mu\eta}_{X,\mu\eta} ;
3539: \Gamma' \proves \Delta',
3540: A\bimp_i B^{\mu}_{X};
3541: \Theta', B^{\mu\eta}_{X,\mu\eta}
3542: \end{array}}
3543: {\Pi'; \Gamma' \proves \Delta'; \Theta'}
3544: \]
3545: The end-sequent here is simple and balanced, so the whole root
3546: block is simple and balanced. The new inference is linked (in virtue of
3547: the linked occurrence of one side expression---$A^{\mu\eta}_{X,\mu\eta}$
3548: or $B^{\mu\eta}_{X,\mu\eta}$) so the whole root block is linked. The
3549: root block is of course canceled. Each element of $\Pi_M$ is required
3550: because it is an element of $\Pi_{M1}$ and required in the immediate
3551: subderivation; each element of $\Theta_M$ is linked, because it is an
3552: element of $\Theta_{M1}$ and therefore linked in the immediate
3553: subderivation.
3554:
3555: To conclude the case, suppose the end-sequent of ${\cal D}$ is
3556: spanned and that $\Gamma'$ and $\Delta'$ are spanned by $\Theta'$; it
3557: follows that same property applies to ${\cal D}_1$ so the subderivation
3558: is spanned. Then the end-sequent must also be spanned.
3559:
3560: The alternative case has $B^{\mu\eta}_{X,\mu\eta} \in \Theta$. By
3561: assumption, it also has $A^{\mu\eta}_{X,\mu\eta} \in \Pi$. We therefore
3562: define an overall $\Pi_M$ and $\Theta_M$ directly as $\Pi_{M1}$ and
3563: $\Theta_{M1}$, respectively; similarly $\Gamma' = \Gamma_1'$ and
3564: $\Delta' = \Delta_1'$. To construct the needed ${\cal D}'$ for
3565: appropriate $\Pi'$ and $\Theta'$, we simply apply the induction
3566: hypothesis to ${\cal D}_1$ for the case that $\Theta_1'$ is $\Theta'$
3567: and $\Pi_1'$ is $\Pi'$. The resulting derivation ${\cal D}_1'$
3568: suffices.
3569:
3570: Having completed the induction, we argue that we can obtain an
3571: overall ${\cal D}'$ that is isolated, assuming the original ${\cal D}$
3572: is not only isolated but spanned. Apply the inductive result to ${\cal
3573: D}$ for the case $\Pi' = \Pi$ and $\Theta' = \Theta$; since $\Gamma'
3574: \subseteq \Gamma$ and $\Delta' \subseteq \Delta$ we obtain a spanned
3575: derivation ${\cal D}'$ ending
3576: \[
3577: \Pi; \Gamma' \proves \Delta'; \Theta
3578: \]
3579: Consider the end-sequent of any block other than the root in ${\cal
3580: D}'$; it is
3581: \[
3582: \Pi_0, E ; \proves ; \Theta_0
3583: \]
3584: where a corresponding block occurs in ${\cal D}$. I argue by
3585: contradiction that for any $F \in \Pi_0$ either $F \in \Pi$ or $F$
3586: is based in an occurrence of $F$ as the side expression of an
3587: inference in ${\cal D}'$ in which $E$ is also based. (This will
3588: show that ${\cal D}'$ is isolated.) So consider an exceptional
3589: $F$. Since ${\cal D}$ is isolated, if $F \not\in \Pi$, $F$ is
3590: based in an occurrence of $F$ as the side expression of an
3591: inference in ${\cal D}$ in which $E$ is also based; this inference
3592: introduces some path symbol $\eta$ which occurs in the label of $F$
3593: and $E$. In ${\cal D}'$, $E$ can not be based in such an
3594: inference; otherwise $F$ would also be based in that inference,
3595: since ${\cal D}'$ is simple. (We have assumed that $F$ is not
3596: based in such an inference.) But in this case the expression in
3597: the end-sequent of ${\cal D}'$ on which $E$ is based must contain
3598: $\eta$. Because the end-sequent of ${\cal D}'$ is spanned the form
3599: of $\Pi$ and $\Theta$ is constrained in ${\cal D}$, $F$ must occur
3600: in $\Pi$. This is absurd. $\qed$
3601:
3602: We conclude Section~\ref{rect-subsubsec} by observing some
3603: facts about this construction. First, let ${\cal D}'$ be a
3604: derivation obtained by the construction of
3605: Lemma~\ref{linking-lemma}, and suppose ${\cal D}'$ is weakened (in
3606: a spanned and balanced way) to ${\cal D}''$ by adding occurrences
3607: of global expressions that either already occur in the end-sequent
3608: of ${\cal D}'$ or never occur as global expressions in ${\cal D}'$.
3609: Then a straightforward induction shows that ${\cal D}'$ is obtained
3610: again from ${\cal D}''$ by the construction of
3611: Lemma~\ref{linking-lemma}.
3612:
3613: Second, observe that if ${\cal D}'$ is a derivation obtained
3614: by the construction of Lemma~\ref{linking-lemma}, and ${\cal D}''$
3615: is obtained from ${\cal D}''$ by the renaming of Herbrand prefixes
3616: (as in Lemma~\ref{renaming-lemma}), then straightforward induction
3617: shows that ${\cal D}''$ is obtained again from ${\cal D}''$ by the
3618: construction of Lemma~\ref{linking-lemma}.
3619:
3620: Third, let ${\cal D}'$ be a derivation for which the
3621: construction of Lemma~\ref{linking-lemma} yields itself. Let $\nu$
3622: be a prefix and let the $\Pi; \Theta$ be the smallest balanced pair
3623: where $\Theta$ contains all the carriers of prefixes of $\nu$
3624: introduced in ${\cal D}'$. Suppose each expression in $\Pi$ and
3625: $\Theta$ has the property that at most one inference of ${\cal D}'$
3626: has an occurrence of that expression as a side expression.
3627: Consider a derivation ${\cal D}''$ obtained from ${\cal D}'$ by
3628: weakening globally by $\Pi$ (on the left) and by $\Theta$ (on the
3629: right). Let ${\cal D}^*$ be the result of applying the
3630: construction of Lemma~\ref{linking-lemma} to ${\cal D}''$. Then
3631: ${\cal D}^*$ contains any subderivation of ${\cal D}'$ whose
3632: end-sequent contains $\Pi$ and $\Theta$ as global formulas. Again
3633: this is a straightforward induction; the base case considers a
3634: subderivation of ${\cal D}'$ whose end-sequent contains $\Pi$ and
3635: $\Theta$ as global formulas; in this case we apply the first
3636: observation. Unary inferences extend the claim immediately. At
3637: binary inferences, one subderivation must be unchanged, by the
3638: first observation: since $\Pi$ and $\Theta$ are introduced on a
3639: unique path, each $\Pi$ and $\Theta$ formula never occurs or
3640: already occurs in the end-sequent in that subderivation. Thus the
3641: other subderivation necessarily appears in the derivation obtained
3642: by the construction of Lemma~\ref{linking-lemma}.
3643:
3644: \subsubsection{Block conversion}
3645: \label{block-proper-subsubsec}
3646:
3647: We now have the background required to perform the conversion to
3648: block structure, and complete the proof of Lemma~\ref{block-lemma}.
3649:
3650: \emph{We are given a blockwise eager SCLS derivation ${\cal
3651: D}$ whose end-sequent is spanned and balanced and takes the form:
3652: \[
3653: \Pi ; \proves ; \Theta
3654: \]
3655: We can transform ${\cal D}$ into a blockwise eager SCLB
3656: derivation in which every block is canceled, linked, isolated,
3657: simple, balanced and spanned.}
3658:
3659: \textbf{Proof.} Our induction hypothesis is stronger than the
3660: lemma. We assume a blockwise eager SCLU derivation ${\cal D}$ with
3661: end-sequent of the form
3662: \[
3663: \Pi ; \proves ; \Theta
3664: \]
3665: in which every block is canceled, linked, isolated, simple,
3666: balanced and spanned, such that that the subproof rooted at any
3667: $(\vee\proveslabel)$ inference in ${\cal D}$ is an SCLS derivation. And
3668: we identify a distinguished expression occurrence $E$ in the end-sequent
3669: of ${\cal D}$ which is linked. By Lemma~\ref{linking-lemma}, it is
3670: straightforward to obtain such a derivation from the SCLS derivation
3671: (containing only a single block) that we have assumed. We transform
3672: ${\cal D}$ into a blockwise eager SCLB derivation in which every block
3673: is canceled, linked, isolated, simple, balanced and spanned and in which
3674: $E$ is also linked; we perform induction on the number of
3675: $(\vee\proveslabel)$ inferences in ${\cal D}$.
3676:
3677: In the base case there are no $(\vee\proveslabel)$ inferences,
3678: so ${\cal D}$ itself is an SCLB derivation.
3679:
3680: In the inductive case, we assume ${\cal D}$ with \m n
3681: $(\vee\proveslabel)$ inferences, and assume the hypothesis true for
3682: derivations with fewer. We find an application $L$ of
3683: $(\vee\proveslabel)$ with no other closer to the root of ${\cal
3684: D}$. We will transform ${\cal D}$ to eliminate $L$.
3685:
3686: Let ${\cal D}'$ denote the smallest subderivation of ${\cal D}$
3687: containing the full block of ${\cal D}$ in which $L$ occurs.
3688: Explicitly, ${\cal D}'$ may be ${\cal D}$ itself; otherwise, ${\cal D}'$
3689: is rooted at the right subderivation of the highest
3690: $(\vee\proveslabel^B)$ inference below $L$---an inference we will refer
3691: to as $H$. In either case, our assumptions allow us to identify a
3692: distinguished linked expression $F$ in the end-sequent of ${\cal D}'$:
3693: either the assumed $E$ from ${\cal D}$, or the side expression of the
3694: inference $H$ (assumed canceled). Suppose $A\vee B^{\nu}_Y$ is the
3695: principal of $L$. We can apply Lemma~\ref{renaming-lemma} to rename
3696: $A\vee B^{\nu}_Y$ to $A\vee B^{\mu}_X$ in such a way that each symbol in
3697: $\mu$ that is introduced in ${\cal D}'$ is introduced by a unique
3698: inference there. Now we can infer the following schema for ${\cal D}'$:
3699: %
3700: \[
3701: \begin{array}{c}
3702: \left[
3703: \centerbox{\derivii{$L$}
3704: {\begin{array}{c}
3705: {\cal D}^A \\
3706: \Pi_0, F, \Pi; \Gamma, A\vee B^{\mu}_X, A^{\mu}_X \proves
3707: \Delta ; \Theta_0, \Theta
3708: \end{array}}
3709: {\begin{array}{c}
3710: {\cal D}^B \\
3711: \Pi_0, F, \Pi; \Gamma, A\vee B^{\mu}_X, B^{\mu}_X \proves
3712: \Delta ; \Theta_0, \Theta
3713: \end{array}}
3714: {\Pi_0, F, \Pi; \Gamma, A\vee B^{\mu}_X \proves
3715: \Delta; \Theta_0, \Theta}~~~}
3716: \right] \\
3717: {\cal D}^L \\
3718: \Pi_0, F; \proves ; \Theta_0
3719: \end{array}
3720: \]
3721: %
3722: That is, the subderivation of ${\cal D}'$ below \m L is${\cal
3723: D}^{\s L}$; the right subderivation above \m L (in which \m B is
3724: assumed) is ${\cal D}^{\s B}$; the left is ${\cal D}^A$.
3725:
3726: We will use the inferences from ${\cal D}^L$ to construct
3727: alternative smaller derivations in place of ${\cal D}^A$ and ${\cal
3728: D}^B$. By $\Theta'$, indicate the minimal set of formulas required in
3729: addition to $\Theta_0$ to span $A^{\mu}_X$; by $\Pi'$ indicate the
3730: minimal set of formulas required in addition to $\Pi_0, F$ and
3731: $A^{\mu}_X$ to ensure that the pair given by $\Pi_0, \Pi', F, A^{\mu}_X$
3732: and $\Theta_0, \Theta'$ is balanced. (This is well-defined because the
3733: sequent $\Pi_0, F \proves \Theta_0$ is already spanned and balanced.)
3734: Now we can construct two new subderivations ${\cal D}'^A$ and ${\cal
3735: D}'^B$ given respectively as follows:
3736: \[
3737: \begin{array}{c}
3738: \left[
3739: \centerbox{\derivi{decide}{
3740: \begin{array}{c}
3741: {} \Pi' + A^{\mu}_X + {\cal D}^A + \Theta' \\
3742: \Pi_0, F, \Pi, \Pi', A^{\mu}_X;
3743: \Gamma, A\vee B^{\mu}_X, A^{\mu}_X \proves
3744: \Delta ; \Theta_0, \Theta, \Theta'
3745: \end{array}}
3746: {\Pi_0, F, \Pi, \Pi', A^{\mu}_X;
3747: \Gamma, A\vee B^{\mu}_X \proves
3748: \Delta ; \Theta_0, \Theta, \Theta'}~~~~~~~~~~~~~~~~~}
3749: \right] \\
3750: \Pi' + A^{\mu}_X + {\cal D}^L + \Theta' \\
3751: \Pi_0, F, \Pi', A^{\mu}_X; \proves ;\Theta_0, \Theta'
3752: \end{array}
3753: \]
3754: \[
3755: \begin{array}{c}
3756: \left[
3757: \centerbox{\derivi{decide}{
3758: \begin{array}{c}
3759: {} [ \Pi' + B^{\mu}_X + {\cal D}^B + \Theta' ] \\
3760: \Pi_0, F, \Pi, \Pi', B^{\mu}_X;
3761: \Gamma, B\vee B^{\mu}_X, B^{\mu}_X \proves
3762: \Delta ; \Theta_0, \Theta, \Theta'
3763: \end{array}}
3764: {\Pi_0, F, \Pi, \Pi', B^{\mu}_X;
3765: \Gamma, B\vee B^{\mu}_X \proves
3766: \Delta ; \Theta_0, \Theta, \Theta'}~~~~~~~~~~~~~~~~~}
3767: \right] \\
3768: \Pi' + B^{\mu}_X + {\cal D}^L + \Theta' \\
3769: \Pi_0, F, \Pi', B^{\mu}_X; \proves ;\Theta_0, \Theta'
3770: \end{array}
3771: \]
3772: That is, we weaken ${\cal D}^A$ and ${\cal D}^B$ by global versions
3773: of the side expression of inference $L$ throughout their \emph{lowest
3774: blocks}; we apply a (decide) inference to obtain a new subderivation to
3775: substitute for the subderivation rooted at $L$ in ${\cal D}^L$. We
3776: weaken by sufficient additional formulas globally in the \emph{lowest
3777: blocks} to ensure that the end-sequents of these derivations are
3778: balanced and spanned.
3779:
3780: Since we have changed only the lowest block here, and have
3781: ensured that this block remains isolated and canceled, we can now
3782: apply Lemma~\ref{linking-lemma} to obtain corresponding derivations
3783: ${\cal D}_I^A$ and ${\cal D}_I^B$ in which every block is canceled,
3784: linked, isolated, simple, balanced and spanned. In light of our
3785: first observation about the construction of
3786: Lemma~\ref{linking-lemma}, we can see that the inferences of ${\cal
3787: D}^A$ are preserved up to the new (decide) inference. And in light
3788: of our third observation about the construction of
3789: Lemma~\ref{linking-lemma}, given the unique inferences introducing
3790: $\Theta_0$ and $\Pi_0$, this (decide) inference must be preserved
3791: in ${\cal D}_I^A$. Thus $A^{\mu}_X$ is linked in ${\cal D}_I^A$
3792: and for analogous reasons $B^{\mu}_X$ is linked in ${\cal D}_I^B$.
3793: These derivations satisfy the induction hypothesis as deductions
3794: with fewer than $n$ $(\vee\proveslabel)$ inferences; we can apply
3795: the induction hypothesis with $A^{\mu}_X$ and $B^{\mu}_X$ as the
3796: distinguished linked formulas to preserve. This results in SCLB
3797: derivations ${\cal A}$ and ${\cal B}$ with the same end-sequents as
3798: ${\cal D}'^A$ and ${\cal D}'^B$, in which every block is canceled,
3799: linked, isolated, simple and spanned, and in which respectively
3800: $A^{\mu}_X$ and $B^{\mu}_X$ are linked.
3801:
3802: We need only one of ${\cal A}$ and ${\cal B}$ to reconstruct
3803: ${\cal D}'$ using blocking inferences. For example, we obtain a
3804: proof using $(\vee\proveslabel^B_L)$ by using ${\cal B}$ in place
3805: of ${\cal D}^B$ as schematized below:
3806: \[
3807: \begin{array}{@{}c@{}}
3808: \left[
3809: \centerbox{\derivii{$\vee\proveslabel^B_L$}
3810: {\begin{array}{c}
3811: {\cal D}^A \\
3812: \Pi_0, F, \Pi; \Gamma, A\vee B^{\mu}_X, A^{\mu}_X \proves
3813: \Delta ; \Theta_0, \Theta
3814: \end{array}}
3815: {\begin{array}{c}
3816: {\cal B} \\
3817: \Pi_0, F, \Pi', B^{\mu}_X \proves \Theta_0, \Theta'
3818: \end{array}}
3819: {\Pi_0, F, \Pi; \Gamma, A\vee B^{\mu}_X \proves
3820: \Delta ; \Theta_0, \Theta }~~~~~~~~~~}
3821: \right] \\
3822: {\cal D}^L \\
3823: \Pi_0, F; \proves ; \Theta_0
3824: \end{array}
3825: \]
3826: In a complementary way, we obtain a proof using
3827: $(\vee\proveslabel^B_R)$ by using ${\cal A}$ in place of ${\cal
3828: D}^A$ as schematized below:
3829: \[
3830: \begin{array}{@{}c@{}}
3831: \left[
3832: \centerbox{\derivii{$\vee\proveslabel^B_L$}
3833: {\begin{array}{c}
3834: {\cal D}^B \\
3835: \Pi_0, F, \Pi; \Gamma, A\vee B^{\mu}_X, B^{\mu}_X \proves
3836: \Delta ; \Theta_0, \Theta
3837: \end{array}}
3838: {\begin{array}{c}
3839: {\cal A} \\
3840: \Pi_0, F, \Pi', A^{\mu}_X \proves \Theta_0, \Theta'
3841: \end{array}}
3842: {\Pi_0, F, \Pi; \Gamma, A\vee B^{\mu}_X \proves
3843: \Delta ; \Theta_0, \Theta}~~~~~~~~~~}
3844: \right] \\
3845: {\cal D}^L \\
3846: \Pi_0, F; \proves ;\Theta_0
3847: \end{array}
3848: \]
3849: Note that the root block is isolated in both cases, because we have
3850: added only as many formulas to $\Pi'$ and $\Theta'$ as are necessary to
3851: obtain a balanced, spanned sequent; the remaining expressions originate
3852: in the end-sequent of the previous block, which we know was isolated.
3853: Thus, in both cases, we have blockwise eager derivations in which every
3854: block is canceled, isolated, simple, balanced and spanned, in which
3855: fewer than $n$ $(\vee\proveslabel)$ inferences are used, and in which
3856: only the root block may fail to be linked. We thus need to apply the
3857: construction of Lemma~\ref{linking-lemma} again to ensure that the root
3858: block is linked. It is possible for the distinguished occurrence of $F$
3859: not to be linked in one of the resulting derivations, but not both. To
3860: see this, consider applying the construction of
3861: Lemma~\ref{linking-lemma} to ${\cal D}'$ itself, as a test: the result
3862: will be ${\cal D}'$ since ${\cal D}'$ is linked. Starting from ${\cal
3863: D}^A$ and ${\cal D}^B$ and axioms elsewhere, each inference in ${\cal
3864: D}'$ corresponds to an inference in the alternative derivations
3865: schematized above. We can argue by straightforward induction that no
3866: formula is linked in the reconstructed ${\cal D'}$ unless it is also
3867: linked in the one of the corresponding reconstructed alternative
3868: derivations. And $F$ is linked in ${\cal D}'$.
3869:
3870: Call the derivation in which $F$ is linked ${\cal D}''$; we
3871: substitute ${\cal D}''$ for ${\cal D}'$ in ${\cal D}$. Since $F$
3872: remains linked in ${\cal D}''$, when we do so, we obtain a blockwise
3873: eager SCLU derivation with an appropriate end-sequent, with fewer
3874: original $(\vee\proveslabel)$ inferences, and in which every block
3875: remains canceled, linked, isolated, simple, balanced and spanned, and in
3876: which $(\vee\proveslabel)$ inferences lie at the root of SCLS
3877: derivations. Applying the induction hypothesis to the result gives the
3878: required SCLB derivation. $\qed$
3879:
3880: \subsection{Proof of Lemma~\ref{lp-seq-lemma}}
3881: \label{modularity-proof-subsec}
3882:
3883: \emph{We are given a blockwise eager SCLB derivation ${\cal
3884: D}$, with end-sequent
3885: \[
3886: \Pi;\Gamma \proves \Delta;\Theta
3887: \]
3888: in which every block is linked, simple and spanned. We
3889: construct an SCLP derivation ${\cal D}'$ of which four additional
3890: properties hold:
3891: %
3892: \begin{itemize}
3893: \item
3894: the end-sequent of ${\cal D}'$ takes the form
3895: \[
3896: \Pi;\Gamma' \proves \Delta';\Theta
3897: \]
3898: with $\Gamma' \subseteq \Gamma$ and $\Delta' \subseteq
3899: \Delta$;
3900: \item
3901: ${\cal D}'$ contains in each segment or block all and only the
3902: axioms of the corresponding segment or block of ${\cal D}$;
3903: \item
3904: whenever ${\cal D}'$ contains a sequent of the form
3905: \[
3906: \Pi^*; \Gamma^* \proveslabel \m F ; \Theta^*
3907: \]
3908: $F$ is the only right formula on which an axiom in that block
3909: is based; and
3910: \item
3911: whenever ${\cal D}'$ contains a sequent of the form
3912: \[
3913: \Pi^* ; \m F \proveslabel \Delta^*; \Theta^*
3914: \]
3915: then \m F is the only left formula on which an axiom in that
3916: segment is based.
3917: \end{itemize}}
3918:
3919: In the base case, ${\cal D}$ is
3920: %
3921: \[
3922: {\Pi; \Gamma, \m A^{\mu}_{\s X} \proves
3923: \m B^{\nu}_{\s X}, \Delta; \Theta}
3924: \]
3925: %
3926: and ${\cal D}'$ is
3927: %
3928: \[
3929: {\Pi; \m A^{\mu}_{\s X} \proves \m B^{\nu} ; \Theta}
3930: \]
3931: %
3932: Supposing the claim true for proofs of height \m h, consider a
3933: proof ${\cal D}$ with height \m h+1. We consider cases for the
3934: different rules with which ${\cal D}$ could end.
3935:
3936: The treatment of $(\proveslabel\wedge)$ is representative of
3937: the case analysis for the right rules other than
3938: $(\proveslabel\bimp)$. ${\cal D}$ ends
3939: \[
3940: \derivii{$\proveslabel\wedge$}
3941: {\Pi; \proves A^{\mu}_X, A\wedge B^{\mu}_X, \Delta; \Theta}
3942: {\Pi; \proves B^{\mu}_X, A\wedge B^{\mu}_X, \Delta; \Theta}
3943: {\Pi; \proves A\wedge B^{\mu}_X, \Delta; \Theta}
3944: \]
3945: (It is a consequence of Lemma~\ref{new-imp-ncxt-lemma} that in
3946: the initial derivation there is an empty local area.) We simply
3947: apply the induction hypotheses to the immediate subderivations. If
3948: the resulting derivations end with (restart), consider the
3949: immediate subderivation of the results, otherwise consider the
3950: results themselves. These derivations end
3951: \[
3952: \begin{array}{c}
3953: \Pi; \proves C ; \Theta \\
3954: \Pi; \proves D ; \Theta
3955: \end{array}
3956: \]
3957: We must have \m C = \m A; we know from the structure of ${\cal
3958: D}$ that \m A is linked, and \m A could not be linked in ${\cal D}$
3959: unless $\m C = \m A$ since ${\cal D}'$ shows that all of the axioms
3960: in ${\cal D}$ derive from \m C. For the same reason \m D = \m B.
3961: So we can combine the resulting proofs by an $(\proveslabel\wedge)$
3962: inference to give the needed ${\cal D}'$.
3963:
3964: The case of $(\proveslabel\bimp)$ proceeds similarly, but relies
3965: on an additional observation. ${\cal D}$ ends
3966: \[
3967: \derivi{$\proveslabel\bimp$}
3968: {\begin{array}{c}
3969: {\cal D}_1 \\
3970: \Pi, A^{\mu\eta}_{X,\mu\eta}; \proves
3971: \Delta, A\bimp_i B^{\mu}_X; B^{\mu\eta}_{X,\mu\eta}, \Theta
3972: \end{array}}
3973: {\Pi; \proves
3974: \Delta, A\bimp_i B^{\mu}_X; \Theta}
3975: \]
3976: We apply the induction hypothesis to ${\cal D}_1$ and
3977: eliminate any final (restart) inference. This gives us a
3978: derivation ${\cal D}_1'$ of
3979: \[
3980: \Pi, A^{\mu\eta}_{X,\mu\eta} ; \proves
3981: E ; B^{\mu\eta}_{X,\mu\eta}, \Theta
3982: \]
3983: If we know that the $B$-side expression of this inference is
3984: linked in this block, then we can conclude, as before, that $E$ is
3985: an occurrence of the expression $B^{\mu\eta}_{X,\mu\eta}$. We show
3986: this as follows. We know from the structure of ${\cal D}$ only
3987: that \emph{one} of the $A$-expression and the $B$-expression must
3988: be linked. However, it is straightforward to show that no left
3989: expression $A^{\mu\eta}_{X,\mu\eta}$ is linked in an SCLP
3990: derivation with a local goal $C^{\nu}_Y$ unless $\mu\eta$ is a
3991: prefix of $\nu$. (The argument is a straightforward variant for
3992: example of \cite[Lemma 2]{permute-paper}.) Since ${\cal D}$ is
3993: simple and spanned, $\eta$ must be new;
3994: $B^{\mu\eta}_{X,\mu\eta}$ is the only expression whose associated
3995: path term has $\mu\eta$ as a prefix.
3996:
3997: Thus, we construct ${\cal D}'$ using an SCLP inference as
3998: \[
3999: \derivi{$\proveslabel\bimp$}
4000: {\begin{array}{c}
4001: {\cal D}_1' \\
4002: \Pi, A^{\mu\eta}_{X,\mu\eta} ; \proves
4003: B^{\mu\eta}_{X,\mu\eta} ; B^{\mu\eta}_{X,\mu\eta}, \Theta
4004: \end{array}}
4005: {\Pi; \proves
4006: A\bimp_i B^{\mu}_{X} ; \Theta}
4007: \]
4008:
4009: Now suppose ${\cal D}$ ends in a left rule other than
4010: $(\imp\proveslabel^S)$ or $(\vee\proveslabel^B)$. We take
4011: $(\wedge\proveslabel)$ as a representative case; then ${\cal D}$ is:
4012: %
4013: \[
4014: \derivi{$\wedge\proveslabel$}
4015: {\begin{array}{c}
4016: {\cal D}_1 \\
4017: \Pi; \Gamma, A \wedge B^{\mu}_X, A^{\mu}_X, B^{\mu}_X
4018: \proves \Delta; \Theta
4019: \end{array}}
4020: {\Pi; \Gamma, A \wedge B^{\mu}_X
4021: \proves \Delta; \Theta}
4022: \]
4023: %
4024: Apply the induction hypothesis to ${\cal D}_1$. If the result
4025: ends in a (decide) inference, let ${\cal D}_1'$ be the immediate
4026: subderivation of the result; otherwise let ${\cal D}_1'$ be the
4027: result itself. ${\cal D}_1'$ is an SCLP derivation with an
4028: end-sequent of the form:
4029: %
4030: \[
4031: \Pi ; \m E \proves \m F; \Theta
4032: \]
4033: %
4034: $E$ must be a side expression of the inference in question,
4035: here $(\wedge\proveslabel)$; otherwise the corresponding inference
4036: could not have been linked in ${\cal D}$. One of the inference
4037: figures $(\wedge\proveslabel_L)$ and $(\wedge\proveslabel_R)$ must
4038: apply depending on which side expression $E$ is. For concrete
4039: illustration, we suppose $E$ is $A^{\mu}_X$; then we construct
4040: ${\cal D}'$ as:
4041: \[
4042: \derivi{$\wedge\proveslabel_L$}
4043: {\begin{array}{c}
4044: {\cal D}_1' \\
4045: \Pi ; A^{\mu}_X \proves F; \Theta
4046: \end{array}}
4047: {\Pi; A\wedge B^{\mu}_X \proves F; \Theta}
4048: \]
4049:
4050: Next, we suppose ${\cal D}$ ends in $(\imp\proveslabel^S)$, as
4051: follows:
4052: %
4053: \[
4054: \derivii{$\imp\proveslabel^S$}
4055: {\begin{array}{c}
4056: {\cal D}_1 \\
4057: \Pi; \proves A^{\mu}_X, \Delta; \Theta
4058: \end{array}}
4059: {\begin{array}{c}
4060: {\cal D}_2 \\
4061: \Pi; \Gamma, A\imp B^{\mu}_X, B^{\mu}_X \proves \Delta; \Theta
4062: \end{array}}
4063: {\Pi; \Gamma, A\imp B^{\mu}_X \proves \Delta; \Theta}
4064: \]
4065: %
4066: We begin by applying the induction hypothesis to the
4067: subderivation ${\cal D}_1$. After stripping off any (restart), we
4068: obtain an SCLP derivation ${\cal D}_1$ with end-sequent
4069: \[
4070: \Pi ; \proves C; \Theta
4071: \]
4072: By the usual linking argument, the expression $C$ must be
4073: identical to $A^{\mu}_X$. We then apply the induction hypothesis
4074: also to the right subderivation. Again, after stripping off any
4075: (decide), we get an SCLP derivation ${\cal D}_2$ with end-sequent
4076: \[
4077: \Pi; D \proves E; \Theta
4078: \]
4079: By the usual linking argument, $D$ must in fact be identical
4080: to $B^{\mu}_X$. Thus we obtain the needed ${\cal D}'$ by combining
4081: the two derivations by the SCLP $(\imp\proveslabel)$ rule:
4082: \[
4083: \derivii{$\imp\proveslabel$}
4084: {\begin{array}{c}
4085: {\cal D}_1' \\
4086: \Pi; \proves A^{\mu}_X ; \Theta
4087: \end{array}}
4088: {\begin{array}{c}
4089: {\cal D}_2' \\
4090: \Pi; B^{\mu}_X \proves E; \Theta
4091: \end{array}}
4092: { \Pi; A\imp B^{\mu}_X \proves E; \Theta }
4093: \]
4094:
4095: Finally, for $(\vee\proveslabel^B)$, we consider the
4096: representative case of ${\cal D}$ as schematized below:
4097: \[
4098: \derivii{$\vee\proveslabel^B_L$}
4099: {\begin{array}{c}
4100: {\cal D}_1 \\
4101: \Pi; \Gamma, A^{\mu}_X \proves \Delta; \Theta
4102: \end{array}}
4103: {\begin{array}{c}
4104: {\cal D}_2 \\
4105: \Pi', B^{\mu}_X ; \proves ; \Theta'
4106: \end{array}}
4107: {\Pi; \Gamma, A\vee B^{\mu}_X \proves \Delta; \Theta}
4108: \]
4109: We begin by applying the induction hypothesis to ${\cal D}_1$,
4110: the subderivation in the current block; if necessary, we strip off
4111: any initial (decide) inference, obtaining ${\cal D}_1'$ with an
4112: end-sequent that by linking takes the form:
4113: \[
4114: \Pi; A^{\mu}_X \proves E ; \Theta
4115: \]
4116: Next, we apply the induction hypothesis to the other
4117: subderivation. Since both local areas are empty in the input
4118: subderivation, they remain empty in the result subderivation: this
4119: gives ${\cal D}_2'$ with end-sequent:
4120: \[
4121: \Pi', B^{\mu}_X ; \proves ; \Theta'
4122: \]
4123: The two subderivations can be recombined by the SCLP
4124: $(\vee\proveslabel_L)$ inference to obtain the needed ${\cal D}'$:
4125: \[
4126: \derivii{$\vee\proveslabel_L$}
4127: {\begin{array}{c}
4128: {\cal D}_1' \\
4129: \Pi; A^{\mu}_X \proves E ; \Theta
4130: \end{array}}
4131: {\begin{array}{c}
4132: {\cal D}_2' \\
4133: \Pi', B^{\mu}_X ; \proves ; \Theta'
4134: \end{array}}
4135: {\Pi; A\vee B^{\mu}_X ; \proves E; \Theta}
4136: \]
4137: $\qed$
4138: