JAIST Repository

(1)

JAIST Repository

https://dspace.jaist.ac.jp/

Title

二重様相論理に関する幾つかの結果

Author(s)

丸山, 晃生

Citation

Issue Date

1999‑03

Type

Thesis or Dissertation

Text version

author

URL

http://hdl.handle.net/10119/1247

Rights

Description

Supervisor:小野寛晰, 情報科学研究科, 修士

(2)

By Akio Maruyama

A thesis submitted to

School of Information Science,

Japan Advanced Institute of Science and Technology,

in partial fulllment of the requirements

for the degree of

Master of Information Science

Graduate Program in Information Science

Written under the direction of

Professor Hiroakira Ono

February 15, 1999

Copyrightc 1999byAkioMaruyama

(3)

1 Intro duction 1

2 Preliminaries 3

2.1 Sequentcalculus LK : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 4

2.2 Mix rule : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6

2.3 Monomodal systems : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7

3 Syntactic results on bimodal logics 8

3.1 Bimodal logics : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 8

3.2 S5 3

lacks cut-elimination prop erty: : : : : : : : : : : : : : : : : : : : : : 10

3.3 Subformula property byTakano's method : : : : : : : : : : : : : : : : : 11

3.4 Decidability : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 22

3.5 Craig'sinterp olation theorem : : : : : : : : : : : : : : : : : : : : : : : : 23

3.6 Remarks : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 28

4 Kripke typ e semantics 29

4.1 Kripkeframes and models : : : : : : : : : : : : : : : : : : : : : : : : : : 29

4.2 Completeness : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 31

4.3 Finitemodel property : : : : : : : : : : : : : : : : : : : : : : : : : : : : 37

4.4 decidability : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 43

(4)

Introduction

Manyreasoningswhichappearindailythoughtareofteninuencedbysituations,states,

the passage of time and so on. The intro duction of mo dal logics to take the situations,

states and the passageof time intoconsiderationis veryuseful. K whichisthe smallest

normal modal logic, KT and S4 which characterize temporal logic , S5 which charac-

terizes epistemic logic and soonare well-known monomodal logics . The variouslogical

properties of them have b een found out already. There are many syntacticalresults on

them. Many monomodal logics have been investigated well since the earlytime of 20th

century. On the other hand, in many multimo dal logics with several modalities, how-

ever, even the most elementary questions concerning completeness, decidability and so

onhaven't been unsolved. From the point of viewof application of modal logics, modal

logics with one modality are sometimes not sucient, and hence introductionof several

modalities will be necessary in many situations. For example, epistemic logics with no-

tion of tense will be able to express knowledge in the past and the future. Epistemic

logics and temporal logics themselves can be also regarded as a kind of bimodal logics.

Moreover,we assumeingeneralthatmodalitiesintemporallogics havecertain relations

among them. On the other hand, for independently axiomatizable modal logics, the

notion of the fusion of them were rstly introduced by S. Thomason 1980. Recently,

independently axiomatizable bimodal logics as special bimodal logics are investigated

semantically by M. Krachtand F. Wolter [3].

This paperpresentsastudyof bimodal logics,that is,modallogics withtwomodali-

ties,andwilldiscussthesebybothsyntacticandsemanticalmetho d. Thecut-elimination

properties of the fusions will be discussed in the syntactical studies. In the semantical

approaches, dependentlyaxiomatizablebimodal logicswill bemainly discussed. Wewill

consider the fusion of well-known logics ( K, KT, S4 and S5 ) and see several logical

(5)

In Chapter 2, several basic monomo dal logics and their sequent systems are intro duced

in the preliminaries, and several notations and denitions which will b e used in later

sectionare given. InChapter 3,wewill describe somesequentsystems corresp ondingto

fusions and derive cut-elimination properties,subformula properties and so on of them.

The cut-eliminationtheorem forsome systems,rst, will beprovedinusualway[4]. On

the other hand, some systems for fusions are shown not to enjoy cut-elimination prop-

erty. For systems which lack cut-elimination property, however, we will show that the

systems havesubformulaproperty, byextending Takano's metho d[11] for S5 3

. Thenas

a corollary, the decidability for the systems will be derived inthe same way as that by

Gentzen [4]. The last topic in Chapter 3 is the Craig's interp olation theorem for these

systems. Toprove the theorem, we will use Maehara'smethod [13]. The method works

well even for the systems lacking cut-elimination property, since they have the subfor-

mula property. As contrasted with the independently axiomatizable bimo dal logics, for

instance, a bimodal logic with the axiom 2p p is a dep endently axiomatizable bi-

modallogic. Forthedependentlyaxiomatizablebimodallogics,however,itisdicultfor

us tond out the systems with cut-elimination property. Next we will study semantics

for bimo dal logics. As Kripke completeness and nite model property of fusions have

been extensively studiedbyM. Krachtand F. Wolter [3], here wewill studythese prop-

ertiesfordependentlyaxiomatizablebimodallogics. Itisquitehardtodevelopageneral

semantical study of dependently axiomatizable bimo dal logics at this moment. So, as

a steppingstone to future study of this topics, we will restrict ourselves to the study of

Kripkecompletenessand the nitemodel propertyof bimodal logics whichare obtained

from afusion of two monomo dal logics by addingan axiom of the formpp, where

and are sequences of twobox op erators.

(6)

Preliminaries

In this chapter, several notations and denitions for some monomodal logics are given.

The language L

2

of propositional monomodal logic consists of

propositional variables: p,q,r,111

logical symb ols: ^,_, , :,2.

Formulas, denoted byA, B, C,111, are constructed inthe usual wayfrom propositional

variables and logical symb ols. In particular, 2A is a formula when A is a formula.

We may app end indexes to propositional variables and formulas. Greek capital letters

0; 1; 5; 6, 2 and 4 denote sequences of formulas. 20 denotes 2A

1

;2A

2

;111;2A

n ,

when 0 isA

1

;A

2

;111;A

n .

Denition 2.1 (modal logic) A set L of formulas in L

2

is a mo dal logic, if the fol-

lowing conditions are satised:

all tautologiesbelong to L,

if A;AB 2L, then B 2L,

if A2L,then 2A2L,

if A2L,then any substitution instance of A belongsto L.

LetL bea modallogic (of L

2

),andQ bea setofformulas( ofL

2

).Thenthe least

