Extensions of EAK from K to S5

For anyΘ⊆ {Ta,Ba,4a,5a|a∈Agt}, Logic of Epistemic Actions and Knowledge EAKΘis the set of all derivable formulas inHEAKΘ. We name someEAKΘ.

EAKT:=EAK{Ta|a∈Agt}, EAKS4:=EAK{Ta,4a|a∈Agt}, EAKB:=EAK{Ta,Ba|a∈Agt}, EAKS5:=EAK{Ta,5a|a∈Agt}. Theorem 4.5.1(Soundness and completeness of HEAKΘ ). Let Θ be a subset of {Ta,Ba,4a,5a|a∈Agt}andA∈ LEAK. Then the following holds:

MΘ⊩A iff⊢HEAKΘA.

Proof. The proof is carried out by the same step as in Theorem 2.3.2. □ Corollary 4.5.1. EAKXis decidable, whereXbe an element of{T,B,S4,S5,D}.

Proof. We show that there is an effective method for deciding of any formulaA∈ LEAK

whether or not it is a theorem ofEAKX. Fix any A ∈ LEAK. Note that translation t:LEAK → LELis inductively defined and so it provides an effective method which is a composition of the two effective methods. Then since modal logicXis decidable by Corollary 2.1.1,t(A)∈ LMLcan be decided whether it is a theorem ofX. □ Extensions of GEAK Let us define the extensions ofGEAK. We add toGEAKone or more of the additional rules which correspond to the frame properties.

Table 4.3: Rules for frame properties

⟨x, ϵ⟩R_a⟨x, ϵ⟩,Γ⇒∆∥Σ

Γ⇒∆∥Σ (refa) Γ⇒∆,⟨x, ϵ⟩Ra⟨y, ϵ⟩ ∥Σ ⟨y, ϵ⟩Ra⟨x, ϵ⟩,Γ⇒∆∥Σ Γ⇒∆∥Σ (syma) Γ⇒∆,⟨x, ϵ⟩Ra⟨y, ϵ⟩ ∥Σ Γ⇒∆,⟨y, ϵ⟩Ra⟨z, ϵ⟩ ∥Σ ⟨x, ϵ⟩Ra⟨z, ϵ⟩,Γ⇒∆∥Σ

Γ⇒∆∥Σ (tra_a)

Γ⇒∆,⟨x, ϵ⟩Ra⟨y, ϵ⟩ ∥Σ Γ⇒∆,⟨x, ϵ⟩Ra⟨z, ϵ⟩ ∥Σ ⟨y, ϵ⟩Ra⟨z, ϵ⟩,Γ⇒∆∥Σ

Γ⇒∆∥Σ (euc_a)

Let^∗be a function from {Ta,Ba,4a,5a |a ∈Agt}to{(refa),(syma),(traa),(euca)

|a∈Agt}defined as follows:

Ta∗:=(refa), 4a∗:=(traa), Ba∗:=(syma), 5a∗:=(euca).

Let Θbe a subset of {T_a,B_a,4_a,5_a | a ∈ Agt}. ThenΘ^∗ is defined to be the set {X^∗|X∈Θ}.

Definition 4.5.2(Extensions ofGEAK). LetΘbe a subset of{Ta,Ba,4a,5a|a∈Agt}. A labelled sequent calculusGEAKΘ^∗is an extension ofGEAK, when each element ofΘ^∗is added toGEAKas inference rules.

Some particular combinations of inference rules are given names.

GEAK_T:=GEAK{(refa)|a∈Agt}, GEAKB:=GEAK{(syma)|a∈Agt}, GEAKS4:=GEAK{(refa),(traa)|a∈Agt}, GEAKS5:=GEAK{(refa),(euca)|a∈Agt}, We call eachGEAKΘ^∗with (Cut)GEAKΘ^∗+.

