(R.&) If (S1 & S2 ) ∈ , start two sub-tableaux by adding S1 or S2 ,

respectively, to .

Logical Explanations 163

Negation can be handled by the following rewriting rule (RR): Rewrite

∼∼S as S; ∼(S1 ∨ S2 ) as (∼S1 & ∼S2 ); ∼(S1 & S2 ) as (∼ S1 ∨ ∼ S2 ); ∼(∃x) as

(∀x)∼; and ∼(∀x) as (∃x)∼. By means of this rewriting rule, each formula can

effectively be brought to a negation normal form in which all negation signs

are pre¬xed to atomic formulas or identities. We will abbreviate ∼(a = b) by

(a = b).

As derived rules (construing (S1 ⊃ S2 ) as a notational variant of

(∼ S1 ∨ S2 )), we can also have:

(L. ⊃) If (S1 ⊃ S2 ) ∈ , add ∼ S1 or S2 to , starting two sub-tableaux.

(R. ⊃) If (S1 ⊃ S2 ) ∈ , add ∼ S1 or S2 to .

For identity, the following rules can be used:

(L.self =) If b occurs in the formulas on the left side, add (b = b) to the

left side.

(L. =) If S[a] and (a = b) occur on the left side, add S[b] to the left side.

Here, S[a] and S[b] are like each other except that some occurrences of a or

b have been exchanged for the other one. The corresponding right-hand rules

(R.self =) and (R. =) are like (L.self =) and (L. =) except that = has been

replaced by its negation = and vice versa.

As we stated, it can be shown that if F G is provable in ¬rst-order logic,

it is provable by means of the rules just listed. A proof means a tableau that

is closed. A tableau is said to be closed if and only if the following condition

is satis¬ed by it: There is a bridge from each open branch on the left to each

open branch on the right. Here, a bridge means a shared formula (it can be

assumed to be an atomic formula or identity). A branch is open if and only if

it is not closed. A branch is closed if it contains a formula and its negation, or

contains (a = a) on the left or (a = a) on the right.

The completeness of our set of rules can be proved in the usual way. (This

completeness holds even if (L.A) and (R.E) are restricted as indicated above.)

If F G cannot be proved by our rules, there is a pair of possibly in¬nite

branches on the left and on the right without a bridge to which no further

applications of the rules are possible. The formulas on the left and the nega-

tions of the formulas form (after the obvious applications of (RR)) what has

been called a “model set” or “Hintikka set.” Then, F and ∼G are true in the

same model, and G hence does not follow logically from G. This is enough

to show that if G follows logically from F, then F G is provable by our

rules.

In the interpolation theorem, we are given a tableau proof of F G by means

of the rules listed here. It is assumed in the new interpolation theorem, just

as in Craig™s (1957) well-known theorem, that neither ∼F nor G is provable.

It can be assumed that F and G are in the negation normal form. The crucial

question is how an interpolation formula is found on the basis of this tableau.

For this purpose, it may be noted that, because of the assumptions just made,

Socratic Epistemology

164

there must be at least one branch open on the left and at least one on the right.

Since the tableau is assumed to be closed, there must be a bridge connecting

each such pair of open branches. It can also be assumed that all the formulas

are in the negation normal form.

Then the new interpolation formula can be constructed as follows:

Step 1. For each open branch on the left, form the conjunction of all the

formulas in it that are used as bridges to the right. They can be

assumed to be atomic.

Step 2. Form the disjunction of all such conjunctions.

Step 3. Replace each constant introduced (i) by an application of (L.E),

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

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 proved that the formula IL obtained in this way is always an

interpolation formula in the sense of Craig™s theorem”that is, we have F IL

and IL G. A proof to this effect will not be given here, however. The resulting

new interpolation theorem is speci¬ed much more closely than Craig™s (1957),

who only requires that the non-logical constants of the interpolation formula

all occur both in F and in G. Instead of a detailed proof, which the reader can

easily construct, we will illustrate the nature of the interpolation formula by

means of a couple of examples.

Consider ¬rst the following closed tableau (Tableau 1) and the interpolation

formula it yields:

tableau 1

(2) (∀y)(L(b,y) ⊃ m = y) ⊃ (m = b)

(1) (∀x)L(x,b) IP UC

(3) ∼(∀y)(L(b,y) ⊃ m = y) from (2) by (R.⊃)

(6) L(b,b) from (1) by (L.A)

(4) m = b from (2) by (R. ⊃)

(5) (∃y)(L(b,y) & (m = y)) from (3) by the

rewrite rule

(7) L(b,b) & (m = b) from (5) by (R.E)

(9) m = b from (7) by

(8) L(b,b) from (7) by

(R.&) (R.&)

Bridge to (6) Closure by (4), (9)

The interpolation formula is trivially

L(b, b) (1.1)

Logical Explanations 165

This example may prompt a deja vu experience in some readers. If one inter-

´`

prets L(x,y) as “x loves y,” b as “my baby,” and m as “me,” we get a version of

the old introductory logic book chestnut. The initial premise (IP) says:

Everybody loves my baby (1.2)

and the ultimate conclusion (UC) says

If my baby loves only me, then I am my baby. (1.3)

Textbook writers cherish this example, because it gives the impression of

expressing a clever, non-trivial inference. In reality, their use of this exam-

ple is cheating, trading on a mistranslation. In ordinary usage, (1.2) does not

imply that my baby loves him/herself. Its correct translation is therefore

(∀x)(x = b ⊃ L(x,b)) (1.4)

which does not any longer support the inference when used as the premise.

Hence the inference from the initial premise to the ultimate conclusion turns

entirely on the premise™s implying L(b,b). This is, in an obvious sense, what

explains the inference. This explanation of the consequence relation is strik-

ingly re¬‚ected by the fact that L(b,b) is precisely the interpolation formula.

In order to see that the explanatory role of the interpolation formula in this

example is no freak, consider another example of a closed tableau (Tableau 2)

and its interpolation formula. To enhance an overview of the tableau argument,

we have not indicated where the different steps come from. (This is easy for

the reader to ascertain, anyway.)

tableau 2

(1) (∀x)((A(x) & C(x)) ⊃B(x)) (3) (∀x)(E(x) ⊃ (A(x) ⊃

IP

B(x))) UC

(2) (∀x)((D(x) ∨ ∼D(x)) ⊃ C(x)) (4) (E( ) ⊃ (A( ) ⊃ B( )))

IP

(9) (A( ) & C( )) ⊃ B( ) (5) ∼E( )

(10) ∼(A( ) & C( )) (6) (A( ) ⊃ B( )

(11) B( )

Bridge

(12) ∼C( ) (13) ∼A( ) (7) ∼A( )

Bridge

(14) (D( ) ∨ ∼D( )) ⊃ C( ) (8) B( )

(15) ∼(D( ) ∨ ∼D( ) (16) C( )

Closure

(17) ∼D( )

(18) ∼∼D( )

Closure

The interpolation formula is, as one can easily ascertain,

(∀x)(∼A(x) ∨ B(x)) (1.5)

Socratic Epistemology

166

But does it in any sense provide an explanation as to why the conclusion

holds? In this example, the ¬rst initial premise says that whatever is both C and

A is also B. But the second initial premise entails the premise that everything

is C anyway. Hence the cash value of the initial premises is that if anything is

A, it is also B. The conclusion says that if any E is A, then it is B. But any A