modal logic containingthe set L[Q is denoted by L L

Q. K denotes the least modal

logic containing the axiom 2(p q) (2p 2q). Any modal logic with the axiom

2(p q) (2p 2q) is called a normal modal logic. The following modal logics are

well-known :

KT=K L

f2ppg

K4=K L

f2p22pg

S4 =K L

f2pp;2p 22pg

(7)

S5 =K f2pp;:2:p2:2:pg

Wewill discuss the combinations of these basic monomodal logicsas fusions.

2.1 Sequent calculus LK

As a formalization for mo dal logics, we will adopt sequent calculus. It based on the

system LK intro duced by G.Gentzen. Any expression of the form 0 ! 1 is called

a sequent. Here, 0 and 1 are called the antecedent and the succedent of the sequent,

respectively.

An inferenceis expressed by the form

S

1

S or

S

2 S

3

S

;

where S

1 , S

2 , S

3

and S are sequents. S

1 , S

2

and S

3

are called the upper sequents and

S is called the lower sequent of the inference. In particular, S

2 ( S

3

) is called the left

(right) upper sequent of the inference.

The sequent system LK for the classical logic has the following initial sequents and

inferences.

Initial sequents:

the sequentsof the formA!A,

Structural rules:

( weakeningrule )

0!1

A;0! 1

(w!)

0!1

0!1;A

(!w)

( contraction rule )

A;A;0!1

A;0 !1

(c!)

0!1;A;A

0!1;A

(!c)

( exchangerule )

0;A;B;5!1

0;B;A;5!1

(e!)

0!1;A;B;6

0!1;B;A;6

(!e)

( cut rule )

0!1;A A;5!6

0;5!1;6

(cut)

(8)

A;0!1

A^B;0!1

(^!)

B;0!1

A^B;0!1

(^!)

0!1;A 0! 1;B

0!1;A^B

(!^)

A;0!1 B;0!1

A_B;0!1

(_!)

0!1;A

0!1;A_B

(!_)

0!1;B

0!1;A_B

(!_)

0!1;A B;5!6

AB;0;5!1;6

(!)

A;0!1;B

0!1;AB

(!)

0!1;A

:A;0!1

(:!)

A;0!1

0!1;:A

(!:) :

Weakening, contraction andexchangerules are calledweak inferences;w:i:for short.

TheformulaAincut ruleiscalledthecut formulaofthe cut. In thelogicalrules,A^B,

A_B, A B and :A which appear in the lower sequent are called principal formulas

of the rules.

Denition 2.2 (proof and end-sequent) Proof and the end-sequent are dened in-

ductively as follows:

Initial sequent is proof, and end-sequent of the proof is itself.

Let P

1

and P

2

be proofswith the end-sequents S

1

and S

2

, respectively. If

S

1

S or

S

1 S

2

S

is one of the inferences in LK, then

P

1

S or

P

1 P

2

S

is proof,and the end-sequent is S.

Denition 2.3 (thread) A sequence of sequents in a proof is called a thread of the

proof if the following conditions are satised:

the sequence begins with an initial sequent and ends with the end-sequent,

every sequent in the sequence except the last is an upper sequent of an inference,

and is followed immediately by the lower sequent of this inference.

(9)

2.2 Mix rule

As aninstrument toeliminate cut rules, weintro ducethe mix rule:

0!1 5!6

0;5

A

!1

A

;6

(A) ;

where A 2 5\ 1, and 5

A

and 1

A

denote the sequences obtained from 5 and 1 by

deleting all occurrences of the formula A in them, respectively. The formula A in the

aboveruleiscalledthemixformulaofthismix. Bymeansofmix,cutcanberepresented

as follows:

0!1 5!6

0;5

A

!1

A

;6 (A)

0;5!1;6

(w:i:) :

Tothe contrary, bymeans of cut, mix can b e represented as follows:

0!1

A

;A (w:i:)

5!6

A;5

A

!6 (w:i:)

0;5

A

!1

A

;6

(cut) :

In this sense, the mix rule and the cut rule are equivalent. Socut- eliminationtheorem

can b e proved by mix-elimination. The outline of the proof of mix-elimination is as

follows:

1) concentrate toone of the uppermostmixes,

2) eliminate the mix by double induction on the degree and the rank which referto

the followingdenitions.

Denition 2.4 (degree) The degreeof a formula A,denotedbydeg(A), isthe number

of logical symbols which occur in A.

Denition 2.5 (rank) Let P be a proof which contains a mix rule only as the last

inference. The left(right)rankof P, denotedby

l (

r

),isthe max number of consecutive

sequents which contain mix formula in the succedent(antecedent), counting upward from

the left(right)upper sequent of themix. Then =

l +

r

isthe rankof P. ( Since

l 1

and

r

1, 2. )

The cut-elimination theorem of LKis provedin detailby [4], [13].

(10)

Inthissection,wewilldescribethe systemK 3

,KT 3

,S4 3

andS5 3

. First,K 3

isobtained

from the system LK by adding the following inference rule:

0!A

20!2A (2) :

Wecan obtain various modal systems from LKby addingsome inferencerules. KT 3

is

the system obtained fromLK byadding the followinginference rules:

A;0!1

2A;0 !1

(2 !)

0!A

20!2A

(!2) :

It is easy to see that, for any formula C, C is in KT if and only if ! C is provable in

KT 3

. In this sense, KT and KT 3

are equivalent. S4 3

is the system obtained from LK

by adding the followinginference rules:

A;0!1

2A;0 !1

(2 !)

20!A

20!2A

(!2) :

Also, S4 and S4 3

are shown to be equivalent. S5 3

is the system obtained from LK by

adding the followinginference rule:

A;0!1

2A;0! 1

(2!)

20!21;A

20!21;2A

(!2) :

S5 and S5 3

are equivalent. See e.g. [8] [9], for the details. It is known that K 3

,

KT 3

and S4 3

enjoy cut- elimination property, but S5 3

lacks it. The cut-elimination

theorem of the system S4 3

are shown by M. Ohnishi and K. Matsumoto [6]. The cut-

free systems for S5 are given by G. E. Mints [5], M. Sato [10] and so on, but they are

complicated. So,the decidabilityand Craig'sinterpolationtheorem ofK 3

,KT 3

andS4 3

are obtained from cut-elimination property by using the standard method. As for S5 3

,

the subformula property has been shown by Takano [11]. Hence, the decidability and

Craig's interp olation theorem followsfromthis.

(11)

Syntactic results on bimodal logics

M. Kracht and F. Wolter developed a semantical study of fusions of independently ax-

iomatizablemodallogics[3]. Inthis chapter,wewillintro ducesequentsystemsoffusions

of some basic monomo dal logics and study logical properties like the decidability and

Craig's interp olation theorem by using these systems. To show them, we rst discuss

cut-elimination prop erty and subformula property for these systems. Since it is shown

that the system for S5 3

lacks cut-elimination property, any system of fusions, one of

whose component is S5 3

, lack cut-elimination property. We will show, however, that

Takano's method works well also for these systems, and hence we can get subformula

property of them [11] [12].

3.1 Bimodal logics

The language L

2

of prop ositional bimodal logic has

propositional variables: p,q,r,111

logical symb ols: ^,_, , :,2, .

Formulas, denoted byA, B, C,111, are constructed inthe usual wayfrom propositional

variablesand logical symb ols. In particular,both 2Aand A are formulaswhen A isa

formula. Wemay append indexestothe propositional variablesandtheformulas. Greek

capitalletter 0, 1,5, 6,2, 4and 7 denotesequences of formulas. 20 and 0 denote

2A

1 ,2A

2

,111,2A

n

and A

1 , A

2

,111, A

n

respectively,when0isA

1 ,A

2

,111,A

n . We

may also append indexes to the Greek letters. Sub(A) denotethe set of allsubformulas

of aformula A. A bimodal logicLof L

2

isdenedbyaddingthe followingconditionto

the denition of monomodal logicL:

if A2L,then A2L.

(12)

2

tively.The fusion of M and N, denoted by M N

N, is the least bimodal logic in L

2

containing both M and N.

When we wantto specify the modality in alogic M, we will attach the modality to

M. Forinstance, M

2

denotes amodal logic inL

2 .

For M 3

;N 3

2 fK 3

;KT 3

;S4 3

;S5 3

g, we will introduce sequent systems of the form

M 3

N

N 3

. The systems M 3

N

N 3

is obtained from M 3

and N 3

, simply by combining

theirinferences. Of course,itisnecessarytodistinguishonemodalityfromanother. For

example, S4 3

N

S5 3

is dened as follows. Let and 2 b e the modalities for S4 3

and

S5 3

, respectively. The system S4 3

N

S5 3

is obtained from LK by adding the following

inference rules:

A;0!1

( !)

0!A

0! A

(! )

A;0!1

2A;0! 1

(2!)

20!21;A

20!21;2A

(!2) :

It is easyto seethe following.

Lemma 3.2 For any formula C, ! C is provable in M 3

N

N 3

if and only if C is in

M N

N.

Without any diculty, we can showthe following.