Theorem 4.5.2. For anyΘ⊆ {T_a,B_a,4_a,5_a |a ∈Agt}, if⊢HEAKΘ Athen⊢GEAKΘ^∗⇒ x:^ϵA(for anyx), for any formulaA∈ LEAK.

Proof. Proof is almost the same as Theorem 3.5.2. We look at the following additional cases.

Case ofBawith (syma). In this case, we show⊢GDELΘ^∗⇒ x:Bawhere (syma)∈Θ^∗.

Initial Seq. x:A,xRay⇒y:♢aA,xRay

Initial Seq. yRax,x:A⇒yRax

Initial Seq. yRax,x:A⇒x:A y^Rax,x:A⇒y:♢aA (R♢a) yRax,x:A,xRay⇒y:♢aA (Lw) x:A,xRay⇒y:♢aA (syma)

x:A⇒x:□a♢aA (R□a)

⇒x:A→□a♢aA (R→)

Case ofTawith (refa). In this case, we show⊢GDELΘ^∗⇒ x:Tawhere (refa)∈Θ^∗. Initial Seq.

xRax⇒x:A,xRax

Initial Seq. xRax,x:A⇒x:A xR_ax,x:□aA⇒x:A (R□a)

x:□aA⇒x:A (re fa)

⇒x:□aA→A (R→)

Case of5_awith (euc_a). In this case, we show⊢GDELΘ^∗⇒ x:5_awhere (euc_a)∈Θ^∗.

Initial Seq. xR_ay,xR_az,z:A⇒y:♢A,xR_ay

Initial Seq. xR_ay,xR_az,z:A⇒y:♢A,xR_az

Initial Seq. y^Raz,z:A⇒y^Raz

Initial Seq. y^Raz,z:A⇒z:A y^Raz,z:A⇒y:♢A (R♢a) y^Raz,xR_ay,xR_az,z:A⇒y:♢A (Lw) xR_ay,xR_az,z:A⇒y:♢A (euca)

x:♢aA,xR_ay⇒y:♢aA (L♢a) x:♢aA⇒x:□a♢aA (R□a)

⇒x:♢aA→□a♢aA (R→)

□ Theorem 4.5.3(Soundness ofGEAKΘ). For anyΘ⊆ {T_a,B_a,4_a,5_a|a∈Agt}, given any c-sequentΓ⇒∆∥ΣinGEAKΘ, if⊢GEAKΘΓ⇒∆∥Σ, thenΓ⇒∆∥Σist-valid in every modelM∈M_Θ.

Proof. Fix anyΘ⊆ {Ta,Ba,4a,5a | a ∈Agt}, and suppose⊢GEAKΘ Γ ⇒ ∆∥ Σ. Fix any modelM∈MΘ. Then we showΓ⇒∆∥Σist-valid. Fix any sequentΓ^′⇒∆^′in the c-sequent. We show the additional cases to the proof of Theorem 3.3.1, and so it suffices to show that any additional rule keepst-validity in any corresponding model to the rule.

Case of(ref_a): Fix anyR_a-reflexive modelM. We show the contraposition. Suppose that there is some f : Var → D(M),M,f ⊩ Γ^′, andM,f ⊩ ∆^′. Fix such f. It suffices to show (f(x),f(x))∈ Rawhich is equivalent to⟨f(x), ϵ⟩Ra⟨f(x), ϵ⟩. This is trivially obtained from theRa-reflexive modelM.

Other cases can be shown by almost the same way as Proposition 3.5.3. SinceΓ^′⇒∆^′ is sound and is an arbitrary sequent inΓ⇒∆∥Σ, this c-sequent is sound as well. □ Theorem 4.5.4(Cut elimination theorem ofGEAKΘ^∗+). For anyΘ⊆ {T_a,B_a,4_a,5_a| a∈ Agt}, and any c-sequentΓ ⇒ ∆∥ Σ, if⊢GEAKΘ^∗+ Γ⇒ ∆∥Σ, then⊢GEAKΘ^∗ Γ ⇒

