the premises that suf¬ces to imply the conclusion is:

(∀x)(A(x) ⊃ B(x)) (1.6)

which is equivalent to the interpolation formula (5). Again, the interpolation

formula expresses the reason (“explanation”) why the logical consequence

relation holds.

The new interpolation theorem applies more widely than Craig™s interpola-

tion theorem. The same construction as was used in the argument earlier can

be used to ¬nd explanatory interpolation formulas even when the premise F

and the conclusion G share all the same non-logical constants, in which case

Craig™s theorem becomes empty.

An example will illustrate this. Let

F = (∀x)(L(c,x) ⊃ (∀y)(L(x,y) ⊃ ∼ L(y,x)))

G = ∼ (∀x)((∀y)(L(x,y) ⊃ ∼ L(y,x)) ⊃ L(c, x))

If L(a,b) is read as “a loves b,” then F says that c loves only people whose love

is always unrequited, while G says that it is not the case that c loves all such

unfortunate folks. A tableau (Tableau 3) for F G might look like this

tableau 3

(1) (∀x)(∼L(c,x) ∨ (∀y)(∼L(x,y) ∨ ∼L(y,x))) (2) (∃x)((∀y)(∼L(x,y) ∨

IP

∼L(y,x))&∼L(c,x)) UC

(3) ∼L(c,c) ∨ (∀y)(∼L(c,y) ∨ ∼L(y,c)) from (1) (7) (∀y)(∼L(c,y) ∨

∼L(y,c)) & ∼L(c,c)

from (2)

First branch: First branch:

(4) (∀y)(∼L(c,y) ∨ ∼L(y,c)) from (3) (8) ∼L(c,c) from (7)

Bridge to (6)

(5) ∼L(c,c) ∨ ∼L(c,c) from (4) Second branch:

(9) (∀y)(∼L(c,y) ∨

∼L(y,c)) from (7)

(6) ∼L(c,c) from (5)”merges with the second (10) ∼L(c, ) ∨ ∼L( ,c)

branch from (9)

(11) ∼L(c, ) ∨ ∼L( ,c) from (4) (14) ∼L(c, ) from (10)

(12) ∼L(c, ) from (11) (13) ∼L( ,c) from (11) (15) ∼L( ,c) from (10)

Bridge to (14) Bridge to (15)

Logical Explanations 167

The interpolation formula is seen to be equivalent to

I = (∀y)(L(c,y) ⊃ ∼ L(y,c)) & ∼ L(c,c) (1.7)

This makes sense as an explanation of F G. For what (1.7) says is that c itself

is a counterexample to the claim that c loves all people whose love is never

requited.

Such examples bring out vividly the fact that the interpolation theorem is

already by itself a means of explanation. The precise sense in which this is the

case will be discussed later in this chapter.

An interesting perspective opened up by these results is the possibility of

measuring the dif¬culty of proving a consequence relation F G by means of

the complexity of the interpolation formula I, as constructed by our rule. An

especially important component of this complexity is the number of quanti¬ers.

It can be seen to equal the number of individuals one has to introduce to the

con¬guration of individuals that is being built on the left side of a tableau in

order to see that the consequence relation holds.

But these explanations (and these examples) tell only half of the story.

Besides the interpolation formula IL de¬ned earlier, we can form another one.

Indeed, the instructions for forming IL (Steps 1“3 earlier) are not left-right

symmetrical. Indeed, IL depends almost exclusively on the left side of the

tableau, the only exception being the steps where a constant that has not yet

occurred on the left side is imported into it by an application of (L.A). Another

interpolation formula IR can be formed as follows:

Step 1* For each open branch on the right, form the disjunction of all the for-

mulas in it that are used as bridges to the left. They can be assumed

to be atomic.

Step 2* Form the conjunction of all such disjunctions.

Step 3* Replace each constant introduced (i) by an application of (R.A),

or (ii) by an application of (R.E) from the left side to the right,

by a variable, say x, different for different rules and for different

applications of the same rule.

Step 4* Moving from the end (bottom) of the tableau upwards step by step,

pre¬x (∀x) in case (i) to the formula so far obtained. In case (ii),

pre¬x (∃x) to the formula so far obtained.

It can easily be shown that the formula IR so obtained is an interpolation

formula. It can also be shown that IL IR .

One can say even more here. Not only does the logical consequence relation

hold in the case of our interpolation formulas. It is always a trivial or analytic

consequence relation, sometimes called a “surface consequence” or “corol-

larial consequence.” (See Chapter 8 of this volume.) Without attempting an

explicit de¬nition of this notion here, it can be characterized intuitively by say-

ing that such a consequence relation can be seen to hold without considering

Socratic Epistemology

168

con¬gurations of individuals other than are already considered in IL or

in ∼IR .

The following example (Tableau 4) illustrates the relationship between IL

and IR :

tableau 4

(1) (∃x)A(x) IP (3) (∀x)B(x) UC

(2) (∀z)(A(z) ⊃ (∀y)L(z,y)) (4) (∃z)((∃y)L(y,z) & ∼B(z))

IP UC

(5) A( ) from (1) B( ) from (3)

(10) (∃y)L(y, ) & ∼B( ) from (4)

(6) (A( ) ⊃ (∀y)L( ,y)) from (2) (11) ∼B( ) from (12) (∃y)L(y, )

(10) from (10)

Closure from

(9), (11)

(7) ∼A( ) from (6) (8) (∀y)L( ,y) (13) L( , ) from

Closure from from (6) (12)

(5), (7) Bridge to (14)

(14) L( , )

Bridge

to (13)

Here, (2) can be taken to say that anyone who has the property A loves

everybody. (1) says that such a person exists. The disjunction of (3) and (4)

says that either everybody is B or else some non-B is loved by someone.

In this case we clearly have

IL = (∃x)(∀y)L(x,y) (1.8)

IR = (∀y)(∃x)L(x,y) (1.9)

IR , i.e. (∃x)(∀y)L(x,y)

IL (∀u)(∃z)L(z,u) (1.10)

This is, again, most natural. For as soon as there is some A loving everybody,

obviously there every non-B is loved by him or her”unless everybody is B.

Hence (1.10) in a natural sense explains why the consequence relation in

question holds.

Moreover, to see this we need to consider only the two individuals x,y to

see that the consequence relation holds. This matches the tableau argument

earlier, where precisely two individuals and need to be considered.

This example (Tableau 4) suggests a number of further things that can

be said about the two interpolation formulas and their interrelation. It also

suggests a proof that IL and IR are both interpolation formulas in Craig™s sense.

First, F IL can be proved by applying to the right side the duals of the

quanti¬er rules that were applied in the proof of F G on the left, and that

prompted the introduction of an individual to IL .

Logical Explanations 169

Second, IR G can be proved dually. Hence, what remains to be proved is:

IL IR (1.11)

A proof of (7) can in this example be obtained in effect as a part of the proof

of F G. In general, an explicit argument to show the provability of (1.11) can

be obtained by induction on the length of the tableau proof of F G. We will

leave the details to the reader as an exercise.

Such as argument will show that (1.11) is a trivial consequence in more than

one sense. Its tableau proof will be no longer than that of F G, from which

it is easily obtained.

The corresponding conditional:

(IL ⊃ IR ) (1.12)

can be shown to be a surface tautology in the sense of Hintikka (1970). (See also

Chapter 8, in this volume.) Moreover, the argument from IL to IR can be con-