Theorem 3.3 (cut-elimination theorem)

Let M 3

;N 3

2fK 3

;KT 3

;S4 3

g. Then every proof in M 3

N

N 3

canbe transformed, with-

out changing the end-sequent, into cut-free one.

Pro of. We rst replaced all cuts by mixes, and can show this theorem by double

induction onthe degreeand the rankas usual.

Corollary 3.4 (subformula property)

Let M 3

;N 3

2 fK 3

;KT 3

;S4 3

g. Then all formulas which construct cut-free proof in

M 3

N

N 3

consist of the subformulas of formulas which occurin the lowest sequent.

Pro of. For any inferences rule I except cut rule, the upper sequents of I consist of

the subformulas of formulas in the lowersequentof I.

(13)

3.2 S5 lacks cut-elimination property

Nextwewilldiscussthecut-eliminationprop ertyofsequentsystemsforfusions,atleast,

oneofwhosecomponentisS5 3

. WerstnotethatS5 3

lacksthecut-eliminationproperty,

while eachof K 3

, KT 3

and S4 3

has it.

Lemma 3.5 S5 3

lacks cut-elimination property.

Pro of. This example was noticed rst by M. Ohnishi and K. Matsumoto [7]. The

sequent p ! 2:2:p is provable in S5 3

. In fact, the following proof is a proof of

p!2:2:pinS5 3

:

2:p!2:p

^!^:2:p;^2:p ^!^2:2:p;^2:p

p!p

:p;p!

2:p;p! ^p^!^2:2:p

(cut)

Next, we will show that p !2:2:p is not provable in S5 3

. Supp ose otherwise. Then

it is easy to seethat the lowest inference of the pro of must b e either weakening rule or

contraction rule.

Case 1: The lowestinferenceis weakeningrule.

Inthis case,the uppersequentoftheinferencerule isp!or!2:2:p. Butclearly

both sequents are not provable inS5 3

.

Case 2: The lowestinferenceis contraction rule.

In this case, the upper sequent of the inference rule is p;p ! 2:2:p or p !

2:2:p;2:2:p. The inference rule which infer one of these sequents is weakening

rule or contraction rule. If the inference rule is weakening rule, any upper sequent of

the inference is a sequent which is former one or not provable in S5 3

. If the infer-

ence rule is contraction rule, an upper sequent of the inference is p;p;p ! 2:2:p;

p;p ! 2:2:p;2:2:p or p ! 2:2:p;2:2:p;2:2:p. Further, the inference rule

which one of these sequents is also weakening rule or contraction rule. If the inference

ruleisweakeningrule,theuppersequentoftheinferenceisthe sequentwhichisprevious

one or not provable in S5 3

. So, only possible sequents in the proof are sequents of the

form p;111;p!2:2:p;111;2:2:p. Thus,wecan neverget an initialsequent.

(14)

WehaveseenthatS5 3

lackscut-eliminationprop erty. Ontheotherhand,Takanoshowed

the following.

Theorem 3.6 EveryproofinS5 3

canbetransformed, withoutchangingtheend-sequent,

into the proof which has subformula property.

Forexample, allformulas whichare occurred inthe above pro of of p!2:2:pare

actually in Sub(2:2:q). Since S5 3

lacks cut-elimination property, any of K 3

N

S5 3

,

KT 3

N

S5 3

, S4 3

N

S5 3

and S5 3

N

S5 3

lacks it. We will show the subformula prop erty

for fusions by extending Takano's method for S5 3

into that for fusions. This section

presents syntactical approach for the systems corresponding to fusions. In this section,

wewill showthat the cutsin pro ofcan berestrict thecuts with subformulapropertyby

extending Takano's method for S5 3

into that for the systems corresponding to fusion (

Theorem 3.9 and Corollary 3.20 ).

Denition 3.7 (acceptable cut) A cut

0!1;A A;5!6

0;5!1;6

is acceptable, if the cut formula forms the subformula of a formula which occurs in the

lower sequent of the cut, namely A 2 Sub(0;1;5;6). The cut which is not acceptable

is called an unacceptable cut.

Denition 3.8 (suitable proof) A proof is suitable, if every cut applied in it is ac-

ceptable.

Theorem 3.9 Every proof in K 3

N

S5 3

, KT 3

N

S5 3

, S4 3

N

S5 3

or S5 3

N

S5 3

can be

transformed, without changing the end-sequent, into suitable one.

The system in which every proof can be transformed, without changing the end-

sequent, into suitable one has subformula property, since in the inference rules which

constructsuitableproofs,the uppersequentsoftheinferencesconsistof thesubformulas

of formulas in lower sequents. Imp ortance of this result will be shown in later section.

Wewill concentrate mainlyonS4 3

N

S5 3

inthe following,asother cases can betreated

similarly.

(15)

cut applied in it is acceptable or has a subformula of A as its cut formula.

Denition 3.11 (partition of sequence) A pair h7

1

;7

2

i of sequences is a partition

of sequence 4, if 7

1

\7

2

= and 7

1 [7

2

=4.

Lemma 3.12 Suppose 4 Sub(0;2;A). If 0;7

1

! 7

2

;2 has an A-suitable proof in

S4 3

N

S5 3

for every partition h7

1

;7

2

i of 4, then so does 0!2.

Pro of. We prove this by induction on the length of 4.

(i)If 4is the empty, h;i is the partition of 4. Soclaim holds.

(ii) If 4 denotes (4 0

;B), then 4 0

4 Sub(0;2). Let h5;6i be any partition of 4 0

.

Thenh5;6;Biandh5;B;6iarepartitionsof 4. So0;5!6;B;2and 0;5;B !6;2

have A-suitable pro ofs. Hence A-suitable pro of of 0;5 ! 6;2 can be obtained from

these sequents by means of a cut and weak inferences, since B 2 4 Sub(0;2;A).

Therefore,0!2 has an A-suitableproof by induction hypothesis.

Denition 3.13 (regular) Aproofisregular, ifforanycutintheproofthecutformula

doesn't occur in the lower sequent of the cut.

If the lowersequent of a cut rule contains the cut formula, itis obtainable from one

of the upper sequents by means of weak inferences. So any proof can b e transformed

into regularone. Note that 2 under the discussion is the modality of S5 3

.

Lemma 3.14 Let P bea regular, suitable proof of 0!2. Suppose 2A62Sub(0;2

2A ).

Then 2Adoesn't occur in the antecedent of any sequent of P.

Pro of. Weprovethis byinduction onthe numb erof sequents. Nowassume that2A

occurs in the antecedent of asequent.

Case 1: If 0! 2isthe initialsequent,0!2is 2A!2A. Then 2A2Sub(0). It

is contradictoryto2A62Sub(0;2

2A ).

Case 2: 2Aoccurinthe antecedentsof the upp er sequentsofstructural rules except

cutrule (weakeningrule,contraction ruleandexchangerule)andlogicalrules. Inthese

cases, clearly 2Aoccur inthe antecedentsof the lowersequents of the rules.

Case 3: 2A occurs in at least one of the antecedents of the upper sequents of cut

rule.

(16)

lowersequent.

3.2. If 2Ais the cut formula, then 2Ais the proper subformula of a formula which

occurs in the antecedent of the lowersequentsince P is regularand suitable.

Hence, if 2Aoccurs inthe antecedent of asequent in P, then there exists aformula

B in0 such that 2Ais the proper subformula of B. So 2A2 Sub(B) Sub(0). It is

howevercontradictory to2A62Sub(0;2

2A ).

Denition 3.15 (family) The family of 2A in a suitable proof is the sequence of all

formulas except 2A which occur in the lower sequents of (! 2) in the proof with the

principal formula 2A.

Since the lower sequents of (! 2) consist of 2-formulas, the family of 2A in a

suitable pro ofof 0!2 consistsof 2-formulas inSub(0;2) except 2A.

Denition 3.16 (covered) Let h27

1

;27

2

i be a partition of the family of 2A in a

suitable proof. An application (!2)

25!26;B

25!26;2B

(!2)

in the proof is covered by h7

1

;7

2

;Ai, if 57

1 , 6

A 7

2

and B =A.

Lemma 3.17 Let P be a regular, suitable proof of 0 !2, and h27

1

;27

2

i a partition

of the family of 2A in P. Suppose 2A62Sub(0;2

2A ).

1) If 1!3 is a sequent in P such that no applicationof (!2) which isapplied above