∆∥Σ.

Proof. It suffices to show additional cases for (refa),(syma),(traa) and (euca) in addi-tion to Theorem 4.2. Since there is no principal expression(s) introduced by the upper c-sequent(s), we do not have the case where cut expressionAs on both sides of upper c-sequents are principal expressions. The other cases like only one of cut expressions is introduced by the right upper c-sequent or the left upper c-sequent are straightforward.

The proof goes through the same procedure as in the proof of Theorem 3.2.2 with the rule of (Ecut), and the proof is divided into four cases. In brief,

(1) at least one of upper c-sequents of (Ecut) is an initial c-sequent;

(2) the last inference rule of either upper c-sequents of (Ecut) is a structural rule;

(3) the last inference rule of either upper c-sequents of (Ecut) is a non-structural rule, and the principal expression introduced by the rule is not the cut expression; and (4) the last inference rules of two upper c-sequents of (Ecut) are both non-structural rules, and the principal expressions introduced by the rules used on the upper c-sequents of (Ecut) are both cut expressions.

It suffices to show additional cases for (refa),(syma),(traa) and (euca) in addition to the proof of Theorem 3.2.2. Since there is no principal expression(s) introduced by the upper c-sequent(s), we do not have the case (4) where cut expressionAs on both sides of upper c-sequents are principal expressions. The other cases like only one of cut expressions is introduced by the right upper c-sequent or the left upper c-sequent are straightforward. We look at one of such cases.

Case of (3)where one of upper c-sequents of (Ecut) is inference rule (sym_a).

.... D1

Γ⇒∆,Aⁿ∥Σ

.... D2

xR_ay,A^m,Γ^′⇒∆^′∥Σ

.... D3

yR_ax,A^m,Γ^′⇒∆^′∥Σ A^m,Γ^′⇒∆^′∥Σ (syma) Γ,Γ^′⇒∆,∆^′∥Σ (Ecut)

This is transformed into the derivation:

.... D1

Γ⇒∆,Aⁿ ∥Σ

.... D2

A^m,xR_ay,Γ^′⇒∆^′∥Σ xR_ay,Γ,Γ^′⇒∆,∆^′∥Σ (Ecut)

.... D1

Γ⇒∆,Aⁿ∥Σ

.... D3

A^m, yR_ax,Γ^′⇒∆^′∥Σ yR_ax,Γ,Γ^′⇒∆,∆^′∥Σ (Ecut) Γ,Γ,Γ^′,Γ^′⇒∆,∆,∆^′,∆^′∥Σ (syma)

Γ,Γ^′⇒∆,∆^′∥Σ (Lc)/(Rc)

Every other case can be shown similar to this. □

Then the corollary below holds.

Corollary 4.5.2. Given a formula A, x ∈ Var, Θ ⊆ {Ta,Ba,4a,5a | a ∈ Agt}, the following statements are all equivalent.

(i) M_Θ⊩A, (ii) ⊢HEAKΘA, (iii) ⊢GEAKΘ^∗+⇒ x:^ϵA, (iv) ⊢GEAKΘ^∗⇒x:^ϵA.

Proof. The direction from (i) to (ii) is shown by Theorem 4.5.1 and the direction from (ii) to (iii) is established by Theorem 4.5.2. Then, the direction from (iii) to (iv) is established by the admissibility of (Cut) (Theorem 4.5.4). Finally, the direction from

(iv) to (i) is shown by Theorem 4.5.3. □

Chapter 5

Intuitionistic Public

Announcement Logic (IntPAL)

Epistemic logics including two major DELs such as PAL and EAK usually employ classical modal logic as their underlying logic; however, we may easily imagine that they can be constructed on a different foundation, intuitionistic modal logic. Intuition-istic PAL (IntPAL), which is a combination of the most basic DEL i.e., PAL and an intuitionistic modal logic, can become the touchstone of intuitionistic DELs.

