Corollary 5.6.1. The empty sequent ⇒ cannot be derived inGIntPAL+.
Proof. Suppose for contradiction thatGIntPAL+⊢ ⇒. By Theorem 5.6.1,GIntPAL⊢ ⇒ is obtained. However, there is no inference rule inGIntPALwhich can derive the
empty sequent. A contradiction. □
where we note thatV¬p(p)=∅. Then we consider a particular instance of (R→):4 x:¬pp⇒x:¬p⊥
⇒x:¬p¬p (R→)
We show that the uppersequent is s-valid inMbut the lowersequent is not s-valid in M, and so (R→) does not preserves-validity in this case. Note thatw0does not survive after¬p, i.e.,w0 <D(M¬p)={w2}. We also note that the semantic clause for→at a statewbecomes classical whenwis a single reflexive point.
First, we show thatx:¬pp⇒iss-valid inM, i.e.,M,f ⊮x:¬ppfor any assignment f :Var→ D(M). So, we fix any f :Var→ D(M). We divide our argument into: f(x)
=w1or f(x)=w2. Iff(x)=w1,f(x) does not survive after¬p, and soM,f ⊮x:¬ppby Proposition 5.7.1. If f(x)=w2, f(x) survives after¬pbut f(x)<V¬p(p)(=∅), which impliesM¬p,f(x) ⊮ phenceM,f ⊮ x:¬ppby Proposition 5.7.1. Therefore, in either case, the uppersequent is valid.
Second, we show that⇒ x:¬p¬pis nots-valid inM, i.e.,M,f ⊮x:¬p¬pfor some assignment f :Var→ W. We fix some f such that f(x)=w1. Since f(x)<D(M¬p) (f(x) does not survive after¬p),M,f ⊮x:p¬pby Proposition 5.7.1, as desired. □ Proposition 5.7.2 is a counter-example of the soundness theorem withs-validity, and so it forces us to change the definition of validity, A key idea of finding another candidate here is that we readΓ⇒∆as ‘it is impossible that all ofΓhold and all of∆fail.’ We define the notion of failure for the labelled expressions explicitly by requiring survival of states as follows (we read ‘M,f ⊩ A’ by ‘labelled expressionAfails underMand
f’).
Definition 5.7.3. LetMbe anIntK-model andf :Var→ D(M) an assignment.
M,f ⊩x:αA iff Mα,f(x)⊮Aand f(x)∈ D(Mα), M,f ⊩xRϵay iff (f(x),f(y))<Ra,
M,f ⊩xRα,aAy iff M,f ⊩xRαayorM,f ⊩x:αAorM,f ⊩y:αA.
Note that the first item means that f(x) survives at the domain of the restricted modelMαandAis false at the survived world f(x) inMα.
Definition 5.7.4(t-validity). Γ⇒∆ist-validinMif there is no assignmentf :Var→ D(M) such thatM,f ⊩Afor allA∈Γ, andM,f ⊩Bfor allB∈∆.
Let us denote byVar(Γ ⇒ ∆) the set of all labels occurring inΓ ⇒ ∆. Then, we note that the domainVar of an assignment f in Definition 5.7.4 can be restricted to Var(Γ ⇒ ∆). The following proposition shows that the clauses for relational atoms and negated form of them characterize what they intend to capture.
Proposition 5.7.3. For anyIntK-modelM, assignmentf, agenta∈Agtandx, y∈Var, (i) :M,f ⊩xRαayiff(f(x),f(y))∈Rαa, (ii) :M,f ⊩xRαayiff(f(x),f(y))<Rαa.
4Note that¬pis an abbreviation ofp→ ⊥.
Proof. Both are easily shown by induction ofα. Let us consider the case ofα=(α′,A) in the proof of (ii). We showM,f ⊮ xRα,aAy iff(f(x),f(y))∈Rα,aA. M,f ⊮ xRαay is, by Definition 5.7.3 and the induction hypothesis, equivalent to (f(x),f(y)) ∈ Rαa and Mα,f(x)⊩AandMα,f(y)⊩A. That is also equivalent to (f(x),f(y))∈Rα,aA. □
For preparations of the soundness theorem, we show the following propositions.
Proposition 5.7.4. LetM=(W,(Ra)a∈Agt,V) andMα =(Wα,(Rαa)a∈Agt,Vα) be arbitrary Kripke models. IfwRαavanduRatandw⩽uandv⩽t, thenuRαatholds.
Proof. By induction on α, and the base case whereα = ϵ is trivial. Therefore, we show the case whereα=α′,A. SupposewRαa′,AvanduRatandw ⩽uandv⩽t. By the supposition, we obtainwRαa′vandM, w⊩AandM, v⊩A. By induction hypothesis, uRαa′t; and by Proposition 5.1.1, we obtainM,u ⊩ AandM,t ⊩ A. Combining with
uRαa′t, we concludeuRαa′,At. □
Proposition 5.7.5. For any Kripke modelM, assignment f,a∈Agtandx, y∈Var, (i) M,f ⊩xRαay iff (f(x),f(y))∈Rαa,
(ii) M,f ⊩xRαay iff (f(x),f(y))<Rαa.
Proof. Both are easily shown by induction ofα. Let us consider the case ofα=α′,A in the proof of (ii). We showM,f ⊮ xRα,aAyiff(f(x),f(y))∈Rα,aA. M,f ⊮ xRα,aAyis, by Definition 3.3.3 and the induction hypothesis, equivalent to (f(x),f(y)) ∈ Rαa and Mα,f(x)⊩AandMα,f(y)⊩A. That is also equivalent to (f(x),f(y))∈Rα,aA.
□ In order to establish the soundness ofGIntPALfor birelational Kripke semantics, we basically employ Simpson’s argument [78, p.153-5] for the soundness of a natural de-duction system for IntK with some modifications for the notion of public announce-ment5. Given any sequentΓ⇒∆, we may extract a directed graph with the help of the relational atoms inΓas follows.
Definition 5.7.5. The derived graphGr(Γ⇒∆) from a sequentΓ⇒∆is a (labelled) directed graph (L,(Ea)a∈Agt) whereLis the setVar(Γ⇒∆) of all labels inΓ⇒∆and Ea⊆V×Vis defined as follows:xEayiffxRαay∈Γfor some listα(a∈Agt).
Next we recall the notion of tree for a finite directed graph.
Definition 5.7.6(Tree). Give any finite directed graph (L,(Ea)a∈Agt), we say that (L,(Ea)a∈Agt) is atreeif the graph is generated with the rootx0and, for every nodex, there is a unique sequence (x1, . . . ,xm) fromLsuch that, for all 0≤k<m, there exists an agentak∈Agt such thatxkEakxx+1andx=xm.
In order to prove the soundness of the rules (R□a) and (R[.]), our attention must be restricted to the sequents whose derived graphs are trees. And, the following lemma (cf. [78, Lemma 8.1.3]) plays a key role in establishing the soundness of the above two rules, where we also note that the restrictions (F1) and (F2) in birelational Kripke semantics are necessary to prove the lemma.
5The author is grateful to the suggestion by Katsuhiko Sano. Because of that, he noticed the application of Simpson’s lifting lemma to a coherent proof of the soundness theorem ofGIntPAL.
Lemma 5.7.1(Lifting lemma). LetΓ⇒∆be a sequent such thatGr(Γ⇒∆) is a tree, M=(W,⩽,(Ra)a∈Agt,V) an IntK-model, and f an assignment fromVar(Γ⇒ ∆) toW such thatM,f ⊩Afor allA∈Γ. Then, for all labelsx∈Var(Γ⇒∆) andw∈W with f(x)⩽w, there exists an assignment f′fromVar(Γ ⇒ ∆) toW such that f′(x)=w, f(z)⩽ f′(z) for all labelsz∈Var(Γ⇒∆) andM,f′⊩Afor allA∈Γ.
Proof. We sketch the idea of its proof by an example. Consider a sequentΓ ⇒ ∆ whereΓ ={x0Rαax1,x1Rβbx2,x0Rγcx3}and∆ =∅. Then,Gr(Γ⇒∆)=(L,Ea,Eb,Ec)= ({x0,x1,x2,x3},{(x0,x1)},{(x1,x2)},{(x0,x3)}) is a tree. LetM =(W,Ra,Rb,Rc,V) be an IntK-model, and f:{x0,x1,x2,x3} → W an assignment such that M,f ⊩ x0Rαax1 andM,f ⊩ x1Rβbx2 andM,f ⊩ x0Rγcx3(they are, by Proposition 5.7.5, equivalent to
f(x0)Rαaf(x1) and f(x1)Rβbf(x2) and f(x0)Rγcf(x3) respectively).
Fix anyw1∈Wsuch thatf(x1)⩽w. By assumptionsf(x0)Rαaf(x1) andf(x1)⩽w1, we obtainf(x0)(Ra◦⩽)w1. Then by (FS2), we obtainf(x0)⩽w0andw0Raw1for some w0∈W. Fix suchw0. By Proposition 5.7.4,w0Rαaw1. Next, since we havef(x1)Rβbf(x2) andf(x1)⩽w1, we also havew1Rbw2andw2⩾ f(x2) for somew2∈Wby (FS1) . Fix suchw2 ∈W. By Proposition 5.7.4,w1Rβbw2. Lastly, since we have f(x0)Rγcf(x3) and f(x0)⩽w0, we also havew0Rbw3andw3⩾ f(x3)for somew3∈Wby (FS1) . Fix such w3∈W. By Proposition 5.7.4,w0Rγcw3.
We define f′ : {x0,x1,x2,x3} → W by f′(xi) = wi(i ∈ {0,1,2,3}). Function f′ defined in this way satisfies the following requirements:
• f′(x1)=w1,
• f(z)⩽f′(z) for allz∈ {x0,x1,x2,x3},
• M,f′⊩ x0Rαax1andM,f′⊩x1Rβbx2andM,f′ ⊩x0Rγcx3fromw0Rαaw1, w1Rβbw2
andw0Rγcw3.
□ Now, we are ready to prove a stronger form of the soundness theorem ofGIntPAL with the notion of tree for derived graphs from sequents.
Theorem 5.7.1(Soundness ofGIntPAL). Given any sequentΓ⇒∆such thatGr(Γ⇒
∆) is a finite tree, if⊢GIntPALΓ⇒∆, thenΓ⇒∆ist-valid in everyIntK-modelM.
Proof. Suppose⊢GIntPAL Γ⇒ ∆such thatGr(Γ⇒ ∆) is a finite tree. Then the proof is carried out by induction of the height of the derivation ofΓ⇒ ∆inGIntPAL. We confirm the following cases alone.
Base case: we show that xRαav ⇒ xRαav ist-valid. Suppose for contradiction that M,f ⊩xRαavandM,f ⊩xRαav. By Proposition 5.7.3, this is impossible.
The case where the last applied rule is(L□a): In this case, we have a derivation of Γ ⇒ ∆,xRαay and y:αA,Γ ⇒ ∆in GIntPAL. BothGr(Γ ⇒ ∆,xRαay) and Gr(y:αA,Γ⇒∆) trivially keep the same structure of tree; therefore, the induction hypothesis may be applied to both derivations. And now we haveΓ⇒ ∆,xRαay andy:αA,Γ ⇒ ∆aret-valid in any IntK-Kripke modelM. Suppose for a con-tradiction that there is some f:L→ D(M) such thatM,f ⊩Afor allA∈Γand
M,f ⊩x:α□aAandM,f ⊩Bfor allB∈∆. Fix such f. Now it suffices to show M,f ⊩xRαayorM,f ⊩y:αA. From our suppositionM,f ⊩ x:α□aA, we obtain (f(x),f(y))<(⩽◦Ra)αorMα,f(y)⊩A. Suppose the former disjunct, which is equivalent to f(x)̸⩽vor (v,f(y)) <Ra for anyv∈ W. Fixvas f(x). Then we obtain (f(x),f(y))<Ra, and by Proposition 5.7.3,M,f ⊩ xRαay. It contradicts Γ⇒∆,xRαayist-valid. Next, suppose the latter disjunctMα,f(y)⊩Awhich is equivalent toM,f ⊩y:αA. It contradictsy:αA,Γ⇒ ∆ist-valid. Therefore, we obtain contradictions in either case.
The case where the last applied rule is(Rat): We show the contraposition. Suppose there is some f : Var → W such that,M,f ⊩ Afor allA∈ Γ, andM,f ⊩ B for allB∈∆, andM,f ⊩ x:α,Ap. Fix such f. We suffice to showM,f ⊩ x:αp.
By Definition 5.7.3, M,f ⊩ x:α,Ap is equivalent toMα,A,f(x)⊮p and f(x) ∈ D(Mα,A). By f(x) ∈ D(Mα,A), we obtain f(x) ∈ D(Mα) andMα,f(x) ⊩ A.
It follows fromMα,f(x) ⊩ A andMα,A,f(x)⊮ p that f(x) < Vα(p), This is equivalent toM,f ⊩x:αp. Then, the contraposition has been shown.
The case where the last applied rule is(Lrela3): In this case, we have a derivation of xRαay,Γ ⇒ ∆ inGIntPAL. Since Gr(xRα,aAy,Γ ⇒ ∆) is a tree and any formula restricting relational atom does not affect the structure of the graph Gr(xRαay,Γ ⇒∆), it is also a tree. Then the induction hypothesis is applicable to the uppersequent of the derivation, and therefore, we obtain thatxRαay,Γ⇒∆ ist-valid for anyM. We must showxRα,aAy,Γ⇒∆ist-valid for anyMSuppose there is some f:L→ D(Mα) such that,M,f ⊩Afor allA∈ Γ,M,f ⊩ xRα,aAy andM,f ⊩Bfor allB∈∆. Fix such f. FromxRα,aAy, we obtainM,f ⊩xRαay. This is what we want to show.
The case where the last applied rule is(R→): In this case, we have a derivation of x:αA,Γ ⇒ ∆,x:αBinGIntPAL, and sinceGr(x:αA,Γ ⇒ ∆,x:αB) =Gr(Γ ⇒
∆,x:αA → B), it is trivially a tree. Let the graph be (L,(Ea)a∈Agt). By the ap-plication of the induction hypothesis, we obtain there is no f:L → D(M) such thatM,f ⊩ x:αAandM,f ⊩ Afor all A ∈ ΓandM,f ⊩ x:αB. Then it suf-fices to show that if there is f:L → D(M) such thatM,f ⊩ Afor allA ∈ Γ andM,f ⊩ x:αA→B, then there is f:L → D(M) such thatM,f ⊩ x:αAand M,f ⊩ Afor all A ∈ ΓandM,f ⊩ x:αB(∗). Suppose the antecedent of (∗), and consider such f:L → D(M). Then we obtain M,f ⊩ A for all A ∈ Γ and M,f ⊩ x:αA→B which is equivalent to f(y) ≤α v and Mα,f(y) ⊩ A and Mα,f(y) ⊮ B for some v ∈ D(Mα), and f(y) ∈ D(Mα). Meanwhile, by Lemma 5.7.1, we obtain a function f′:L → D(Mα) such that f′ ≥ f and M,f′ ⊩ Afor allA ∈ Γ. Now, f′can be extend to f′′:L → D(Mα) such that f′′(x)=vand all others are the same as f′. Then we obtain the succedent of (∗) that is what we desired.
The case where the last applied rule is(R[.]): In this case, we have a derivation of x:αA,Γ ⇒ x:α,AB inGIntPAL, and sinceGr(x:αA,Γ ⇒ x:α,AB) = Gr(Γ ⇒ x:α[A]B), it is trivially a finite tree. Let us denote the graph by (L,(Ea)a∈Agt).
Suppose for contradiction that there is an assignment f:L → D(M) such that
M,f ⊩ Afor allA∈ ΓandM,f ⊩ x:α[A]B. Fix such f:L → D(M). Then, it suffices to show that there is an assignmentf′:L→ D(M) such thatM,f′⊩x:αA andM,f′⊩Afor allA∈ΓandM,f′⊩x:α,AB, since this gives us a contradiction with our induction hypothesis tox:αA,Γ ⇒ x:α,AB. By the supposition,M,f ⊩ x:α[A]B, which is equivalent to: f(x) ∈ D(Mα) and there is some v ∈ D(Mα) such that f(x) ⩽α vandMα, v ⊩ AandMα,A, v ⊮ B. By Lemma 5.7.1 and the supposition thatM,f ⊩Afor allA∈Γ, we obtain an assignment f′:L→ D(M) such that f′(x)=vandf(z)⩽ f′(z) for allz∈LandM,f′ ⊩Afor allA∈Γ. It also follows thatM,f′⊩x:αAandM,f′⊩x:α,AB, as desired.
The case where the last applied rule is(R□a): In this case, we have a derivation of xRαay,Γ⇒y:αAinGIntPAL. Let us denote a treeGr(Γ⇒ x:α□aA) by (L,(Eb)b∈Agt).
Sinceyis a fresh variable,Gr(xRαay,Γ⇒y:αA)=(L∪{y},Ea∪{(x, y)},(Eb)b∈Agt\{a}) is still a finite tree. Suppose for contradiction that there is an assignment f:L→ D(M) such thatM,f ⊩Afor allA∈ΓandM,f ⊩x:α□aA. Fix such assignment f:L→ D(M). It suffices to show that there is an assignmentg:L∪ {y} → D(M) such thatM, g⊩ Afor allA ∈ΓandM, g⊩ xRαayandM, g⊩y:αA, since this gives us a contradiction with our induction hypothesis toxRαay,Γ⇒y:αA. Then, by the supposition ofM,f ⊩x:α□aA, we havef(x)∈ D(Mα) and there are some v,u ∈ D(Mα) such that f(x)⩽αu,uRαavandMα, v ⊮ A. By the supposition that M,f ⊩ Afor allA ∈ Γ, we apply Lemma 5.7.1 to the sequentΓ ⇒ x:α□aA to find an assignment f′:L → D(Mα) such that f′(x)=u, f(z) ⩽ f′(z) for all z∈LandM,f′ ⊩Afor allA∈Γ. Now, f′can be extend to a new assignment g:L∪ {y} → D(M) such thatgis the same asf′exceptg(y)=v. Then, we obtain M, g⊩Afor allA∈Γ,M, g⊩xRαayandM, g⊩y:αA, as desired.
□ We have done to prove all theorems which are declared to be shown in the intro-duction. But the following last piece should be significant for an indirect proof of the completeness ofGIntPAL.
Proposition 5.7.6. If⇒x:ϵAist-valid in anIntK-modelM, thenAis valid inM.
Proof. Suppose that ⇒ x:ϵAis t-valid. So, it is not the case that there exists some assignment f such thatM,f ⊩x:ϵA. Equivalently, for all assignments f,M,f ⊮x:ϵA.
For any assignmentf,M,f ⊮x:ϵAis equivalent toM,f(x)⊩Abecause f(x)∈ D(M).
So, it follows thatM,f(x)⊩Afor all assignments f. Then, it is immediate to see that
Ais valid inM, as required. □
Finally, we may establish the completeness theorem as follows.
Corollary 5.7.1(Completeness ofGIntPAL). Given any formulaAand labelx∈Var, the following are equivalent:
(i) Ais valid on allIntK-models;
(ii) ⊢HIntPALA;
(iii) ⊢GIntPAL+⇒x:ϵA;
(iv) ⊢GIntPAL⇒ x:ϵA.
Proof. The direction from (i) to (ii) is established by Fact 5.3.1 and the direction from (ii) to (iii) is shown by Theorem 5.5.1. Then, the direction from (iii) to (iv) is estab-lished by the admissibility of cut, i.e., Theorem 5.6.1. Finally, the direction from (iv) to (i) is shown by Theorem 5.7.1 and Proposition 5.7.6, sinceGr(⇒ x:ϵA) is a tree (a single point-tree) and therefore Theorem 5.7.1 is applicable, and then Proposition 5.7.6
may be applied to its conclusion. □
Chapter 6
Conclusion
6.1 Summary of contributions
In Chapter 2, we introduced multi-modal logics and labelled sequent calculus which are main bases of this thesis. In Chapter 3, we found that inference rules for accessi-bility relations were missing in the existing labelled sequent calculus ofG3PAL, and that (RA4) ([A]□aB ↔ A → □a[A]B), one of the recursion axioms in HPAL, was not provable by the system, although it should be if it is complete for Kripke seman-tics. Therefore, we revisedG3PALby reformulating and adding some rules to it and named the first labelled system in this thesisGPAL. Additionally, we showed the cut-elimination theorem ofGPAL(Theorem 3.2.2). During this revision, we also make the notion ofsurvivalexplicit. According to this revision, we could show thatGPALis sound for Kripke semantics (Theorem 3.3.1). Moreover, by carefully considering the notion of survival, we found the link-cutting version of PAL’s semantics is more suit-able to our labelled sequent calculus than the standard semantics i.e., the world-deleting semantics, and then we showedGPALis complete for the link-cutting semantics (The-orem 3.4.1). Then, the basis ofGPALwas extended to be based on other basic modal logics including S5 which is the usual basis of epistemic logics.
In Chapter 4, we introduced the second labelled sequent calculus GEAK, and showed its cut-admissibility (Theorem 4.2.1) and the soundness theorem (Theorem 4.4.1).
After that, we obtained as a corollary the semantic completeness (Corollary 4.4.1) through the completeness theorem of an existing Hilbert-systemHEAK. Moreover, we also showed our system is sound for the standard Kripke semantics. In the proof of the soundness theorem, we also took into account the notion of survival of worlds in the restricted domain. Therefore, we demonstrated that it is critical especially in the case of labelled systems to carefully consider deleted (or restricted) world(s) in a mod-ified Kripke model. EAK is not only a complicated logic but also the core of the field of DEL (we mentioned in the introduction EAK is called Dynamic Epistemic Logic in a narrower range of the meaning). Therefore, our labelled system is handled much easier than Hilbert-systemHEAKand is beneficial for the study of DEL since it is often troublesome to construct a derivation of a theorem of it (formulas concerning a
knowledge-state tend to be long and complicated, in fact). Then, the basis ofGEAK was extended to be based on other basic modal logics including S5 which is the usual basis of epistemic logics.
In Chapter 5, we provided the third labelled sequent calculusGIntPALfor PAL within an intuitionistic framework, and as with previous labelled systems, we showed the cut-elimination theorem (Theorem 5.6.1), the soundness theorem (Theorem 5.7.1) and the completeness theorem as a corollary (Corollary 5.7.1) of the completeness of Hilbert-systemHEAKand Theorem 5.7.1. A sequent calculus that is easy to handle may be particularly significant for intuitionistic epistemic logics that regard verification or evidence as important.