1 ! 3 is covered by h7

1

;7

2

;Ai, then 1;27

1

! 27

2

;3

2A

has an A-suitable proof in

S4 3

N

S5

2 3

.

2)Either27

1

!27

2

;Aor0;27

1

!27

2

;2

2A

hasanA-suitableproofinS4 3

N

S5

2 3

.

Pro of. 1) We prove this by induction on the number of sequents which are ab ove

1! 3.X and X

#

denotethe sequents1!3and 1;27

1

!27

2

;3

2A

respectively. If

X is the lower sequentof weakinferences, (^!), (!^), (_!), (!_),(!), (!),

(:!) or (!:), the conclusion follows fromthe induction hyp othesis immediately. So

we will mention the other cases.

Case 1: X is the initial sequent B ! B. Since B 6= 2A by Lemma 3.14, X

#

(i.e.

B;27

1

!27

2

;B)has a suitableproof.

(17)

5

1

!6

1

;B B;5

2

!6

2

5

1

;5

2

!6

1

;6

2

(acceptable cut);

where B 2Sub(5

1

;5

2

;6

1

;6

2

). By the induction hypothesis, 5

1

;27

1

!27

2

;6

12A

;B

and B;5

2

;27

1

!27

2

;6

22A

haveA-suitable proofs.