In the context of epistemic logic, knowledge defined in an intuitionistic system can be regarded as knowledge with verification or evidence (cf. [2, 87]).¹ The area of intuitionistic modal logics, since Fitch [26] proposed, has been developed histori-cally by efforts of several logicians (e.g., [15, 25, 64, 70, 78]). On the foundation of the past studies, Ma et al. [49] recently gave a Hilbert-system of IntPAL (we called it HIntPAL), which is based on intuitionistic modal logic IK (or IntK) by Fischer Servi [25] and Simpson [78], is shown to be semantically complete for algebraic se-mantics. It is our expectation that a sequent calculus brings abundant benefits espe-cially for constructive knowledge requiring verification, since a sequent calculus is usually feasible in computation, compared with Hilbert-system; the calculus can easily be translated into an algorithmic procedure. Thus it can supply a proof for any valid formula i.e., verification for any knowledge that is based on intuitionistic system.

The outline of Chapter 5 is as follows. Section 5.1 provides the birelational Kripke semantics and the Hilbert-system HIntPALfor IntPAL. Section 5.3 introduces our calculusGIntPAL(with the rule of cut) and shows that all theorems ofHIntPALare derivable inGIntPAL⁺ (Theorem 5.5.1). Section 5.6 establishes the cut elimination theorem ofGIntPAL⁺(Theorem 5.6.1) and, as a corollary of the theorem, shows that GIntPAL⁺ is consistent. Section 5.7 tackles the soundness theorem of GIntPAL⁺ (Theorem 5.7.1), and it should be noted that its soundness is not straightforward at all by the following two reasons. First, it depends on a non-trivial choice of the notions of validity of a sequent as suggested in [61]. Second, there is another difficulty, pointed

1Regarding recent trends in knowledge-representation with intuitionistic logic, several constructive de-scription logics [13, 21, 53] are proposed to investigate possibly incomplete knowledge.

out in [78], which is peculiar to intuitionist modal logic. Then the semantic complete-ness ofGIntPAL(Corollary 5.7.1) is shown through the proven theorems. The last section concludes the paper.

5.1 Language L

and birelational Kripke Seman-tics

First of all, we address the syntax of IntPAL. LetProp ={p,q,r, . . .}be a countably infinite set of propositional atoms andAgt={a,b,c, . . .}a nonempty finite set of agents.

Then the setLIntPAL = {A,B,C, . . .}of formulas of IntPAL is inductively defined as follows:

A::=p| ⊥ |(A∧A)|(A∨A)|(A→A)|□aA|♢aA|[A]A| ⟨A⟩A,

wherep∈Prop,a∈Agt. We define¬A:=A→ ⊥. Also,⊤andA↔Bare defined as usual. Similar to PAL,□aAreads ‘agentaknows thatA’, and [A]Breads ‘after public announcement ofA, it holds thatB’.

Example 5.1.1. Let us consider a propositional atompto read ‘it will rain tomorrow’.

Then a formula¬(□ap∨□a¬p) means that adoes not know whether it will rain to-morrow or not, and [¬p]□a¬pmeans that after a public announcement (e.g., a weather report) of¬p,aknows that it will not rain tomorrow.

Let us go on to the semantics of IntPAL. We mainly follow the birelational Kripke semantics introduced in Ma et al. [49], which is based on intuitionistic version of modal logic K. We callF=(W,⩽,(R_a)_a∈Agt) anIntK-frameif (W,⩽) is a nonempty poset (Wis also denoted byD(M)), (R_a)_a∈Agtis aAgt-indexed family of binary relations onWsuch that the following two conditions (F1) and (F2) in Simpson [78, p.50] are satisfied:

(F1) : (⩾◦Ra)⊆(Ra◦⩾), (F2) : (R_a◦⩽)⊆(⩽◦R_a).

We note that (F1) and (F2) are essential features to express a combination of the two different relations such as⩽andR_a.

