is derivable in LG.
Proof. Note that the sequent A1 , . . . , Am ’ B1 , . . . , Bn is logically valid if
and only if the block T A1 , . . . , T Am , F B1 , . . . , F Bn is not satis¬able. Thus,
soundness and completeness of LG is equivalent to soundness and completeness
of the block tableau method. The latter is in turn easily seen to be equivalent
to soundness and completeness of the signed tableau method, as presented in
Theorems 2.3.9 and 2.5.5.
Exercise 3.4.10. Let LG(atomic) be a variant of LG in which “, A ’ A, ∆ is
assumed only for atomic LV sentences A. Show that LG(atomic) is sound and
complete. (Hint: Use the result of Exercise 2.5.7.)
Exercise 3.4.11.
1. The modi¬ed block tableau rules are a variant of the block tableau rules of
De¬nition 3.4.3, replacing each nonbranching rule of the form
S, X

S, X, Y1 , Y2
by a pair of rules
S, X S, X
 
S, X, Y1 S, X, Y2
Show that the modi¬ed block tableau rules are sound and complete.
2. Let LG be the variant of LG corresponding to the modi¬ed block tableau
rules. Write out all the rules of LG explicitly. Show that LG is sound
and complete.
48
3.5 The Interpolation Theorem
As usual, let L be a language and let V be the set of parameters.
Theorem 3.5.1 (the Interpolation Theorem). Let A and B be LV sentences.
If A ’ B is logically valid, we can ¬nd an LV sentence I such that:
1. A ’ I and I ’ B are logically valid.
2. Each predicate and parameter occurring in I occurs in both A and B.
Such an I is called an interpolant for A ’ B. We indicate this by writing
I
A ’ B.
Remark 3.5.2. If A and B have no predicates in common, then obviously the
theorem is incorrect as stated, because all LV sentences necessarily contain at
least one predicate. In this case, we modify the conclusion of the theorem to
say that at least one of ¬ A and B is logically valid.3 The conclusion is obvious
in this case.
In order to prove the Interpolation Theorem, we introduce a “symmetric”
variant of LG, wherein sentences do not move from one side of ’ to the other.
De¬nition 3.5.3. A signed sequent is an expression of the form M ’ N where
M and N are ¬nite sets of signed LV sentences. A variant of M ’ N is a
signed sequent obtained from M ’ N by transferring sentences from one side
of ’ to the other, changing signs. In particular, M, X ’ N and M ’ X, N
are variants of each other, where we use an overline to denote conjugation, i.e.,
T A = F A, F A = T A.
De¬nition 3.5.4. Let
C1 , . . . , Cm ’ D1 , . . . , Dn
be an unsigned sequent4 . A signed variant of C1 , . . . , Cm ’ D1 , . . . , Dn is any
variant of the signed sequent
T C1 , . . . , T Cm ’ T D1 , . . . , T Dn .
Note that each signed sequent is a signed variant of one and only one unsigned
sequent. We de¬ne a signed sequent to be logically valid if and only if the
corresponding unsigned sequent is logically valid.
De¬nition 3.5.5. LG(symmetric) is the following proof system.
1. The objects are signed sequents.
3 Thisamounts to saying that at least one of the truth values T and F is an interpolant for
A ’ B.
4 An unsigned sequent is just what we have previously called a sequent.
49
2. We have
M, X ’ X, N
and
M, X, X ’ N
and
M ’ X, X, N
for all X.
3. For each signed tableau rule of the form
. . . .
. . . .
. . . .
X X X X
. . . .
. . . .
. . . .
  /\ /\
Y Y1 Y Z Y1 Z1
Y2 Y2 Z2
we have a corresponding pair of signed sequent rules
M, X, Y ’ N M ’ X, Y , N
M, X ’ N M ’ X, N
M, X, Y1 , Y2 ’ N M ’ X, Y1 , Y2 , N
M, X ’ N M ’ X, N
M, X, Y ’ N M, X, Z ’ N M ’ X, Y , N M ’ X, Z, N
M, X ’ N M ’ X, N
M, X, Y1 , Y2 ’ N M, X, Z1 , Z2 ’ N M ’ X, Y1 , Y2 , N M ’ X, Z1 , Z2 , N
M, X ’ N M ’ X, N
respectively.
Lemma 3.5.6. An unsigned sequent is derivable in LG if and only if all of its
signed variants are derivable in LG(symmetric).
Proof. The proof is by induction on the length of derivations in LG. The
base step consists of noting that all signed variants of “, A ’ A, ∆ are of
the form M, X ’ X, N or M, X, X ’ N or M ’ X, X, N , hence deriv
able in LG(symmetric). The inductive step consists of checking that, for each
rule of inference of LG, if all signed variants of the premises are derivable
in LG(symmetric), then so are all signed variants of the conclusion. This is
straightforward.
50
Theorem 3.5.7. LG(symmetric) is sound and complete. In other words, a
signed sequent is logically valid if and only if it is derivable in LG(symmetric).
In particular, an LV sentence A ’ B is logically valid if and only if the signed
sequent T A ’ T B is derivable in LG(symmetric).
Proof. Soundness and completeness of LG(symmetric) follows from Theorem
3.4.9, soundness and completeness of LG, using Lemma 3.5.6.
We now prove the Interpolation Theorem.
De¬nition 3.5.8. Let M ’ N be a signed sequent. An interpolant for M ’ N
is an LV sentence I such that the signed sequents M ’ T I and T I ’ N are
logically valid, and all predicates and parameters occurring in I occur in both
I
M and N .5 We indicate this by writing M ’ N .
In order to prove the Interpolation Theorem, it su¬ces by Theorem 3.5.7 to
prove that every signed sequent derivable in LG(symmetric) has an interpolant.
We prove this by induction on the length of derivations.
For the base step, we note that X is an interpolant for M, X ’ X, N , and
X
that M, X, X ’ and ’ X, X, N are logically valid. Thus we have M, X ’ X, N
F T
and M, X, X ’ N and M ’ X, X, N .
For the induction step we show that, for each rule of LG(symmetric), given
interpolants for the premises of the rule, we can ¬nd an interpolant for the
conclusion. We present some representative special cases.
I I
M, T A & B, T A, T B ’ N M ’ F A & B, F A, FB, N
I I
M, T A & B ’ N M ’ F A & B, N