If B 2 Sub(2A) ( i.e. B 2 Sub(A)[f2Ag ), then B 2 Sub(A) since B 6= 2A by

Lemma 3.14. Inthis case,

5

1

;27

1

!27

2

;6

12A

;B B;5

2

;27

1

!27

2

;6

22A

5

1

;5

2

;27

1

;27

1

!27

2

;27

2

;6

12A

;6

22A

(cut)

5

1

;5

2

;27

1

!27

2

;6

12A

;6

22A

(weak inferences) 1111(＊⁾

is anA-suitable proof.

If B 62Sub(2A),then B 2Sub(5

1

;5

2

;6

12A

;6

22A

).So (＊⁾ ^is^a ^suitable^proof.

Case 3: X isthe lowersequent of an

25!26;B

25!26;2B

(!2) :

If B = A, then X

#

is 25;27

1

! 27

2

;2(6

A

). By the assumption this inference

is not covered by h7

1

;7

2

;Ai. So either 5\7

2

6= or 6

A

\7

1

6= .In both cases, a

suitable pro ofof X

#

can beobtained by means of weakeningrules.

If B 6= A, then X

#

is 25;27

1

! 27

2

;2(6

A

);2B . By induction hyp othesis,

25;27

1

!27

2

;2(6

A

);B has an A-suitable pro of, and in the case of B =2A, ithas

anA-suitable proof by means of weakeningrule. Hence X

#

has anA-suitable proof.

Case 4: X isthe lowersequent of an

5 !B

5! B

(! ) :

Since B is -formula, then B

2A

is B. So X

#

is 5;27

1

!27

2

; B. Hence an

A-suitable pro ofof X

#

can be obtained bymeans of weak inferences.

2) Case 1 : Some application of (! 2) is covered by h7

1

;7

2

;Ai. Take one of the

uppermostsuch application

25!26;A

25!26;2A

(!2) ;

(18)

1 A 2

can obtain 25;27

1

!27

2

;2(6

A

);A. So27

1

!27

2

;A has anA-suitable proof.

Case 2 : Otherwise. Byapplying 1)to the end-sequent,wecan obtainanA-suitable

proof of 0;27

1

!27

2

;2

2A .

Corollary 3.18 If 0 ! 2 has a suitable proof in S4 3

N

S5

2 3

, then 0 ! 2

2A

;A has

an A-suitable one.

Pro of. Let P b ea regular,suitable proof of 0!2.

(i)If 2A2Sub(0;2

2A

), 0!2

2A

;A has the suitable proof :

0!2

A!A

2A!A

0!2

2A

;A

(acceptable cut):

(ii) 2A62Sub(0;2

2A

). Let 4 be the family of 2A in P, and h27

1

;27

2

i any partition

of 4. Then either 27

1

! 27

2

;A or 0;27

1

! 27

2

;2

2A

has an A-suitable pro of by

Lemma3.17 ,and sotoohas 0;27

1

!27

2

;2

2A

;Abymeansof weakinferences. Thus

0!2

2A

;A has anA-suitable one by Lemma3.12.

Proof of Theorem 3.9 for S4 3

N

S5

2 3

. We rst replaced all unacceptable cuts by

mixes, andshowitbydoubleinductiononthedegreeandtherankthatanyproofwitha

mixfor itslowestinference and not containingany other mixcan be transformed intoa

suitableone withoutchangingthe end-sequent. Byeliminating oneof uppermostsucha

mixesinturn,allmixescanbeeliminated. Inparticular wewill mentionthecases which

the upper sequentsof the mixesare the lowersequents of (2 !);(!2);( !);(! )

and (acceptabl e cut), since the other cases can b eproved inusual way by the induction

hyp othesis immediately.

Case 1 : =2.

1.1. The left and right upp er sequents of the mix are the lower sequents of (! 2)

and (2!) respectively. Then the pro of runs as follows:

20!22;A

20!22;2A

(!2)

A;1!6

2A;1!6

(2!)

20;1!22;6

(2A) ;

where 2Ais the mix formulaand 2A6222[1. Wetransform itintothe proof :

(19)

20!22;6

(A) :

The degree of A is smaller than that of 2A. Hence we can eliminate the mix by the

hyp othesis ofinduction onthe degree.

1.2. The left and right upper sequents of the mix are the lower sequents of (! )

and ( !)respectively. Then the proof runs as follows :

0!A

0! A

(! )

A;1!6

( !)

0!6

( A) ;

where A is the mix formula and A621. We transformit intothe pro of:

0!A A;1!6

0;1!6

(A) :

The degree of A is smaller than that of A. Hence we can eliminate the mix by the

hyp othesis ofinduction onthe degree.

Case 2 : ＞^2.

Subcase 2.1:

r

=1. In this case

l＞¹^since ＞² ^and ^r ⁼^1.

2.1.1. The right upper sequent of the mix is the lower sequent of (2 !). Then the

proof runs as follows:

0!2

A;1!6

2A;1! 6

(2!)

0;1!2

2A

;6

(2A) ;

where2Aisthemixformula,2A22and2A621. Since0!2

2A

;AhasanA-suitable

proof byCorollary 3.18, we can construct the pro of :

0!2

2A

;A A;1!6

0;1

A

!(2

2A )

A

;6

(A)

0;1!2

2A

;6

(w :i:) :

Even if mixes appear in a proof of 0 ! 2

2A

;A, all the mix formulas are subformulas

of A. Since the degreeof A is smallerthan that of 2A, the mixescan beeliminated by

the hyp othesis of induction on the degree. In the similar way, the mix which is lowest

(20)

suitable pro ofcan beobtained withoutexchanging the end-sequent.

2.1.2. The left and right upp er sequents of the mix are the lower sequents of (2!)

and ( !)respectively. Then the proof runs as follows :

A;0!2

2A;0!2

(2!)

B;1!6

( !)

2A;0;1!2

B

;6

( B) ;

where B is the mix formula, B 22and B 62 1. Wetransformit into the pro of :

A;0!2

B;1!6

( !)

A;0;1!2

B

;6

( B)

2A;0;1!2

B

;6

(2!) :

Theleftrankofthispro ofissmallerthanthatoftheformerone. Hencewecaneliminate

the mix bythe hyp othesis of induction on the rank.

2.1.3. The left and rightupper sequents of the mix are the lower sequentsof ( !)

and (! ) resp ectively. Then the pro of runs as follows:

A;0!2

( !)

B;1!6

( !)

A;0;1!2

B

;6

( B) ;

where B is the mix formula, B 22and B 62 1. Wetransformit into the pro of :

A;0!2

B;1!6

( !)

A;0;1!2

B

;6

( B)

A;0;1!2

B

;6

( !) :

Subcase 2.2:

r＞^1.

2.2.1. The both upper sequents of the mix are the lower sequents of (! 2). Then

the pro of runs as follows:

20 !22

21!23;B

21!23;2B

(!2)

20;2(1

A

)!2(2

A

);23;2B

(2A) ;

(21)

20! 22 21!23;B

20;2(1

A

)!2(2

A

);23;B (2A)

20;2(1

A

)!2(2

A

);23;2B

(!2) :

The right rank of this proof is smaller than that of the former one. Hence we can

eliminate the mix by the hyp othesis of induction onthe rank.

and (!2) respectively. Then the pro of runs as follows:

A;0!2

2A;0!2

(2!)

21!23;B

21!23;2B

(!2)

2A;0;2(1

C

)!2

2C

;23;2B

(2C) ;

where 2C is the mixformula and 2C 22\21. We transformit intothe proof :

A;0!2

21!23;B

21 !23;2B

(!2)

A;0;2(1

C )!2

2C

;23;2B (2C)

2A;0;2(1

C )!2

2C

;23;2B

(2!) :

and (!2) respectively. Then the pro of runs as follows:

A;0!2

( !)

21!23;B

21!23;2B

(!2)

A;0;2(1

C

)!2

2C

;23;2B

(2C) ;

where 2C is the mixformula and 2C 22\21. We transformit intothe proof :

A;0!2

21!23;B

21!23;2B

(!2)

A;0;2(1

C )!2

2C

;23;2B (2C)

A;0;2(1

C )!2

2C

;23;2B

( !) :

The left rank of this proof is smaller than that of former one. Hence we can eliminate

and (! ) resp ectively.

(22)

2A;0!2

(2!)

1!B

1! B

(! )

2A;0; (1

C )!2

C

; B

( C) ;

where C is the mix formula and C22\21. Wetransform itintothe proof :

A;0!2

1!B

1! B

(! )

A;0; (1

C )!2

C

; B ( C)

2A;0; (1

C

)!2

C

; B

(2!) :

and (! ) resp ectively. Then the pro of runs as follows:

A;0!2

( !)

1!B

1! B

(! )

A;0; (1

C )!2

C

; B

( C) ;

where C is the mix formula and C22\21. Wetransform itintothe proof :

A;0!2

1!B

1! B

(! )

A;0; (1

C )!2

C

; B ( C)

A;0; (1

C

)!2

C

; B

( !) :

Case 3 : If the right upper sequent of the mix is the lowersequent of acceptable cut in

particular, then the proof runs as follows:

5!6

0!2;B B;1!3

0;1!2;3

(acceptablecut)

5;0

A

;1

A

!6

A

;2;3

(A) ;

where A is the mix formula and A 2 (0;1)\6. Since B is the cut formula of the

acceptable cut, B 2 Sub(0;1;2;3). Suppose A 2 1 but A 62 0, since other cases are

shown likewise.

3.1. If B 2Sub(A)nfAg, we transformthe given pro ofintothe pro of :

(23)

0!2;B 5;B;1

A

!6

A

;3 (A)

5;0

A

;1

A

!2;6

A

;3

(B) ;

Hence we can eliminate the upp er mix by the hyp othesis of induction on the rank and

the lowermix bythe hyp othesis of induction onthe degree since deg(B)＜^deg(A).

3.2. If B A, we transform the given proof intothe proof :

5!6 B;1!3

5;1

A

!6

A

;3

(A)

5;0

A

;1

A

!6

A

;2;3

(w:i:) :

Hence wecan eliminate the mixby the hyp othesis of induction on the rank.

3.3. If B 62Sub(A), we transformthe given proof into the proof :

0!2;B

5!6 B;1!3

5;B;1

A

!6

A

;3 (A)

5;0

A

;1

A

!2;6

A

;3

(acceptabl e cut) ;

where B 2 Sub(0

A

;1

A

;2;3). Hence we can eliminate the mix by the hypothesis

of induction on the rank, and the lowest inference is an acceptable cut since B 2

Sub(0

A

;1

A

;2;3).

Corollary 3.18 must bemodied as follows:

Corollary 3.19 If 0 ! 2 has an suitable proof in S5 3

N

S5 3

, then 0 ! 2

2A

;A and

0!2

A

;A respectively have A-suitable proofsin S5 3

N

S5 3

.

Proof of Theorem 3.9 for S5 3

N

S5 3

. We rst replaced all unacceptable cut by

mixes, andshowthe theorem forS5 3

N

S5 3

bydoubleinduction onthedegree andrank

that any pro of with a mixfor its lowermost inferenceand not containingany other mix

can b e transformed into a suitable one with the same end-sequent. By eliminating one

of uppermost such a mixes in turn, all mixes can be eliminated. We will particularly

mention onlycrucial cases.

Case 1: Therightuppersequentof the mix isthe lowersequent of(!2). Then the

0!2

A;1!6

2A;1! 6

(2!)

0;1!2

2A

;6

(2A) ;

(24)

2A

proof byCorollary 3.19, we can construct the pro of:

0!2

2A

;A A;1!6

0;1

A

!(2

2A )

A

;6

(A)

0;1!2

2A

;6

(w :i:) :

2A

of A. Since the degreeof A is smallerthan that of 2A, the mixescan beeliminated by

inference can be also eliminated by the hyp othesis of induction onthe degree. Hence a

suitable pro ofcan beobtained withoutchanging the end-sequent.

Case 2: The rightuppersequentof the mix isthe lowersequent of( !). Then the

0!2

A;1!6

( !)

0;1!2

A

;6

( !) ;

where Aisthemixformula, A 22and A621. Since0!2

A

;AhasanA-suitable

proof byCorollary 3.19, we can construct the pro of:

0!2

A

;A A;1!6

0;1

A

!(2

A )

A

;6

(A)

0;1!2

A

;6

(w:i:) :

A

of A. Since the degreeof A issmaller than that of A, the mixescan beeliminated by

inference can be also eliminated by the hyp othesis of induction onthe degree. Hence a

suitable pro ofcan beobtained withoutchanging the end-sequent.

As for K 3

N

S5 3

and KT 3

N

S5 3

,subformula property can be seen ina similar way

to S4 3

N

S5 3

. Thus, we havethe following.

Corollary 3.20 (subformula property)

Then all formulas which construct suitable proof in K 3

N

S5 3

, KT 3

N

S5 3

, S4 3

N

S5 3

or S5 3

N

S5 3

consist of the subformulas of formulas which occur in the lowest sequent.

(25)

ofthesubformulasofformulasinthelowersequents.Intheacceptablecutrule,ofcourse,

the upp er sequents of the inferences consist of the subformulas of formulas inthe lower

sequent.

3.4 Decidability

Asanapplicationofsubformulapropertywhichwasseenintheprevioussection,wewill

seethe decidabilityforthe systemscorrespondingtofusions. Aconcreteniteprocedure

which decides to be provable or not for any formula in a system is called a decision

procedure. If there existsa decision pro cedure, the system is side to b e decidable.

Denition 3.21 (reduced) A sequent 0 ! 1 is reduced, if each formula occurs at

most three times in both 0 and 1.

Lemma 3.22 Let 0 !1 be arbitrary sequent. Then there exists a suitable S4 3

N

S5 3

proof of 0 0

!1 0

which consists solely of reduced sequents such that 0 0

!1 0

is provable

in S4 3

N

S5 3

if and only if 0!1 is provablein S4 3

N

S5 3

.

Pro of. Suppose 0 ! 1 is not reduced. Then a reduced sequent 0 0

! 1 0

can be

obtained from0 !1 by meansof contraction and exchange rules. Conversely, 0!1

can be obtained from 0 0

! 1 0

by means of weakening and exchange rules. So, for any

sequent 0 ! 1, there existsa reduced sequent 0 0

! 1 0

such that 0 0

! 1 0

is provable

in S4 3

N

S5 3

if and only if 0 ! 1 is provable in S4 3

N

S5 3

. Then we can obtained a

suitable pro ofof reduced sequent0 0

!1 0

byTheorem 3.9.

The sequences 0, 1, 5 and 6 of formulas in the structural and logical rules of

S4 3

N

S5 3

,respectively,arenotabletocontaintwoormoresameformulasbydeletingthe

overlappingformulas. Thenbymeansofweakinferencesandbydeletingthenonessential

sequents, we can obtain the suitable proof of 0 0

! 1 0

which consists solely of reduced

sequents.

Theorem 3.23 S4 3

N

S5 3

isdecidable.

Pro of. We will showthis theorem by giving adecision procedure. Supposethat any

sequent0!1is given. ByLemma3.22 it isprovablein S4 3

N

S5 3

if and onlyif there

existsa reducedsequent0 0

!1 0

obtained from0!1whichisprovable inS4 3

N

S5 3

.

LetG bethe setof allthe reduced sequentswhichconsist ofall formulasinSub(0 0

;1 0

).

Since the setSub(0 0

;1 0

) is nite, the setG is nite. Nowwedene G

n

asfollows:

(26)

0

G

i+1

is the union of G

i

and the set of all the sequentsin GnG

i

which can b e lower

sequentswhen upp er sequentsare in G

i .

Then there existsj suchthat G

j+1

=G

j

since the setG is nite. If the sequent 0 0

!1 0

is in G

j

, then 0 0

! 1 0

is provable in S4 3

N

S5 3

, viz. 0 !1 is provable in S4 3

N

S5 3

.

Otherwise, 0!1is not provable in S4 3

N

S5 3

.

Similarly,wecan show the following.

Theorem 3.24 For any M 3

;N 3

2fK 3

;KT 3

;S4 3

;S5 3

g, M N

N is decidable.

3.5 Craig's interpolation theorem

In this section, Craig's interp olation theorem for various fusions is shown syntactically

by using Maehara's method. Since, for any M 3

;N 3

2 fK 3

;KT 3

;S4 3

g, M 3

N

N 3

has

cut-elimination property by Theorem 3.3, Craig's interpolation theorem for M 3

N

N 3

can be shown by using the usual way. Also, even when at least one of M 3

and N 3

is

S5 3

, we can use Maehara,smethodand get Craig'sinterp olation theorem forM 3

N

N 3

.

In the following,wewill givena detailed proof of itfor S4 3

N

S5 3

.

For technical reasons, we introduce the constant symbol >, and admit ! > as an

initial sequent.

Denition 3.25 (partition of sequence)

hf0

1

;1

1 g;f0

2

;1

2

gi is a partition of sequent 0 ! 1, if 0

1

\ 0

2

= , 0

1 [ 0

2

= 0,

1

1 [1

2

= and 1

1 [1

2

=1.

ThesetofallpropositionalvariableswhichoccurinAandconstantsymb olisdenoted

by V(A).

Lemma 3.26 Suppose that a sequent 0!1 is provable in S4 3

N

S5

2 3

, andalso that

hf0

1

;1

1 g;f0

2

;1

2

gi is an arbitrarypartitionof 0!1. Then there exists a formula C,

calledan interpolant, such that

1) 0

1

!1

1

;C and C ;0

2

!1

2

are bothprovable in S4 3

N

S5

2 3

,

2) V(C)V(0

1 [1

1

)\V(0

2 [1

2 ).

Pro of. This lemma is provedby induction on the length a suitableproof of 0!1.

Wewill give a proof onlythe cases where 0!1 is initial sequentor the lowersequent

of one of (2!), (!2), ( !), (! ) and (acceptable cut).

(27)

hf;g;fD;Dgi, hfD;g;f;Dgi and hf;Dg;fD;gi as the partitions. Then :>, >, D and

:D are servesas the interpolants,respectively.

Case 2. The last inference is

A;0!1

2A;0!1

(2!) :

2.1. The partition ishf2A;0

1

;1

1 g;f0

2

;1

2

gi. Byapplyingthe inductionhypothesis

totheproofof theuppersequent,thereexistsaninterp olantC suchthatA;0

1

!1

1

;C

and C ;0

2

! 1

2

are both provable in S4 3

N

S5

2 3

. Then we can obtain following two

proofs:

.

A;0

1

!1

1

;C

2A;0

1

!1

1

;C

.

C ;0

2

!1

2 :

Hence C serves asan interpolantof the presentpartition.

2.2. The partition ishf0

1

;1

1

g;f2A;0

2

;1

2

to the proof of the upp er sequent, there exists an interp olant C such that 0

1

! 1

1

;C

andC ;A;0

2

!1

2

arebothprovableinS4 3

N

S5

2 3

. Thenwecan obtainfollowingtwo

proofs:

.

0

1

!1

1

;C

.

C ;A;0

2

!1

2

C ;2A;0

2

!1

2 :

20!21;A

20!21;2A

(!2) :

3.1. The partition is hf20

1

;21

1

;2Ag;f20

2

;21

2

gi. By applying the induction

hyp othesis to the proof of the upper sequent, there exists an interp olant C such that

20

1

!21

1

;A;C and C ;20

2

!21

2

are b oth provable inS4 3

N

S5

2 3

. Then we can

obtain following twopro ofs:

(28)

.

20

1

!21

1

;A;C

:C ;20

1

!21

1

;A

2:C ;20

1

!21

1

;A

2:C;20

1

!21

1

;2A

20

1

!21

1

;2A;:2:C

.

C ;20

2

!21

2

20

2

!21

2

;:C

20

2

!21

2

;2:C

:2:C ;20

2

!21

2 :

Hence :2:C servesas aninterpolantof the presentpartition.

3.2. The partition is hf20

1

;21

1

g;f20

2

;21

2

;2Agi. By applying the induction

hyp othesis to the proof of the upper sequent, there exists an interp olant C such that

20

1

! 21

1

;C and C ;20

2

! 21

2

;2A are both provable in S4 3

N

S5

2 3

. Then we

can obtain followingtwoproofs:

.

20

1

!21

1

;C

20

1

!21

1

;2C

.

C ;20

2

!21

2

;A

2C ;20

2

!21

2

;A

2C ;20

2

!21

2

;2A :

Hence 2C servesas aninterpolantof the present partition.

A;0!1

( !) :

4.1. The partitionis hf A;0

1

;1

1 g;f0

2

;1

2

totheproofof theuppersequent,thereexistsaninterp olantC suchthatA;0

1

!1

1

;C

and C ;0

2

! 1

2

are both provable in S4 3

N

S5

2 3

. Then we can obtain following two

proofs:

.

A;0

1

!1

1

;C

A;0

1

!1

1

;C

.

C ;0

2

!1

2 :

4.2. The partitionis hf0

1

;1

1

g;f A;0

2

;1

2

to the proof of the upp er sequent, there exists an interp olant C such that 0

1

! 1

1

;C

andC ;A;0

2

!1

2

arebothprovableinS4 3

N

S5

2 3

. Thenwecan obtainfollowingtwo

proofs:

(29)

.

0

1

!1

1

;C

.

C ;A;0

2

!1

2

C ; A;0

2

!1

2 :

0!A

0! A

(! ) :

5.1. The partition is hf 0

1

; Ag;f 0

2

;gi. Byapplying the induction hypothesisto

the proofof the uppersequent, thereexistsaninterp olantC suchthat 0

1

!A;C and

C ; 0

2

!are both provable in S4 3

N

S5

2 3

. Then we can obtain following two proofs:

.

0

1

!A;C

:C ; 0

1

!A

:C ; 0

1

!A

:C ; 0

1

! A

0

1

! A;: :C

.

C ; 0

2

!

0

2

!:C

0

2

! :C

: :C; 0

2

! :

Hence : :C servesas aninterp olantof the present partition.

5.2. The partition is hf 0

1

;g;f 0

2

;Agi. By applying the induction hyp othesis to

the proof of the upper sequent, there exists an interp olant C such that 0

1

! C and

C ; 0

2

!AarebothprovableinS4 3

N

S5

2 3

. Thenwecanobtainfollowingtwopro ofs:

.

0

1

!C

0

1

! C

.

C ; 0

2

!A

C; 0

2

!A

C ; 0

2

! A

:

Hence C servesas aninterpolant of the presentpartition.

0!1;A A;5! 6

0;5!1;6

(acceptable cut) ;

where A 2 Sub(0;5;1;6). Then the partition is hf0

1

;5

1

;1

1

;6

1 g;f0

2

;5

2

;1

2

;6

2 gi.

This is onlythe case whichnever happens whenthe cut-elimination theorem holds.

(30)

1 1 1 1

of the upp er sequent, there exist interp olants C

1

and C

2

such that 0

1

! 1

1

;A;C

1

;

C

1

;0

2

! 1

2

; A;5

1

! 6

1

;C

2

and C

2

;5

2

! 6

2

are all provable in S4 3

N

S5

2 3

. Then

we can obtain following two proofs:

.

0

1

!1

1

;A;C

1

.

A;5

1

!6

1

;C

2

0

1

;5

1

!1

1

;6

1

;C

1

;C

2

0

1

;5

1

!1

1

;6

1

;C

1 _C

2

;C

1 _C

2

0

1

;5

1

!1

1

;6

1

;C

1 _C

2

.

C

1

;0

2

!1

2

C

1

;0

2

;5

2

!1

2

;6

2

.

C

2

;5

2

!6

2

C

2

;0

2

;5

2

!1

2

;6

2

C

1 _C

2

;0

2

;5

2

!1

2

;6

2

:

Hence C

1 _C

2

servesas interp olantsof the presentpartition.

6.2. If A2Sub(0

2

;5

2

;1

2

;6

2

),byapplying the induction hyp othesisto the proof of

the upper sequent,there existinterp olantsC

1

and C

2

suchthat 0

1

!1

1

;C

1

; C

1

;0

2

!

1

2

;A; 5

1

! 6

1

;C

2

and C

2

;A;5

2

! 6

2

are all provable in S4 3

N

S5

2 3

. Then we can

obtain following twopro ofs:

.

0

1

!1

1

;C

1

0

1

;5

1

!1

1

;6

1

;C

1

.

5

1

!6

1

;C

2

0

1

;5

1

!1

1

;6

1

;C

2

0

1

;5

1

!1

1

;6

1

;C

1

^C

2

.

C

1

;0

2

!1

2

;A

.

C

2

;A;5

2

!6

2

C

1

;0

2

;C

2

;5

2

!1

2

;6

2

C

1

^C

2

;0

2

;C

1

^C

2

;5

2

!1

2

;6

2

C

1

^C

2

;0

2

;5

2

!1

2

;6

2

:

Hence C

1

^C

2

servesas interp olantsof the presentpartition.

Theorem 3.27 (Craig's interp olation theorem)

If A B is provablein S4 3

N

S5 3

, then there existsa formula C such that

1) AC and C B are bothprovable in S4 3

N

S5 3

,

2) V(C)V(A)\V(B).

Pro of. Assume that AB is provablein S4 3

N

S5 3

. Clearly,the sequent A!B is

provableinit. Thenby Lemma3.26,taking Aas0

1

and B as1

2

,there existsa formula

C satisfying 1) and 2) of Theorem 3.27.

Similarly,wecan show the following.

Theorem 3.28 Let M 3

;2 fK 3

;KT 3

;S5 3

g. If A B is provable in M 3

N

S5 3

, then

there exists a formula C such that

1) AC and C B are bothprovable in M 3

N

S5 3

,

2) V(C)V(A)\V(B).