Moreover, a pairM=(F,V) is anIntK-modelifFis an IntK-frame andV:Prop→ P^↑(W) is a valuation function where

P^↑(W) :={X∈ P(W)|x∈Xandx⩽yjointly implyy∈Xfor allx, y∈W}, that is,P^↑(W) is the set of all upward closed sets. Next, let us define the satisfaction relationM, w⊩ A. Given an IntK-model M, a worldw ∈ D(M), and a formulaA ∈ LIntPAL, we defineM, w⊩Aas follows:

M, w⊩p iff w∈V(p), M, w⊩⊥ Never,

M, w⊩A∧B iff M, w⊩AandM, w⊩B, M, w⊩A∨B iff M, w⊩AorM, w⊩B,

M, w⊩A→B iff for allv∈W:w⩽vandM, v⊩Ajointly imply M, v⊩B, M, w⊩ □aA iff for allv∈W:w(⩽◦R_a)vimpliesM, v⊩A,

M, w⊩ ♢aA iff for somev∈W :wRavandM, v⊩A,

M, w⊩[A]B iff for allv∈W:w⩽vandM, v⊩Ajointly imply M^A, v⊩B, M, w⊩⟨A⟩B iff M, w⊩AandM^A, w⊩B,

where the restrictionM^A, in the definition of the announcement operators, is the re-stricted IntK-model to the truth set ofA, defined asM^A = ([[A]]M,⩽^A,(R_a^A)a∈^Agt,V^A) with

[[A]]M := {w∈W |M, w⊩A}

⩽^A := ⩽∩([[A]]M×[[A]]M) R^A_a := Ra∩([[A]]M×[[A]]M)

V^A(p) := V(p)∩[[A]]M (p∈Prop).

We note that the conditions (F1) and (F2) are still satisfied inM^A. Added to these, the restriction of the composition (⩽◦Ra)^Ais defined by (⩽◦Ra)∩([[A]]M×[[A]]M).

Definition 5.1.1. A formulaAisvalidin an IntK-modelMifM, w ⊩ Afor all w ∈ D(M).

By the above semantics, the important semantic feature, heredity, is preserved as follows.²

Proposition 5.1.1(Hereditary). For all IntK-modelsM, for allw, v∈ D(M), ifM, w⊩ Aandw⩽v, thenM, v⊩A, for any formulaA.

Besides, the following proposition is also significant.

Proposition 5.1.2. (⩽◦Ra)^A=(⩽^A◦R^A_a)

Proof. We briefly look at the direction of⊆. Fix anyv,u∈ D(M) such thatv(⩽◦R_a)^Au.

We showx(⩽^A◦R^A_a)u. By the above definition, we havev(⩽◦R_a)uand (v,u)∈[[A]]M× [[A]]M, and then there exists some t, such thatv ⩽ t andtR_au. Take such t, and by Proposition 5.1.1, we gett∈[[A]]M. Therefore, we concludex(⩽^A◦R^A_a)u. □ We denote finite lists (A1, ...,An) of formulas byα, β,etc., and do the empty list byϵ. As an abbreviation, for any listα=(A1,A2, ...,An) of formulas, we naturally defineM^α inductively as: M^α :=M(ifα=ϵ), andM^α :=(M^β)^An =(W^β,An,(R^β,_a^An)a∈^Agt,V^β,An) (ifα = β,An). We may also denote (M^β)^An byM^β,An for simplicity. From Proposi-tion 5.1.2, the next corollary may be easily shown by inducProposi-tion on the number ofα. Corollary 5.1.1. (⩽◦Ra)^α=(⩽^α◦R^α_a)

2Two conditions, (F1) and (F2), are required to show heredity (and validity of axioms) in IntK on which GIntPALis based. In fact, one more condition is added to the two in [49] for some specific purpose in their paper. That isRa=(⩽◦Ra)∩(Ra◦⩾).