(31)

As for fusions, M. Krachtand F. Wolter [3]proved the followings semantically:

both Mand Nare decidable ) M N

N is decidable,

both Mand Nhold the Craig'sinterp olationtheorem ) M N

N holds it.

Inthischapter,we obtainedthesyntacticalresultsfortheseproperty. ForanyM 3

;N 3

2

fK 3

;KT 3

;S4 3

;S5 3

g, we could see that M 3

N

N 3

has subformula property either by

derivingthecut-elimination prop ertyorby showingthat everypro ofcanbetransformed

intosuitableonewithsame end-sequent. Ineithercase, importantlogicalproperties like

the decidability and the Craig's interp olation theorem can b e derived.

As for dependently axiomatizable bimodal logics, however, it is dicult to nd se-

quentsystemsinwhichthecut-eliminationpropertyholds. Therefore,itwouldbeneces-

sarytodevelopsemanticalmethodsfor them. Someattempts tothisdirection are made

in the nextsection.

(32)

Kripke type semantics

Thereareseveralsemanticalresearchesonfusionofindependentlyaxiomatizablebimodal

logics by M. Kracht and F. Wolter [3] and soon, and some syntacticalapproaches have

been seen in previous section. In this chapter, we will examine several dependently

axiomatizable bimodal logics, using semantical method. Using Kripke typ e semantics,

logicalpropertieslikethe completenessand thenitemodelpropertyfortheselogicswill

be discussed. Thoughour studyinthe presentchapterremainsstill aninitial stage,the

attempt made here will contribute tofuture extensive,semanticalstudy infuture.

4.1 Kripke frames and models

First we will extend Kripketyp e semantics tobimodal logics.

Denition 4.1 (Kripke frame)

Let M be a nonempty set, and R

2

and R be binary relations onM; viz. R

2

M 2M

and R M 2M. Then a frame is a triple (M;R

2

;R ), where M is called the set of

possible worlds, and bothR

2

and R are called accessibility relations.

Denition 4.2 (Kripke model)

Let F = (M;R

2

;R ) be a frame, and V be a mapping such that V(p) M for each

propositional variable p. Then a Kripke model is a pair (F;V), i.e. (M;R

2

;R ;V),

whereV is called a valuation on F. For a given Kripke model (M;R

2

;R ;V), a binary

relationj= betweena 2M and formulas is dened inductively on the length of formulas

as follows:

aj=p()a2V(p)

(33)

aj=A_B ()aj=A or aj=B

aj=AB ()aj=A implies aj=B

aj=:A() not aj=A

aj=2A() for any b 2M, aR

2

b implies bj=A

aj= A() for any b2M, aR b implies b j=A.

The relationj=is dened by the valuation V uniquely. So j= and (M;R

2

;R ;j=) is

also calleda valuation,and a Kripkemodel, resp ectively,when noconfusionswilloccur.

A formula A is true in model M = (M;R

2

;R ;j=), denoted by M j= A, if a j= A for

any a 2 M. A formula A is valid in frame F = (M;R

2

;R ), denoted by F j= A, if

Mj=A for any model M=(M;R

2

;R ;j=).

Inthefollowing,wewillconsiderparticularinterdep endencesb etween2and ,which

canbeexpressedbyaformulaoftheform

1 111

m p

1 111

n

p,where

i

;

j

2f2; g.

An example is 2p p, which can be interpreted in epistemic logic as H knows

everythingwhat H

2

knows when 2p ( p)is interpreted as H

2

(H )knows p .

Lemma 4.3 Let

i

;

j

2 f2; g. Suppose m;n 1. For any frame F =(M;R

2

;R ),

F j=

1 111

m

A

1 111

n

A ()

(33) 8c

k

(0k n01) (c

k R

k+1 c

k +1 ) 9d

l

(0lm01) d

l R

l+1 d

l+1 ),

where c

0

=d

0

=a and c

n

=d

m

=b.

Pro of. [(] Let(M;R

2

;R ;j=) be a mo del,and a be inM.

a6j=

1

2 111

n01

n A

) 9e

1 (aR

1 e

1 and e

1 6j=

2 111

n A)

.

) 9e

1 1119e

n01 (aR

1 e

1

;111;e

n02 R

n01 e

n01 and e

n01 6j=

n A)

) 9e

1 1119e

n01 9e

n (aR

1 e

1

;111;e

n02 R

n01 e

n01

;e

n01 R

n e

n and e

n 6j=A)

) 9d

1 1119d

m01 9d

m (aR

1 d

1

;111;d

m02 R

m01 d

m01

;d

m01 R

m d

m and d

m

6j=A) (e

n

=d

m )

) 9d

1 1119d

m01 (aR

1 d

1

;111;d

m02 R

m01 d

m01 and d

m01 6j=

m A)

.

) 9d

1 (aR

1 d

1 and d

1 6j=

2 111

m A)

) a6j=

1

2 111

m01

m A

[)] Supposec

k R

k+1 c

k +1

for any c

k +1

(0kn01), wherec

0

=a and c

n

=b. Let

(M;R

2

;R ;j=) bea model in which

(34)

l l

l+1 l+1

whered

0

=aandd

m

=x. Thenaj=

1 111

m

p,andsoa j=

1 111

n

pbytheassumption.

Since, for any c

k

(0 k n01), c

k R

k +1 c

k +1

and a j=

1 111

n p, c

n

j=p (i:e: b j=p).

Hence 9d

l

(0l m01);d

l R

l+1 d

l+1

where d

0

=a and d

m

=b.

The condition inLemma 4.3 corresponding tothe schema

1 111

m

A

1 111

n A is

displayed by the followingFigure 4.1.

a

c

1

c

2

c

n02

c

n01

d

1

d

2

d

m02

d

m01

b

3

Q

Q s

Q

Qs Q

Q

Qs Q

Q

Qs Q

Q

Qs Q

Q

Qs

3 -

- - -

- - - -

- -

R

1

R

2

R

n01

R

n

R

1

R

2

R

m01

R

m

Figure 4.1:

4.2 Completeness

We will see Kripke completeness for the bimodal logics with the axiom

1 111

m p

1 111

n

p where

i

;

j

2f2; g byusing the canonicalmodels.

In the following, 8denotes the setof all formulas of bimodal logics.

Denition 4.4 ( L-consistent set ) For a bimodal logic L, a set U 28 is L- consis-

tent if :(B

0

^B

1

^111^B

n01

)62L for any B

0

;111;B

n01 2U.

Denition 4.5 ( L-maximal set ) For a bimodal logic L, a set U 28 isL- maximal

is the following conditions are satised:

U isL-consistent,

for any A28, either A2U or :A2U.

Lemma 4.6 Let L be a normal logic.

(1) (A

0

^111^A

n01

)A2L

) (2A

0

^111^2A

n01

)2A2L and ( A

0

^111^ A

n01

) A2L.

(2) (2A

0

_111_2A

n01

)2(A

0

_111_A

n01 )2L,

( A

0

_111_ A

n01

) (A

0

_111_A

n01 )2L.

(35)

0

andthen2(A

0

A)2L. SinceLisnormal,2A

0

2A2L. If(A

0

^111^A

k

)A2L,

then(A

0

^111^A

k 01

)(A

k

A)2L. Byinductionhyp othesis, (2A

0

^111^2A

k 01 )

2(A

k

A) 2 L. Since L is normal, (2A

0

^111^2A

k 01

) (2A

k

2A) 2 L. Hence

(2A

0

^111^2A

k

)2A2L. Asfor , wecan seein the similarway to 2.

(2) By induction on n. The case n = 0 is clearly. Suppose the case n = k 01,

and then (2A

0

_ 111_ 2A

k 01

) 2(A

0

_ 111 _A

k 01

) 2 L. (2A

0

_111 _2A

k 01 )

2(A

0

_111_A

k 01 _A

k

)2Lsince(A

0

_111_A

k01

)(A

0

_111_A

k 01 _A

k

)2L. Further,

A

k (A

0

_111_A

k 01 _A

k

) 2 L, and so 2A

k

2(A

0

_111_A

k 01 _A

k

) 2 L. Thus

(2A

0

_111_2A

k 01 _2A

k

)2(A

0

_111_A

k 01 _A

k

)2L. Asfor ,wecan seein the

similar way to 2.

The following lemmais essentialinproving the completeness.

Lemma 4.7 ( Lindenbaum's lemma )

Every L-consistent set of formulas iscontained in a L-maximal set.

Pro of. LetA

0

;111;A

i

;111b eanenumerationofthe set8,andU be anyL-consistent

set. Nowdene as follows:

0

=U

n+1

= 8

<

:

n [fA

n

g; if

n [fA

n

g isL-consistent;

n

[f:A

n

g; otherwise:

= S

n0

n .

By using induction, we will show that

n

is L -consistent for any n. Clearly,

0 is L-

consistent. Nextassumethat

n

isL-consistent. If

n [fA

n

gisL-consistent,then

n+1

is L-consistentby the denition of

n

. Nowconsiderthe case that

n [fA

n

g is not L-

consistent,i.e. thereexistB

1

;111;B

k 2

n

suchthat:(B

1

^111^B

k

^A

n

)2 L. Suppose

moreoverthat

n+1 (=

n [f:A

n

g)isnotL-consistent. ThenthereexistC

1

;111;C

l 2

n

suchthat :(C

1

^111^C

l

^(:A

n

))2L. Hence C

1

^111^C

l

:(B

1

^111^B

k

)2L, i.e.

:(C

1

^111^C

l

^B

1

^111^B

k

)2L. Butthis contradictsthe L-consistency of

n

. Next,

we willshow that isL-consistent. Supposeotherwise. Then,:(D

1

^111^D

s

)2L for

some D

1

;111;D

s

2 . Since = S

n

n , D

i 2

n

for each i. Let N be the maximum

numb er in fn

1

;111;n

s

g. Then, D

i 2

N

for all i. This means that

N

is inconsistent.

But this is acontradiction.

It remainstoshowthat eitherA2or:A2foreachA28. SupposeA2and

:A 2 for some formula A. Since :(A^:A) 2 L, this contradictsthe L-consistency

of . So exactlyone ofA and :Amust be in for any A28.