This paper was converted on www.awesomepapers.org from LaTeX by an anonymous user.
Want to know more? Visit the Converter page.

11institutetext: Institute of Logic and Cognition, Sun Yat-sen University 22institutetext: Department of Computer Science, Open University of the Netherlands 33institutetext: School of Philosophy, Zhejiang University

A Labelled Sequent Calculus for Public Announcement Logic

Hao Wu 11    Hans van Ditmarsch 22    Jinsheng Chen 33
Abstract

Public announcement logic (𝖯𝖠𝖫\mathsf{PAL}) is an extension of epistemic logic (𝖤𝖫\mathsf{EL}) with some reduction axioms. In this paper, we propose a cut-free labelled sequent calculus for 𝖯𝖠𝖫\mathsf{PAL}, which is an extension of that for 𝖤𝖫\mathsf{EL} with sequent rules adapted from the reduction axioms. This calculus admits cut and allows terminating proof search.

Keywords:
Public announcement logic, labelled sequent calculus, cut elimination.

1 Introduction

The modern modal approach to the logic of knowledge and belief was extensively developed by Hintikka [10] to interpret epistemic notions utilizing possible world semantics. The standard multi-agent epistemic logic 𝖤𝖫\mathsf{EL} is usually identified with the poly-modal modal logic 𝖲𝟧\mathsf{S5} with a group of agents. Public announcement logic (PAL), introduced in Plaza [17], is an extension of 𝖤𝖫\mathsf{EL} that studies logical dynamics of epistemic information after the action of public announcement. More general actions are studied in action model logic (see e.g. [5, 7, 4]).

𝖯𝖠𝖫\mathsf{PAL} is an extension of 𝖤𝖫\mathsf{EL} with announcement operators of the form [φ][\varphi]. As 𝖤𝖫\mathsf{EL}, formulas in 𝖯𝖠𝖫\mathsf{PAL} are interpreted in Kripke models in which all relations are reflexive, transitive and symmetric. In particular, formulas of the form [φ]​ψ[\varphi]\psi are interpreted in the restrictions of Kripke models induced by the announcement φ\varphi. The Hilbert-style axiomatization of 𝖯𝖠𝖫\mathsf{PAL} is obtained by adding to that of 𝖤𝖫\mathsf{EL} the so called reduction axioms for announcement operators, which can be used to eliminate announcement operators in a 𝖯𝖠𝖫\mathsf{PAL}-formula.

Generally speaking, it is difficult to prove whether proof search using a Hilbert-style axiomatization is decidable. In view of these, many proof systems for 𝖯𝖠𝖫\mathsf{PAL} are proposed in the literature, e.g., tableau systems [3], labelled sequent calculi [2, 16].

In this paper, we propose another labelled sequent calculus for 𝖯𝖠𝖫\mathsf{PAL}. This calculus is based on a labelled sequent calculus for 𝖤𝖫\mathsf{EL} proposed in Hakli and Negri [9] and rules for announcement operators designed according to the reduction axioms. This calculus admits structural rules (including cut) and allows terminating proof search. Unlike [2, 16], which are based on another semantics for 𝖯𝖠𝖫\mathsf{PAL}, our calculus is based on the original semantics and takes into account the conditions of reflexivity, transitivity and symmetry in 𝖤𝖫\mathsf{EL}.

The rest of the paper is structured as follows: Section 2 presents some basic notions and concepts. Section 3 presents our labelled sequent calculus G𝖯𝖠𝖫G_{\mathsf{PAL}} for 𝖯𝖠𝖫\mathsf{PAL}. Section 4 shows that G𝖯𝖠𝖫G_{\mathsf{PAL}} admits some structural rules, including cut. Section 5 shows that G𝖯𝖠𝖫G_{\mathsf{PAL}} allows terminating proof search. Section 6 compares G𝖯𝖠𝖫G_{\mathsf{PAL}} with related works, concludes the paper and discusses future work.

2 Preliminaries

2.1 𝖤𝖫\mathsf{EL} and 𝖯𝖠𝖫\mathsf{PAL}

Let 𝖯𝗋𝗈𝗉\mathsf{Prop} be a denumerable set of variables and 𝖠𝗀\mathsf{Ag} a finite set of agents. Language ℒ𝖤𝖫\mathcal{L}_{\mathsf{EL}} for epistemic logic is defined inductively as follows:

ℒ::=p∣¬φ∣φ∧φ∣φ→φ∣Kaφ\mathcal{L}::=p\mid\neg\varphi\mid\varphi\land\varphi\mid\varphi\to\varphi\mid K_{a}\varphi

Moreover, language ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}} for public announcement logic is defined inductively as follows:

ℒ::=p∣¬φ∣φ∧φ∣φ→φ∣Kaφ∣[φ]φ\mathcal{L}::=p\mid\neg\varphi\mid\varphi\land\varphi\mid\varphi\to\varphi\mid K_{a}\varphi\mid[\varphi]\varphi

where p∈𝖯𝗋𝗈𝗉p\in\mathsf{Prop} and a∈𝖠𝗀a\in\mathsf{Ag}. We use φ↔ψ\varphi\leftrightarrow\psi as an abbreviation for (φ→ψ)∧(ψ→φ)(\varphi\to\psi)\land(\psi\to\varphi). ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}} is an extension of ℒ𝖤𝖫\mathcal{L}_{\mathsf{EL}} with announcement formulas.

An epistemic frame ℱ\mathcal{F} is a tuple (W,{∼a}a∈𝖠𝗀)(W,\{\sim_{a}\}_{a\in\mathsf{Ag}}), where WW is a set of states and ∼a⊆W×W\sim_{a}\subseteq W\times W is a reflexive, transitive and symmetric relation for each a∈𝖠𝗀a\in\mathsf{Ag}.

An epistemic model ℳ\mathcal{M} is a tuple (W,{∼a}a∈𝖠𝗀,V)(W,\{\sim_{a}\}_{a\in\mathsf{Ag}},V) where (W,{∼a}a∈𝖠𝗀)(W,\{\sim_{a}\}_{a\in\mathsf{Ag}}) is an epistemic frame and VV is a function from 𝖯𝗋𝗈𝗉\mathsf{Prop} to 𝒫​(W)\mathcal{P}(W).

Let ℳ=(W,{∼a}a∈𝖠𝗀,V)\mathcal{M}=(W,\{\sim_{a}\}_{a\in\mathsf{Ag}},V) be an epistemic model and w∈Ww\in W. The notion of φ\varphi being true at ww in ℳ\mathcal{M} (notation: ℳ,w⊩φ\mathcal{M},w\Vdash\varphi) is defined inductively as follows:

ℳ,w⊩piffw∈V​(p)ℳ,w⊩¬φiffℳ,w⊮φℳ,w⊩φ∧ψiffℳ,w⊩φ​and​ℳ,w⊩ψℳ,w⊩φ→ψiffℳ,w⊮φ​or​ℳ,w⊩ψℳ,w⊩Ka​φifffor all​v∈W,w∼av​implies​ℳ,v⊩φℳ,w⊩[φ]​ψiffℳ,w⊩φ​implies​ℳφ,w⊩ψ\begin{array}[]{lll}\mathcal{M},w\Vdash p&~{}\text{iff}{}&w\in V(p)\\ \mathcal{M},w\Vdash\neg\varphi&~{}\text{iff}{}&\mathcal{M},w\nVdash\varphi\\ \mathcal{M},w\Vdash\varphi\land\psi&~{}\text{iff}{}&\mathcal{M},w\Vdash\varphi~{}\text{and}~{}\mathcal{M},w\Vdash\psi\\ \mathcal{M},w\Vdash\varphi\to\psi&~{}\text{iff}{}&\mathcal{M},w\nVdash\varphi~{}\text{or}~{}\mathcal{M},w\Vdash\psi\\ \mathcal{M},w\Vdash K_{a}\varphi&~{}\text{iff}{}&\text{for~{}all}~{}v\in W,w\sim_{a}v~{}\text{implies}~{}\mathcal{M},v\Vdash\varphi\\ \mathcal{M},w\Vdash[\varphi]\psi&~{}\text{iff}{}&\mathcal{M},w\Vdash\varphi~{}\text{implies}~{}\mathcal{M}^{\varphi},w\Vdash\psi\end{array}

where ℳφ=(Wφ,{∼aφ}a∈𝖠𝗀,Vφ)\mathcal{M}^{\varphi}=(W^{\varphi},\{\sim^{\varphi}_{a}\}_{a\in\mathsf{Ag}},V^{\varphi}) is called the model restricted to φ\varphi where Wφ={w∈W∣ℳ,w⊩φ}W^{\varphi}=\{w\in W\mid\mathcal{M},w\Vdash\varphi\}, ∼aφ=∼a∩(Wφ×Wφ)\sim^{\varphi}_{a}=\sim_{a}\cap(W_{\varphi}\times W_{\varphi}) and Vφ=V​(p)∩WφV^{\varphi}=V(p)\cap W^{\varphi}.

A formula φ\varphi is globally true in an epistemic model (notation: ℳ⊩φ\mathcal{M}\Vdash\varphi) if ℳ,w⊩φ\mathcal{M},w\Vdash\varphi for all w∈Ww\in W. A formula φ\varphi is valid in an epistemic frame ℱ\mathcal{F} if ℱ,V⊩φ\mathcal{F},V\Vdash\varphi for all valuations VV.

Epistemic logic 𝖤𝖫\mathsf{EL} is the set of ℒ𝖤𝖫\mathcal{L}_{\mathsf{EL}}-formulas that are valid on the class of all epistemic frames. Public announcement logic 𝖯𝖠𝖫\mathsf{PAL} is the set of ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-formulas that are valid on the class of all epistemic frames.

𝖤𝖫\mathsf{EL} is axiomatized by (Tau), (K), (4), (T), (5), (MP) and (GKa). 𝖯𝖠𝖫\mathsf{PAL} is axiomatized by the axiomatization for 𝖤𝖫\mathsf{EL} plus reduction axioms (R1–6):

(Tau) Classical propositional tautologies.
(K) Ka​(φ→ψ)→(Ka​φ→Ka​ψ)K_{a}(\varphi\to\psi)\to(K_{a}\varphi\to K_{a}\psi)
(4) Ka​φ→Ka​Ka​φK_{a}\varphi\to K_{a}K_{a}\varphi
(T) Ka​φ→φK_{a}\varphi\to\varphi
(5) ¬Ka​φ→Ka​¬Ka​φ\neg K_{a}\varphi\to K_{a}\neg K_{a}\varphi
(MP) From φ\varphi and φ→ψ\varphi\to\psi infer ψ\psi.
(GKa) From φ\varphi infer Ka​φK_{a}\varphi.
(R1) [φ]​p↔(φ→p)[\varphi]p\leftrightarrow(\varphi\to p)
(R2) [φ]​¬ψ↔(φ→¬[φ]​ψ)[\varphi]\neg\psi\leftrightarrow(\varphi\to\neg[\varphi]\psi)
(R3) [φ]​(ψ∧χ)↔([φ]​ψ∧[φ]​χ)[\varphi](\psi\wedge\chi)\leftrightarrow([\varphi]\psi\wedge[\varphi]\chi)
(R4) [φ]​(ψ→χ)↔([φ]​ψ→[φ]​χ)[\varphi](\psi\to\chi)\leftrightarrow([\varphi]\psi\to[\varphi]\chi)
(R5) [φ]​Ka​ψ↔(φ→Ka​[φ]​ψ)[\varphi]K_{a}\psi\leftrightarrow(\varphi\to K_{a}[\varphi]\psi)
(R6) [φ]​[ψ]​χ↔[φ∧[φ]​ψ]​χ[\varphi][\psi]\chi\leftrightarrow[\varphi\wedge[\varphi]\psi]\chi
Remark 1

The standard language for 𝖯𝖠𝖫\mathsf{PAL} does not contain →\to. To simplify our writing, we add →\to to our language. Because of its existence, (R4)\mathrm{(R4)} is added to the axiomatization.

2.2 Labelled sequent calculus

A labelled sequent calculus for a logic with Kripke semantics is based on the internalization of Kripke semantics.

Let ℱ=(W,{∼a}a∈𝖠𝗀)\mathcal{F}=(W,\{\sim_{a}\}_{a\in\mathsf{Ag}}) be an epistemic frame. A relational atom is of the form x∼ayx\sim_{a}y, where x,y∈Wx,y\in W and a∈𝖠𝗀a\in\mathsf{Ag}. A labelled formula is of the form x:φx:\varphi, where x∈Wx\in W and φ\varphi is an ℒ𝖤𝖫\mathcal{L}_{\mathsf{EL}}-formula. We use σ,δ\sigma,\delta with or without subscript to denote relational atoms or labelled formulas.

A multiset is a ‘set with multiplicity’, or put the other way round, a sequence modulo the ordering. A labelled sequent is of the form Γ⇒Δ\Gamma\Rightarrow\Delta where Γ,Δ\Gamma,\Delta are finite multisets of relational atoms and labelled formulas. A sequent rule is of the form

(ℛ)​Γ1⇒Δ1​…​Γm⇒ΔmΓ⇒Δ(\mathcal{R})~{}\frac{\Gamma_{1}\Rightarrow\Delta_{1}~{}\ldots~{}\Gamma_{m}\Rightarrow\Delta_{m}}{\Gamma\Rightarrow\Delta}

where m≥0m\geq 0. Γ1⇒Δ1,…,Γm⇒Δm\Gamma_{1}\Rightarrow\Delta_{1},\ldots,\Gamma_{m}\Rightarrow\Delta_{m} are called premises of this rule and Γ⇒Δ\Gamma\Rightarrow\Delta is called the conclusion. If m=0m=0, we simply write Γ⇒Δ\Gamma\Rightarrow\Delta and call it an initial sequent. The formula with the connective in a rule is the principal formula of that rule, and its components in the premisses are the active formulas. A labelled sequent calculus is a set of sequent rules. A derivation in a labelled sequent calculus GG is defined as usual. The derivation height h of a sequent is defined as the length of longest branch in the derivation of the sequent. We use G⊢Γ⇒ΔG\vdash\Gamma\Rightarrow\Delta to denote that Γ⇒Δ\Gamma\Rightarrow\Delta is derivable in GG and G⊢hΓ⇒ΔG\vdash_{h}\Gamma\Rightarrow\Delta to denote that Γ⇒Δ\Gamma\Rightarrow\Delta is derivable in GG with a derivation the height of which is at most hh.

A sequent rule (ℛ)(\mathcal{R}) is admissible in GG if G⊢Γi⇒ΔiG\vdash\Gamma_{i}\Rightarrow\Delta_{i} for 1≤i≤m1\leq i\leq m implies G⊢Γ⇒ΔG\vdash\Gamma\Rightarrow\Delta. It is height-preserving admissible if G⊢hΓi⇒ΔiG\vdash_{h}\Gamma_{i}\Rightarrow\Delta_{i} for 1≤i≤m1\leq i\leq m implies G⊢hΓ⇒ΔG\vdash_{h}\Gamma\Rightarrow\Delta.

Let ℳ=(W,{∼a}a∈𝖠𝗀,V)\mathcal{M}=(W,\{\sim_{a}\}_{a\in\mathsf{Ag}},V) be an epistemic model. The interpretation τℳ\tau_{\mathcal{M}} of relational atoms and labelled formulas are defined as follows:

τℳ​(x∼ay)\displaystyle\tau_{\mathcal{M}}(x\sim_{a}y) =\displaystyle\quad=\quad x∼ay;\displaystyle x\sim_{a}y;
τℳ(x:φ)\displaystyle\tau_{\mathcal{M}}(x:\varphi) =\displaystyle\quad=\quad ℳ,x⊩φ.\displaystyle\mathcal{M},x\Vdash\varphi.

A labelled sequent σ1,…,σm⇒δ1,…,δn\sigma_{1},\ldots,\sigma_{m}\Rightarrow\delta_{1},\ldots,\delta_{n} is valid if

∀ℳ​∀x1​…​∀xk​[τℳ​(σ1)∧…∧τℳ​(σm)→τℳ​(δ1)∨…∨τℳ​(δn)]\forall\mathcal{M}\forall x_{1}\ldots\forall x_{k}[\tau_{\mathcal{M}}(\sigma_{1})\land\ldots\land\tau_{\mathcal{M}}(\sigma_{m})\to\tau_{\mathcal{M}}(\delta_{1})\lor\ldots\lor\tau_{\mathcal{M}}(\delta_{n})]

is true, where ℳ=(W,{∼a}a∈𝖠𝗀,V)\mathcal{M}=(W,\{\sim_{a}\}_{a\in\mathsf{Ag}},V) is an epistemic model, and x1,…,xkx_{1},\ldots,x_{k} are variables occurring in σ1,…,σm⇒δ1,…,δn\sigma_{1},\ldots,\sigma_{m}\Rightarrow\delta_{1},\ldots,\delta_{n} ranging over WW.

A sequent rule ℛ\mathcal{R} is valid if the validity of all the premises implies the validity of the conclusion.

Given a labelled sequent calculus GG and a logic Λ\Lambda, we say GG is a labelled sequent calculus for Λ\Lambda if for all φ\varphi, G⊢⇒φG\vdash{}\Rightarrow\varphi if and only if φ∈Λ\varphi\in\Lambda.

2.3 Labelled sequent calculus for 𝖤𝖫\mathsf{EL}

Definition 2

Labelled sequent calculus G𝖤𝖫G_{\mathsf{EL}} for 𝖤𝖫\mathsf{EL} consists of the following initial sequents and rules111It is mentioned without proof in [9] that this is a labelled sequent calculus for 𝖤𝖫\mathsf{EL}. This calculus is a multi-agent version of the labelled sequent calculus for 𝖲​5\mathsf{S}5 proposed in [14].:

(1) Initial sequents:

x:p,Γ⇒Δ,x:p\displaystyle x:p,\Gamma\Rightarrow\Delta,x:p x∼ay,Γ⇒Δ,x∼ay\displaystyle x\sim_{a}y,\Gamma\Rightarrow\Delta,x\sim_{a}y

(2) Propositional rules:

(¬⇒)Γ⇒Δ,x:φx:¬φ,Γ⇒Δ\displaystyle(\neg{\Rightarrow})~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi}{x:\neg\varphi,\Gamma\Rightarrow\Delta} (⇒¬)x:φ,Γ⇒ΔΓ⇒Δ,x:¬φ\displaystyle({\Rightarrow}\neg)~{}\frac{x:\varphi,\Gamma\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,x:\neg\varphi}
(∧⇒)x:φ1,x:φ2,Γ⇒Δx:φ1∧φ2,Γ⇒Δ\displaystyle(\land\!\Rightarrow)~{}\frac{x:\varphi_{1},x:\varphi_{2},\Gamma\Rightarrow\Delta}{x:\varphi_{1}\land\varphi_{2},\Gamma\Rightarrow\Delta} (⇒∧)Γ⇒Δ,x:φ1Γ⇒Δ,x:φ2Γ⇒Δ,x:φ1∧φ2\displaystyle(\Rightarrow\!\land)~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi_{1}\quad\Gamma\Rightarrow\Delta,x:\varphi_{2}}{\Gamma\Rightarrow\Delta,x:\varphi_{1}\land\varphi_{2}}
(→⇒)Γ⇒Δ,x:φx:ψ,Γ⇒Δx:φ→ψ,Γ⇒Δ\displaystyle(\to\Rightarrow)~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi\quad x:\psi,\Gamma\Rightarrow\Delta}{x:\varphi\to\psi,\Gamma\Rightarrow\Delta} (⇒→)x:φ,Γ⇒Δ,x:ψΓ⇒Δ,x:φ→ψ\displaystyle(\Rightarrow\to)~{}\frac{x:\varphi,\Gamma\Rightarrow\Delta,x:\psi}{\Gamma\Rightarrow\Delta,x:\varphi\to\psi}

(3) Modal rules:

(Ka⇒)y:φ,x:Kaφ,x∼ay,Γ⇒Δx:Kaφ,x∼ay,Γ⇒Δ\displaystyle(K_{a}\Rightarrow)~{}\frac{y:\varphi,x:K_{a}\varphi,x\sim_{a}y,\Gamma\Rightarrow\Delta}{x:K_{a}\varphi,x\sim_{a}y,\Gamma\Rightarrow\Delta} (⇒Ka)x∼ay,Γ⇒Δ,y:φΓ⇒Δ,x:Ka​φ\displaystyle(\Rightarrow K_{a})~{}\frac{x\sim_{a}y,\Gamma\Rightarrow\Delta,y:\varphi}{\Gamma\Rightarrow\Delta,x:K_{a}\varphi}

where yy does not occur in the conclusion of (⇒Ka)(\Rightarrow K_{a}), .

(4) Relational rules:

(Refa)​x∼ax,Γ⇒ΔΓ⇒Δ\displaystyle(\text{Ref}_{a})~{}\frac{x\sim_{a}x,\Gamma\Rightarrow\Delta}{\Gamma\Rightarrow\Delta} (Transa)​x∼az,x∼ay,y∼az,Γ⇒Δx∼ay,y∼az,Γ⇒Δ\displaystyle(\text{Trans}_{a})~{}\frac{x\sim_{a}z,x\sim_{a}y,y\sim_{a}z,\Gamma\Rightarrow\Delta}{x\sim_{a}y,y\sim_{a}z,\Gamma\Rightarrow\Delta}
(Syma)​y∼ax,x∼ay,Γ⇒Δx∼ay,Γ⇒Δ\displaystyle(\text{Sym}_{a})~{}\frac{y\sim_{a}x,x\sim_{a}y,\Gamma\Rightarrow\Delta}{x\sim_{a}y,\Gamma\Rightarrow\Delta}
Proposition 3

For any ℒ𝖤𝖫\mathcal{L}_{\mathsf{EL}}-formula φ\varphi, G𝖤𝖫⊢x:φ,Γ⇒Δ,x:φG_{\mathsf{EL}}\vdash x:\varphi,\Gamma\Rightarrow\Delta,x:\varphi.

Proof

It can be proved by induction on φ\varphi.

By proofs similar to those in [14], we have Theorems 4 and 5.

Theorem 4

Structural rules (w⇒)(w\Rightarrow), (⇒w)(\Rightarrow w), (c⇒)(c\Rightarrow), (⇒c)(\Rightarrow c), (cR⇒)(c_{R}\Rightarrow) and (⇒cR)(\Rightarrow c_{R}) are height-preserving admissible in G𝖤𝖫G_{\mathsf{EL}}. The cut rule (C​u​t)(Cut) is admissible in G𝖤𝖫G_{\mathsf{EL}}.

(w⇒)Γ⇒Δx:φ,Γ⇒Δ\displaystyle(w\Rightarrow)~{}\frac{\Gamma\Rightarrow\Delta}{x:\varphi,\Gamma\Rightarrow\Delta} (⇒w)Γ⇒ΔΓ⇒Δ,x:φ\displaystyle(\Rightarrow w)~{}\frac{\Gamma\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,x:\varphi}
(c⇒)x:φ,x:φ,Γ⇒Δx:φ,Γ⇒Δ\displaystyle(c\Rightarrow)~{}\frac{x:\varphi,x:\varphi,\Gamma\Rightarrow\Delta}{x:\varphi,\Gamma\Rightarrow\Delta} (⇒c)Γ⇒Δ,x:φ,x:φΓ⇒Δ,x:φ\displaystyle(\Rightarrow c)~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi,x:\varphi}{\Gamma\Rightarrow\Delta,x:\varphi}
(cR⇒)x∼ay,x∼ay,Γ⇒Δx∼ay,Γ⇒Δ\displaystyle(c_{R}\Rightarrow)~{}\frac{x\sim_{a}y,x\sim_{a}y,\Gamma\Rightarrow\Delta}{x\sim_{a}y,\Gamma\Rightarrow\Delta} (⇒cR)Γ⇒Δ,x∼ay,x∼ayΓ⇒Δ,x∼ay\displaystyle(\Rightarrow c_{R})~{}\frac{\Gamma\Rightarrow\Delta,x\sim_{a}y,x\sim_{a}y}{\Gamma\Rightarrow\Delta,x\sim_{a}y}
(C​u​t)​Γ⇒Δ,x:φx:φ,Γ′⇒Δ′Γ,Γ′⇒Δ,Δ′\displaystyle(Cut)~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi\quad x:\varphi,\Gamma^{\prime}\Rightarrow\Delta^{\prime}}{\Gamma,\Gamma^{\prime}\Rightarrow\Delta,\Delta^{\prime}}
Theorem 5

G𝖤𝖫G_{\mathsf{EL}} allows terminating proof search.

Example 6

A derivation for axiom (5)(5) in G𝖤𝖫G_{\mathsf{EL}} is as follows:

  z:φ,y:Kaφ,y∼az,x∼az,y∼ax,x∼ay⇒z:φz:\varphi,y:K_{a}\varphi,y\sim_{a}z,x\sim_{a}z,y\sim_{a}x,x\sim_{a}y\Rightarrow z:\varphi    (Ka⇒)(K_{a}\Rightarrow)       y:Kaφ,y∼az,x∼az,y∼ax,x∼ay⇒z:φy:K_{a}\varphi,y\sim_{a}z,x\sim_{a}z,y\sim_{a}x,x\sim_{a}y\Rightarrow z:\varphi        (T​r​a​na)(Tran_{a})           y:Kaφ,x∼az,y∼ax,x∼ay⇒z:φy:K_{a}\varphi,x\sim_{a}z,y\sim_{a}x,x\sim_{a}y\Rightarrow z:\varphi            (S​y​ma)(Sym_{a})                y:Kaφ,x∼az,x∼ay⇒z:φy:K_{a}\varphi,x\sim_{a}z,x\sim_{a}y\Rightarrow z:\varphi               (⇒¬)(\Rightarrow\neg)              x∼az,x∼ay⇒y:¬Ka​φ,z:φx\sim_{a}z,x\sim_{a}y\Rightarrow y:\neg K_{a}\varphi,z:\varphi               (⇒Ka)(\Rightarrow K_{a})                 x∼ay⇒y:¬Ka​φ,x:Ka​φx\sim_{a}y\Rightarrow y:\neg K_{a}\varphi,x:K_{a}\varphi                  (⇒Ka)(\Rightarrow K_{a})                   ⇒x:Ka​¬Ka​φ,x:Ka​φ\Rightarrow x:K_{a}\neg K_{a}\varphi,x:K_{a}\varphi                   (¬⇒)(\neg\Rightarrow)                  x:¬Ka​φ⇒x:Ka​¬Ka​φx:\neg K_{a}\varphi\Rightarrow x:K_{a}\neg K_{a}\varphi                   (⇒→)(\Rightarrow\to)                   ⇒x:¬Ka​φ→Ka​¬Ka​φ\Rightarrow x:\neg K_{a}\varphi\to K_{a}\neg K_{a}\varphi

3 Labelled sequent calculus for 𝖯𝖠𝖫\mathsf{PAL}

In this section, we introduce a labelled sequent calculus for 𝖯𝖠𝖫\mathsf{PAL}. The Hilbert-style axiomatization for 𝖯𝖠𝖫\mathsf{PAL} is the extension of that for 𝖤𝖫\mathsf{EL} with reduction axioms. Can we obtain a labelled sequent calculus for 𝖯𝖠𝖫\mathsf{PAL} by adding some rules adapted from reduction axioms to the labelled sequent calculus G𝖤𝖫G_{\mathsf{EL}} for 𝖤𝖫\mathsf{EL}? The answer is yes and this is what we do.

Take reduction axiom (R1)[φ]​p↔(φ→p)[\varphi]p\leftrightarrow(\varphi\to p) as an example. The equivalence symbol in the axiom means that [φ]​p[\varphi]p and φ→p\varphi\to p are equivalent in 𝖯𝖠𝖫\mathsf{PAL}. Therefore, the most direct sequent rules for (R1) are

x:φ→p,Γ⇒Δx:[φ]​p,Γ⇒Δ​ and ​Γ⇒Δ,x:φ→pΓ⇒Δ,x:[φ]​p\frac{x:\varphi\to p,\Gamma\Rightarrow\Delta}{x:[\varphi]p,\Gamma\Rightarrow\Delta}\text{~{}~{}~{}and~{}~{}~{}}\frac{\Gamma\Rightarrow\Delta,x:\varphi\to p}{\Gamma\Rightarrow\Delta,x:[\varphi]p}

The rule on the left is sound because of [φ]​p→(φ→p)[\varphi]p\to(\varphi\to p) and the rule on the right is sound because of (φ→p)→[φ]​p(\varphi\to p)\to[\varphi]p. These rules can be written in a more neat way if we see φ→p,Γ⇒Δ\varphi\to p,\Gamma\Rightarrow\Delta as the conclusion of an application of (→⇒)(\to\Rightarrow) and Γ⇒Δ,φ→p\Gamma\Rightarrow\Delta,\varphi\to p as the conclusion of an application of (⇒→)(\Rightarrow\to). Applying the reverse of (→⇒)(\to\Rightarrow) and (⇒→)(\Rightarrow\to) to their premises, we have the rules for (R1) that will be added to G𝖤𝖫G_{\mathsf{EL}}:

Γ⇒Δ,x:φx:p,Γ⇒Δx:[φ]​p,Γ⇒Δ​ and ​x:φ,Γ⇒Δ,pΓ⇒Δ,x:[φ]​p\frac{\Gamma\Rightarrow\Delta,x:\varphi\quad x:p,\Gamma\Rightarrow\Delta}{x:[\varphi]p,\Gamma\Rightarrow\Delta}\text{~{}~{}~{}and~{}~{}~{}}\frac{x:\varphi,\Gamma\Rightarrow\Delta,p}{\Gamma\Rightarrow\Delta,x:[\varphi]p}

In a similar way, we can have sequent rules for other reduction axioms. Therefore, we have:

Definition 7

Labelled sequent calculus G𝖯𝖠𝖫G_{\mathsf{PAL}} for 𝖯𝖠𝖫\mathsf{PAL} is G𝖤𝖫G_{\mathsf{EL}} plus the following sequent rules:

(R1⇒)Γ⇒Δ,x:φ​x:p,Γ⇒Δx:[φ]​p,Γ⇒Δ\displaystyle\small{(R1\!\Rightarrow)~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi\quad x:p,\Gamma\Rightarrow\Delta}{x:[\varphi]p,\Gamma\Rightarrow\Delta}} (⇒R1)x:φ,Γ⇒Δ,x:pΓ⇒Δ,x:[φ]​p\displaystyle\small{(\Rightarrow\!R1)~{}\frac{x:\varphi,\Gamma\Rightarrow\Delta,x:p}{\Gamma\Rightarrow\Delta,x:[\varphi]p}}
(R2⇒)Γ⇒Δ,x:φx:¬[φ]​ψ,Γ⇒Δx:[φ]​¬ψ,Γ⇒Δ\displaystyle(R2\Rightarrow)~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi\quad x:\neg[\varphi]\psi,\Gamma\Rightarrow\Delta}{x:[\varphi]\neg\psi,\Gamma\Rightarrow\Delta} (⇒R2)x:φ,Γ⇒Δ,x:¬[φ]ψΓ⇒Δ,x:[φ]​¬ψ\displaystyle(\Rightarrow R2)~{}\frac{x:\varphi,\Gamma\Rightarrow\Delta,x:\neg[\varphi]\psi}{\Gamma\Rightarrow\Delta,x:[\varphi]\neg\psi}
(R3⇒)x:[φ]​ψ1,x:[φ]​ψ2,Γ⇒Δx:[φ]​(ψ1∧ψ2),Γ⇒Δ\displaystyle(R3\Rightarrow)~{}\frac{x:[\varphi]\psi_{1},x:[\varphi]\psi_{2},\Gamma\Rightarrow\Delta}{x:[\varphi](\psi_{1}\land\psi_{2}),\Gamma\Rightarrow\Delta} (⇒R3)Γ⇒Δ,x:[φ]ψ1Γ⇒Δ,x:[φ]ψ2Γ⇒Δ,x:[φ]​(ψ1∧ψ2)\displaystyle(\Rightarrow R3)~{}\frac{\Gamma\Rightarrow\Delta,x:[\varphi]\psi_{1}\quad\Gamma\Rightarrow\Delta,x:[\varphi]\psi_{2}}{\Gamma\Rightarrow\Delta,x:[\varphi](\psi_{1}\land\psi_{2})}
(R4⇒)Γ⇒Δ,x:[φ]​ψ1x:[φ]​ψ2,Γ⇒Δx:[φ]​(ψ1→ψ2),Γ⇒Δ\displaystyle(R4\Rightarrow)~{}\frac{\Gamma\Rightarrow\Delta,x:[\varphi]\psi_{1}\quad x:[\varphi]\psi_{2},\Gamma\Rightarrow\Delta}{x:[\varphi](\psi_{1}\to\psi_{2}),\Gamma\Rightarrow\Delta} (⇒R4)x:[φ]ψ1,Γ⇒Δ,x:[φ]ψ2Γ⇒Δ,[φ]​(ψ1→ψ2)\displaystyle(\Rightarrow R4)~{}\frac{x:[\varphi]\psi_{1},\Gamma\Rightarrow\Delta,x:[\varphi]\psi_{2}}{\Gamma\Rightarrow\Delta,[\varphi](\psi_{1}\to\psi_{2})}
(R5⇒)Γ⇒Δ,x:φKa​[φ]​ψ,Γ⇒Δx:[φ]​Ka​ψ,Γ⇒Δ\displaystyle(R5\Rightarrow)~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi\quad K_{a}[\varphi]\psi,\Gamma\Rightarrow\Delta}{x:[\varphi]K_{a}\psi,\Gamma\Rightarrow\Delta} (⇒R5)x:φ,Γ⇒Δ,x:Ka[φ]ψΓ⇒Δ,x:[φ]​Ka​ψ\displaystyle(\Rightarrow R5)~{}\frac{x:\varphi,\Gamma\Rightarrow\Delta,x:K_{a}[\varphi]\psi}{\Gamma\Rightarrow\Delta,x:[\varphi]K_{a}\psi}
(R6⇒)x:[φ∧[φ]​ψ]​χ,Γ⇒Δx:[φ]​[ψ]​χ,Γ⇒Δ\displaystyle(R6\Rightarrow)~{}\frac{x:[\varphi\wedge[\varphi]\psi]\chi,\Gamma\Rightarrow\Delta}{x:[\varphi][\psi]\chi,\Gamma\Rightarrow\Delta} (⇒R6)Γ⇒Δ,x:[φ∧[φ]​ψ]​χΓ⇒Δ,x:[φ]​[ψ]​χ\displaystyle(\Rightarrow R6)\frac{\Gamma\Rightarrow\Delta,x:[\varphi\wedge[\varphi]\psi]\chi}{\Gamma\Rightarrow\Delta,x:[\varphi][\psi]\chi}

We call these sequent rules the reduction rules.

There are six pairs of reduction rules in G𝖯𝖠𝖫G_{\mathsf{PAL}}, each pair dealing with a kind of announcement formulas. Each left rule introduces a formula on the left of ⇒\Rightarrow, and each right rule introduces one on the right of ⇒\Rightarrow. Another desirable property for sequent rules is that the complexity of each premise should be less than that of the conclusion. If we define the complexity of a sequent to be the the sum of relational atoms and labelled formulas occurring in it, then the definition of formula complexity that counts the number of connectives will make (R5) and (R6) fail to satisfy the complexity increasing property. The following definition for formula complexity can solve this problem222This is Definition 7.21 in [7].:

Definition 8

Let φ\varphi be an ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}} formula, The complexity c​(φ)c(\varphi) of φ\varphi is defined as follows:

c​(p)=1c(p)=1 c​(φ→ψ)=1+max⁡{c​(φ),c​(ψ)}c(\varphi\to\psi)=1+\max{\{c(\varphi),c(\psi)\}}
c​(¬φ)=1+c​(φ)c(\neg\varphi)=1+c(\varphi) c​(Ka​φ)=1+c​(φ)c(K_{a}\varphi)=1+c(\varphi)
c​(φ∧ψ)=1+max⁡{c​(φ),c​(ψ)}c(\varphi\land\psi)=1+\max{\{c(\varphi),c(\psi)\}} c​([φ]​ψ)=(4+c​(φ))⋅c​(ψ)c([\varphi]\psi)=(4+c(\varphi))\cdot c(\psi).

Then we have the following lemma333This is Lemma 7.22 in [7].:

Lemma 9

For all ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-formulas φ,ψ\varphi,\psi and χ\chi:

  1. (1)

    c​([φ]​p)>c​(φ→p)c([\varphi]p)>c(\varphi\to p);

  2. (2)

    c​([φ]​¬ψ)>c​(φ→¬[φ]​ψ)c([\varphi]\neg\psi)>c(\varphi\to\neg[\varphi]\psi);

  3. (3)

    c​([φ]​(ψ∧χ))>c​([φ]​ψ∧[φ]​χ)c([\varphi](\psi\land\chi))>c([\varphi]\psi\land[\varphi]\chi);

  1. (4)

    c​([φ]​Ka​ψ)>c​(φ→Ka​[φ]​ψ)c([\varphi]K_{a}\psi)>c(\varphi\to K_{a}[\varphi]\psi);

  2. (5)

    c​([φ]​[ψ]​χ)>c​([φ∧[φ]​ψ]​χ)c([\varphi][\psi]\chi)>c([\varphi\land[\varphi]\psi]\chi).

Lemma 10

For any ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-formula φ\varphi, G𝖯𝖠𝖫⊢x:φ,Γ⇒Δ,x:φG_{\mathsf{PAL}}\vdash x:\varphi,\Gamma\Rightarrow\Delta,x:\varphi.

Proof
Proof

We prove this by induction on the structure of φ\varphi with a subinduction on ψ\psi of the inductive case where φ\varphi equals [φ]​ψ[\varphi]\psi. All inductive case not involving announcement are the same as in the proof of Proposition 3. When φ\varphi involves a public announcement operator, there are 6 subcases. We show two representative cases.

When φ=[ϕ]​Ka​ψ\varphi=[\phi]K_{a}\psi, the derivation is as follows:

  x:ϕ,Γ⇒Δ,x:Ka[ϕ]ψ,x:ϕx:\phi,\Gamma\Rightarrow\Delta,x:K_{a}[\phi]\psi,x:\phi         x:Ka[ϕ]ψ,x:ϕ,Γ⇒Δ,x:Ka[ϕ]ψx:K_{a}[\phi]\psi,x:\phi,\Gamma\Rightarrow\Delta,x:K_{a}[\phi]\psi    (R5⇒)(R5\Rightarrow)                          x:ϕ,x:[ϕ]Kaψ,Γ⇒Δ,x:Ka[ϕ]ψx:\phi,x:[\phi]K_{a}\psi,\Gamma\Rightarrow\Delta,x:K_{a}[\phi]\psi                           (⇒R​5)(\Rightarrow R5)                              x:[ϕ]Kaψ,Γ⇒Δ,x:[ϕ]Kaψx:[\phi]K_{a}\psi,\Gamma\Rightarrow\Delta,x:[\phi]K_{a}\psi

When φ=[ϕ]​[χ]​ψ\varphi=[\phi][\chi]\psi, the derivation is as follows:

  x:[ϕ∧[χ]ψ],Γ⇒Δ,x:[ϕ∧[ϕ]χ]ψx:[\phi\land[\chi]\psi],\Gamma\Rightarrow\Delta,x:[\phi\land[\phi]\chi]\psi    (R6⇒)(R6\Rightarrow)     x:[ϕ][χ]ψ,Γ⇒Δ,x:[ϕ∧[ϕ]χ]ψx:[\phi][\chi]\psi,\Gamma\Rightarrow\Delta,x:[\phi\land[\phi]\chi]\psi      (⇒R​6)(\Rightarrow R6)        x:[ϕ][χ]ψ,Γ⇒Δ,x:[ϕ][χ]ψx:[\phi][\chi]\psi,\Gamma\Rightarrow\Delta,x:[\phi][\chi]\psi

Other cases can be proved analogously.

Example 11

Now we show that (R​5)​[φ]​Ka​ψ↔(φ→Ka​[φ]​ψ)(R5)[\varphi]K_{a}\psi\leftrightarrow(\varphi\to K_{a}[\varphi]\psi) is derivable in G𝖯𝖠𝖫G_{\mathsf{PAL}}. A derivation for [φ]​Ka​ψ→(φ→Ka​[φ]​ψ)[\varphi]K_{a}\psi\to(\varphi\to K_{a}[\varphi]\psi) in G𝖯𝖠𝖫G_{\mathsf{PAL}} is as follows:

  x∼ay,x:φ⇒y:[φ]​ψ,x:φx\sim_{a}y,x:\varphi\Rightarrow y:[\varphi]\psi,x:\varphi          y:[φ]ψ,x:Ka[φ]ψ,x∼ay,x:φ⇒y:[φ]ψy:[\varphi]\psi,x:K_{a}[\varphi]\psi,x\sim_{a}y,x:\varphi\Rightarrow y:[\varphi]\psi    (Ka⇒)(K_{a}\!\Rightarrow)         x:Ka[φ]ψ,x∼ay,x:φ⇒y:[φ]ψx:K_{a}[\varphi]\psi,x\sim_{a}y,x:\varphi\Rightarrow y:[\varphi]\psi    (R5⇒)(R5\Rightarrow)                            x∼ay,x:[φ]​Ka​ψ,x:φ⇒y:[φ]​ψx\sim_{a}y,x:[\varphi]K_{a}\psi,x:\varphi\Rightarrow y:[\varphi]\psi                             (⇒Ka)(\Rightarrow K_{a})                              x:[φ]​Ka​ψ,x:φ⇒x:Ka​[φ]​ψx:[\varphi]K_{a}\psi,x:\varphi\Rightarrow x:K_{a}[\varphi]\psi                               (⇒→)(\Rightarrow\to)                                x:[φ]​Ka​ψ⇒x:φ→Ka​[φ]​ψx:[\varphi]K_{a}\psi\Rightarrow x:\varphi\to K_{a}[\varphi]\psi                                (⇒→)(\Rightarrow\to)                               ⇒x:[φ]​Ka​ψ→(φ→Ka​[φ]​ψ)\Rightarrow x:[\varphi]K_{a}\psi\to(\varphi\to K_{a}[\varphi]\psi)

A derivation for (φ→Ka​[φ]​ψ)→[φ]​Ka​ψ(\varphi\to K_{a}[\varphi]\psi)\to[\varphi]K_{a}\psi in G𝖯𝖠𝖫G_{\mathsf{PAL}} is as follows:

  x:φ⇒x:Ka​[φ]​ψ,x:φx:\varphi\Rightarrow x:K_{a}[\varphi]\psi,x:\varphi         x:Ka​[φ]​ψ,x:φ⇒x:Ka​[φ]​ψx:K_{a}[\varphi]\psi,x:\varphi\Rightarrow x:K_{a}[\varphi]\psi    (→⇒)(\to\Rightarrow)                    x:φ,x:φ→Ka​[φ]​ψ⇒x:Ka​[φ]​ψx:\varphi,x:\varphi\to K_{a}[\varphi]\psi\Rightarrow x:K_{a}[\varphi]\psi                     (⇒R​5)(\Rightarrow R5)                        x:φ→Ka​[φ]​ψ⇒x:[φ]​Ka​ψx:\varphi\to K_{a}[\varphi]\psi\Rightarrow x:[\varphi]K_{a}\psi                        (⇒→)(\Rightarrow\to)                       ⇒x:(φ→Ka[φ]ψ)→[φ]Kaψ)\Rightarrow x:(\varphi\to K_{a}[\varphi]\psi)\to[\varphi]K_{a}\psi)
Example 1

[p∧¬Ka​p]​¬Ka​p[p\land\neg K_{a}p]\neg K_{a}p is not derivable in G𝖯𝖠𝖫G_{\mathsf{PAL}}.

                       𝒟0\mathcal{D}_{0}     x∼ay,x:Ka​[p∧¬Ka​p]​p,x:p⇒y:px\sim_{a}y,x:K_{a}[p\land\neg K_{a}p]p,x:p\Rightarrow y:p    (⇒Ka)(\Rightarrow K_{a})      x:Ka​[p∧¬Ka​p]​p,x:p⇒x:Ka​px:K_{a}[p\land\neg K_{a}p]p,x:p\Rightarrow x:K_{a}p        x:p⇒x:p∧¬Ka​p,x:Ka​px:p\Rightarrow x:p\land\neg K_{a}p,x:K_{a}p                                     x:[p∧¬Ka​p]​Ka​p,x:p⇒x:Ka​px:[p\land\neg K_{a}p]K_{a}p,x:p\Rightarrow x:K_{a}p                               (¬⇒)(\neg\Rightarrow)                              x:[p∧¬Ka​p]​Ka​p,x:p,x:¬Ka​p⇒x:[p\land\neg K_{a}p]K_{a}p,x:p,x:\neg K_{a}p\Rightarrow                               (∧⇒,⇒¬)(\land\Rightarrow,\Rightarrow\neg)                               x:p∧¬Ka​p⇒x:¬[p∧¬Ka​p]​Ka​px:p\land\neg K_{a}p\Rightarrow x:\neg[p\land\neg K_{a}p]K_{a}p                                                                    ⇒x:[p∧¬Ka​p]​¬Ka​p\Rightarrow x:[p\land\neg K_{a}p]\neg K_{a}p

where 𝒟0\mathcal{D}_{0} is:

  x∼ay,x:p⇒y:p,y:px\sim_{a}y,x\!:\!p\Rightarrow y\!:\!p,y\!:\!p            y:Kap,x∼ay,x:p⇒y:py\!:\!K_{a}p,x\sim_{a}y,x\!:\!p\Rightarrow y\!:\!p     x∼ay,x:p⇒y:p,y:¬Ka​px\sim_{a}y,x\!:\!p\Rightarrow y\!:\!p,y\!:\!\neg K_{a}p                    x∼ay,x:p⇒y:p,y:p∧¬Ka​px\sim_{a}y,x\!:\!p\Rightarrow y\!:\!p,y\!:\!p\land\neg K_{a}p        y:p,x∼ay,x:p⇒y:py\!:\!p,x\sim_{a}y,x\!:\!p\Rightarrow y\!:\!p                                                         y:[p∧¬Kap]p,x∼ay,x:p⇒y:py\!:\![p\land\neg K_{a}p]p,x\sim_{a}y,x\!:\!p\Rightarrow y\!:\!p                                                                           x∼ay,x:Ka​[p∧¬Ka​p]​p,x:p⇒y:px\sim_{a}y,x\!:\!K_{a}[p\land\neg K_{a}p]p,x\!:\!p\Rightarrow y\!:\!p

4 Admissibility of some structural rules

In light of the reduction axioms, we can define a translation from ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-formulas to ℒ𝖤𝖫\mathcal{L}_{\mathsf{EL}}-formulas444This is Definition 7.20 in [7]..

Definition 12

The translation t:ℒ𝖯𝖠𝖫→ℒ𝖤𝖫t:\mathcal{L}_{\mathsf{PAL}}\to\mathcal{L}_{\mathsf{EL}} is defined as follows:

t​(p)=pt​(¬φ)=¬t​(φ)t​(φ∧ψ)=t​(φ)∧t​(ψ)t​(φ→ψ)=t​(φ)→t​(ψ)t​(Ka​φ)=Ka​t​(φ)\begin{aligned} &t(p)&=\quad&p\\ &t(\neg\varphi)&=\quad&\neg t(\varphi)\\ &t(\varphi\land\psi)&=\quad&t(\varphi)\land t(\psi)\\ &t(\varphi\to\psi)&=\quad&t(\varphi)\to t(\psi)\\ &t(K_{a}\varphi)&=\quad&K_{a}t(\varphi)\\ \end{aligned} t​([φ]​p)=t​(φ→p)t​([φ]​¬ψ)=t​(φ→¬[φ]​ψ)t​([φ]​(ψ∧χ))=t​([φ]​ψ∧[φ]​χ)t​([φ]​(ψ→χ))=t​([φ]​ψ→[φ]​χ)t​([φ]​Ka​ψ)=t​(φ→Ka​[φ]​ψ)t​([φ]​[ψ]​χ)=t​([φ∧[φ]​ψ]​χ)\begin{aligned} &t([\varphi]p)&=\quad&t(\varphi\to p)\\ &t([\varphi]\neg\psi)&=\quad&t(\varphi\to\neg[\varphi]\psi)\\ &t([\varphi](\psi\land\chi))&=\quad&t([\varphi]\psi\land[\varphi]\chi)\\ &t([\varphi](\psi\to\chi))&=\quad&t([\varphi]\psi\to[\varphi]\chi)\\ &t([\varphi]K_{a}\psi)&=\quad&t(\varphi\to K_{a}[\varphi]\psi)\\ &t([\varphi][\psi]\chi)&=\quad&t([\varphi\land[\varphi]\psi]\chi)\par\end{aligned}

Now we extend translation tt to relational atoms and labelled ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-formulas: for any relational atom x∼ayx\sim_{a}y, let t​(x∼ay)=x∼ayt(x\sim_{a}y)=x\sim_{a}y; for any labelled ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-formula x:φx:\varphi, t(x:φ)=x:t(φ)t(x:\varphi)=x:t(\varphi). Moreover, for any set Γ\Gamma of relational atoms and labelled formulas: t​(Γ)={t​(σ)∣σ∈Γ}t(\Gamma)=\{t(\sigma)\mid\sigma\in\Gamma\}.

Lemma 13

For any ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-sequent x:φ,Γ⇒Δx:\varphi,\Gamma\Rightarrow\Delta, the following hold:

  1. (1)

    if G𝖯𝖠𝖫⊢x:t​(φ),t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:t(\varphi),t(\Gamma)\Rightarrow t(\Delta), then G𝖯𝖠𝖫⊢x:φ,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:\varphi,t(\Gamma)\Rightarrow t(\Delta);

  2. (2)

    if G𝖯𝖠𝖫⊢t​(Γ)⇒t​(Δ),x:t​(φ)G_{\mathsf{PAL}}\vdash t(\Gamma)\Rightarrow t(\Delta),x:t(\varphi), then G𝖯𝖠𝖫⊢t​(Γ)⇒t​(Δ),x:φG_{\mathsf{PAL}}\vdash t(\Gamma)\Rightarrow t(\Delta),x:\varphi.

Proof

We prove these claims simultaneously by induction on the height of derivation hh of G𝖯𝖠𝖫⊢x:t​(φ),t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:t(\varphi),t(\Gamma)\Rightarrow t(\Delta) (or G𝖯𝖠𝖫⊢t​(Γ)⇒t​(Δ),x:t​(φ)G_{\mathsf{PAL}}\vdash t(\Gamma)\Rightarrow t(\Delta),x:t(\varphi)).

If h=1h=1, then x:t​(φ),t​(Γ)⇒t​(Δ)x:t(\varphi),t(\Gamma)\Rightarrow t(\Delta) (or t​(Γ)⇒t​(Δ),x:t​(φ)t(\Gamma)\Rightarrow t(\Delta),x:t(\varphi)) is an initial sequent. If x:t​(φ)x:t(\varphi) is principal, then t​(φ)=pt(\varphi)=p for some proposition letter pp. It follows that φ=p\varphi=p. Therefore, x:φ,t​(Γ)⇒t​(Δ)x:\varphi,t(\Gamma)\Rightarrow t(\Delta) (or t​(Γ)⇒t​(Δ),x:φt(\Gamma)\Rightarrow t(\Delta),x:\varphi) is also an initial sequent. If x:t​(φ)x:t(\varphi) is not principal, it is immediate that x:φ,t​(Γ)⇒t​(Δ)x:\varphi,t(\Gamma)\Rightarrow t(\Delta) (or t​(Γ)⇒t​(Δ),x:φt(\Gamma)\Rightarrow t(\Delta),x:\varphi) is an initial sequent.

If h>1h>1, the induction hypothesis is formulated as:

(1)′(1)^{\prime}for all i<hi<h, if G𝖯𝖠𝖫⊢ix:t(φ),t(Γ)⇒t(Δ)G_{\mathsf{PAL}}\vdash_{i}x:t(\varphi),t(\Gamma)\Rightarrow t(\Delta), then G𝖯𝖠𝖫⊢x:φ,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:\varphi,t(\Gamma)\Rightarrow t(\Delta);

(2)′(2)^{\prime}for all i<hi<h, if G𝖯𝖠𝖫⊢it(Γ)⇒t(Δ),x:t(φ)G_{\mathsf{PAL}}\vdash_{i}t(\Gamma)\Rightarrow t(\Delta),x:t(\varphi), then G𝖯𝖠𝖫⊢t​(Γ)⇒t​(Δ),x:φG_{\mathsf{PAL}}\vdash t(\Gamma)\Rightarrow t(\Delta),x:\varphi.

In what follows we only give the proof for claim (1)′(1)^{\prime}. The proof for the other claim is similar.

Assume that G𝖯𝖠𝖫⊢hx:t(φ),t(Γ)⇒t(Δ)G_{\mathsf{PAL}}\vdash_{h}x:t(\varphi),t(\Gamma)\Rightarrow t(\Delta). Then there exists a derivation 𝒟\mathcal{D} for x:t​(φ),t​(Γ)⇒t​(Δ)x:t(\varphi),t(\Gamma)\Rightarrow t(\Delta) in G𝖯𝖠𝖫G_{\mathsf{PAL}}. Let the last rule applied in dd be ℛ\mathcal{R}. If x:t​(φ)x:t(\varphi) is not principal in the application of ℛ\mathcal{R}, the desired result can be obtained by applying the induction hypothesis to the premise(s) of ℛ\mathcal{R} and then applying ℛ\mathcal{R}.

If x:t​(φ)x:t(\varphi) is principal in the application of ℛ\mathcal{R}, we prove by an sub-induction on the complexity c​(φ)c(\varphi) of φ\varphi. Since x:t​(φ)x:t(\varphi) is principal and h>1h>1, φ\varphi is not a proposition letter. We have ten sub-cases. We divide them into two groups depending on whether φ\varphi starts with an announcement operator or not.

If φ\varphi does not start with an announcement operator, the desired result can be obtained by applying the induction hypothesis to the premise(s) of ℛ\mathcal{R} and then applying ℛ\mathcal{R}. There are four sub-cases: φ\varphi is of the form ¬ψ\neg\psi, ψ1∧ψ2\psi_{1}\land\psi_{2}, ψ1→ψ2\psi_{1}\to\psi_{2} or Ka​ψK_{a}\psi. We illustrate this by the cases ¬ψ\neg\psi and Ka​ψK_{a}\psi.

  • •

    If φ=¬ψ\varphi=\neg\psi, then ℛ\mathcal{R} is (¬⇒)(\neg\!\Rightarrow). Note that t​(φ)=t​(¬ψ)=¬t​(ψ)t(\varphi)=t(\neg\psi)=\neg t(\psi). Let the derivation 𝒟\mathcal{D} end with

        t​(Γ)⇒t​(Δ),x:t​(ψ)t(\Gamma)\Rightarrow t(\Delta),x:t(\psi)    (¬⇒)(\neg\!\Rightarrow)   x:¬t​(ψ),t​(Γ)⇒t​(Δ)x:\neg t(\psi),t(\Gamma)\Rightarrow t(\Delta)

    By the induction hypothesis, we have G𝖯𝖠𝖫⊢t​(Γ)⇒t​(Δ),x:ψG_{\mathsf{PAL}}\vdash t(\Gamma)\Rightarrow t(\Delta),x:\psi. Then by (¬⇒)(\neg\!\Rightarrow) we have G𝖯𝖠𝖫⊢x:¬ψ,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:\neg\psi,t(\Gamma)\Rightarrow t(\Delta).

  • •

    If φ=Ka​ψ\varphi=K_{a}\psi, then ℛ\mathcal{R} is (Ka⇒)(K_{a}\Rightarrow). Note that t​(φ)=t​(Ka​ψ)=Ka​t​(ψ)t(\varphi)=t(K_{a}\psi)=K_{a}t(\psi). Let the derivation 𝒟\mathcal{D} end with

      y:t(ψ),x:Kat(ψ),x∼ay,t(Γ)⇒t(Δ)y:t(\psi),x:K_{a}t(\psi),x\sim_{a}y,t(\Gamma)\Rightarrow t(\Delta)    (Ka⇒)(K_{a}\Rightarrow)         x:Kat(ψ),x∼ay,t(Γ)⇒t(Δ)x:K_{a}t(\psi),x\sim_{a}y,t(\Gamma)\Rightarrow t(\Delta)

    First apply the main induction hypothesis to x:Ka​t​(ψ)x:K_{a}t(\psi) and we have G𝖯𝖠𝖫⊢y:t(ψ),x:Kaψ,x∼ay,t(Γ)⇒t(Δ)G_{\mathsf{PAL}}\vdash y:t(\psi),x:K_{a}\psi,x\sim_{a}y,t(\Gamma)\Rightarrow t(\Delta). Then apply the sub-induction hypothesis to y:t​(ψ)y:t(\psi) and we have G𝖯𝖠𝖫⊢y:ψ,x:Kaψ,x∼ay,t(Γ)⇒t(Δ)G_{\mathsf{PAL}}\vdash y:\psi,x:K_{a}\psi,x\sim_{a}y,t(\Gamma)\Rightarrow t(\Delta). Finally by (Ka⇒)(K_{a}\Rightarrow) we have G𝖯𝖠𝖫⊢x:Kaψ,x∼ay,t(Γ)⇒t(Δ)G_{\mathsf{PAL}}\vdash x:K_{a}\psi,x\sim_{a}y,t(\Gamma)\Rightarrow t(\Delta).

If φ\varphi starts with an announcement operator, then there are six sub-cases: φ\varphi is [ϕ]​p[\phi]p, [ϕ]​¬ψ[\phi]\neg\psi, [ϕ]​(ψ1∧ψ2)[\phi](\psi_{1}\land\psi_{2}), [ϕ]​(ψ1→ψ2)[\phi](\psi_{1}\to\psi_{2}), [ϕ]​Ka​ψ[\phi]K_{a}\psi or [ϕ]​[ψ]​χ[\phi][\psi]\chi.

If φ\varphi is [ϕ]​p[\phi]p, [ϕ]​¬ψ[\phi]\neg\psi, [ϕ]​(ψ1→ψ2)[\phi](\psi_{1}\to\psi_{2}) or [ϕ]​Ka​ψ[\phi]K_{a}\psi, then t​(φ)t(\varphi) is t​(ϕ)→pt(\phi)\to p, t​(ϕ)→t​(¬[ϕ]​ψ)t(\phi)\to t(\neg[\phi]\psi), t​([ϕ]​ψ1)→t​([ϕ]​ψ2)t([\phi]\psi_{1})\to t([\phi]\psi_{2}), or t​(ϕ)→t​(Ka​[ϕ]​ψ)t(\phi)\to t(K_{a}[\phi]\psi), respectively. Since x:t​(φ)x:t(\varphi) is principal, ℛ\mathcal{R} must be (→⇒)(\to\Rightarrow).We substitute the application of (→⇒)(\to\Rightarrow) with an application of (R1⇒)(R1\Rightarrow), (R2⇒)(R_{2}\Rightarrow), (R4⇒)(R_{4}\Rightarrow) and (R5⇒)(R_{5}\Rightarrow), respectively. We illustrate the proof by the case where φ\varphi is [ϕ]​¬ψ[\phi]\neg\psi and the case where φ\varphi is [ϕ]​Ka​ψ[\phi]K_{a}\psi.

  • •

    If φ\varphi is [ϕ]​¬ψ[\phi]\neg\psi, then the derivation 𝒟\mathcal{D} ends with

      t​(Γ)⇒t​(Δ),x:t​(ϕ)t(\Gamma)\Rightarrow t(\Delta),x:t(\phi)         x:t​(¬[ϕ]​ψ),t​(Γ)⇒t​(Δ)x:t(\neg[\phi]\psi),t(\Gamma)\Rightarrow t(\Delta)    (→⇒)(\to\Rightarrow)                x:t​(ϕ)→t​(¬[ϕ]​ψ),t​(Γ)⇒t​(Δ)x:t(\phi)\to t(\neg[\phi]\psi),t(\Gamma)\Rightarrow t(\Delta)

    Apply the induction hypothesis to the premises and we have G𝖯𝖠𝖫⊢t​(Γ)⇒t​(Δ),ϕG_{\mathsf{PAL}}\vdash t(\Gamma)\Rightarrow t(\Delta),\phi and G𝖯𝖠𝖫⊢¬[ϕ]​ψ,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash\neg[\phi]\psi,t(\Gamma)\Rightarrow t(\Delta). Then by (R2⇒)(R2\Rightarrow) we have G𝖯𝖠𝖫⊢x:[ϕ]​¬ψ,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:[\phi]\neg\psi,t(\Gamma)\Rightarrow t(\Delta).

  • •

    If φ\varphi is [ϕ]​Ka​ψ[\phi]K_{a}\psi, then the derivation 𝒟\mathcal{D} ends with

      t​(Γ)⇒t​(Δ),x:t​(ϕ)t(\Gamma)\Rightarrow t(\Delta),x:t(\phi)         x:t​(Ka​[ϕ]​ψ),t​(Γ)⇒t​(Δ)x:t(K_{a}[\phi]\psi),t(\Gamma)\Rightarrow t(\Delta)    (→⇒)(\to\Rightarrow)                x:t​(ϕ)→t​(Ka​[ϕ]​ψ),t​(Γ)⇒t​(Δ)x:t(\phi)\to t(K_{a}[\phi]\psi),t(\Gamma)\Rightarrow t(\Delta)

    Apply the induction hypothesis to the premises and we have G𝖯𝖠𝖫⊢t​(Γ)⇒t​(Δ),ϕG_{\mathsf{PAL}}\vdash t(\Gamma)\Rightarrow t(\Delta),\phi and G𝖯𝖠𝖫⊢Ka​[ϕ]​ψ,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash K_{a}[\phi]\psi,t(\Gamma)\Rightarrow t(\Delta). Then by (R5⇒)(R5\Rightarrow) we have G𝖯𝖠𝖫⊢x:[ϕ]​Ka​ψ,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:[\phi]K_{a}\psi,t(\Gamma)\Rightarrow t(\Delta).

If φ\varphi is [ϕ]​(ψ1∧ψ2)[\phi](\psi_{1}\land\psi_{2}), then t​(φ)t(\varphi) is t​([ϕ]​ψ1)∧t​([ϕ]​ψ2)t([\phi]\psi_{1})\land t([\phi]\psi_{2}). Since x:t​(φ)x:t(\varphi) is principal, ℛ\mathcal{R} must be (∧⇒)(\land\!\Rightarrow). We substitute the application of (∧⇒)(\land\!\Rightarrow) with an application of (R3⇒)(R3\Rightarrow). Let the derivation 𝒟\mathcal{D} end with

  x:t​([ϕ]​ψ1),x:t​([ϕ]​ψ2),t​(Γ)⇒t​(Δ)x:t([\phi]\psi_{1}),x:t([\phi]\psi_{2}),t(\Gamma)\Rightarrow t(\Delta)    (∧⇒)(\land\Rightarrow)    x:t​([ϕ]​ψ1)∧t​([ϕ]​ψ2),t​(Γ)⇒t​(Δ)x:t([\phi]\psi_{1})\land t([\phi]\psi_{2}),t(\Gamma)\Rightarrow t(\Delta)

Apply the sub-induction hypothesis to the premise twice and we have G𝖯𝖠𝖫⊢x:[ϕ]​ψ1,x:[ϕ]​ψ2,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:[\phi]\psi_{1},x:[\phi]\psi_{2},t(\Gamma)\Rightarrow t(\Delta). Then by (R3⇒)(R3\Rightarrow) we have G𝖯𝖠𝖫⊢x:[ϕ]​(ψ1∧ψ2),t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:[\phi](\psi_{1}\land\psi_{2}),t(\Gamma)\Rightarrow t(\Delta).

If φ\varphi is [ϕ]​[ψ]​χ[\phi][\psi]\chi, by assumption, G𝖯𝖠𝖫⊢x:t​([ϕ]​[ψ]​χ),t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:t([\phi][\psi]\chi),t(\Gamma)\Rightarrow t(\Delta). Since t​([ϕ]​[ψ]​χ)=t​([ϕ∧[ϕ]​ψ]​χ)t([\phi][\psi]\chi)=t([\phi\land[\phi]\psi]\chi), G𝖯𝖠𝖫⊢x:t​([ϕ∧[ϕ]​ψ]​χ),t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:t([\phi\land[\phi]\psi]\chi),t(\Gamma)\Rightarrow t(\Delta). Since c​([ϕ∧[ϕ]​ψ]​χ)<c​([ϕ]​[ψ]​χ)c([\phi\land[\phi]\psi]\chi)<c([\phi][\psi]\chi), by the sub-induction hypothesis, we have G𝖯𝖠𝖫⊢x:[ϕ∧[ϕ]​ψ]​χ,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:[\phi\land[\phi]\psi]\chi,t(\Gamma)\Rightarrow t(\Delta). Then by (R6⇒)(R6\Rightarrow), G𝖯𝖠𝖫⊢x:[ϕ]​[ψ]​χ,t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash x:[\phi][\psi]\chi,t(\Gamma)\Rightarrow t(\Delta).

This completes the proof.

The following theorem is a bridge between G𝖯𝖠𝖫G_{\mathsf{PAL}} and G𝖤𝖫G_{\mathsf{EL}}, enabling us to prove properties of G𝖯𝖠𝖫G_{\mathsf{PAL}} through G𝖤𝖫G_{\mathsf{EL}}.

Theorem 14

For any ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-sequent Γ⇒Δ\Gamma\Rightarrow\Delta,

  1. (1)

    if G𝖤𝖫⊢t​(Γ)⇒t​(Δ)G_{\mathsf{EL}}\vdash t(\Gamma)\Rightarrow t(\Delta), then G𝖯𝖠𝖫⊢Γ⇒ΔG_{\mathsf{PAL}}\vdash\Gamma\Rightarrow\Delta;

  2. (2)

    if G𝖯𝖠𝖫⊢hΓ⇒ΔG_{\mathsf{PAL}}\vdash_{h}\Gamma\Rightarrow\Delta, then G𝖤𝖫⊢ht(Γ)⇒t(Δ)G_{\mathsf{EL}}\vdash_{h}t(\Gamma)\Rightarrow t(\Delta).

Proof

(1) Assume that G𝖤𝖫⊢t​(Γ)⇒t​(Δ)G_{\mathsf{EL}}\vdash t(\Gamma)\Rightarrow t(\Delta). Since G𝖯𝖠𝖫G_{\mathsf{PAL}} is an extension of G𝖤𝖫G_{\mathsf{EL}}, G𝖯𝖠𝖫⊢t​(Γ)⇒t​(Δ)G_{\mathsf{PAL}}\vdash t(\Gamma)\Rightarrow t(\Delta). Since t​(Γ)⇒t​(Δ)t(\Gamma)\Rightarrow t(\Delta) is finite, applying Lemma 13 a finite number of times, we have G𝖯𝖠𝖫⊢Γ⇒ΔG_{\mathsf{PAL}}\vdash\Gamma\Rightarrow\Delta.

(2) Prove by induction on hh.

If h=1h=1, then Γ⇒Δ\Gamma\Rightarrow\Delta is an initial sequent in G𝖯𝖠𝖫G_{\mathsf{PAL}}. By definition, it is also an initial sequent in G𝖤𝖫G_{\mathsf{EL}}.

If h>1h>1, we consider the last rule ℛ\mathcal{R} applied in the derivation. If ℛ\mathcal{R} is not a reduction rule, the claim can be proved by first applying the induction hypothesis to the premise(s) and then applying ℛ\mathcal{R}.

If ℛ\mathcal{R} is a reduction rule for (R1), (R2), (R4) or (R5), we apply the induction hypothesis to the premise(s), and then apply (→⇒)(\to\Rightarrow) or (⇒→)(\Rightarrow\to). We illustrate this by a few cases.

If ℛ\mathcal{R} is (R1⇒)(R1\Rightarrow), let the derivation end with:

  Γ′⇒Δ,x:φ\Gamma^{\prime}\Rightarrow\Delta,x:\varphi         x:p,Γ′⇒Δx:p,\Gamma^{\prime}\Rightarrow\Delta    (R1⇒)(R1\Rightarrow)             x:[φ]​p,Γ′⇒Δx:[\varphi]p,\Gamma^{\prime}\Rightarrow\Delta

By the induction hypothesis, we have G𝖤𝖫⊢h−1t(Γ′)⇒t(Δ),x:t(φ)G_{\mathsf{EL}}\vdash_{h-1}t(\Gamma^{\prime})\Rightarrow t(\Delta),x:t(\varphi) and G𝖤𝖫⊢h−1x:t(p),t(Γ′)⇒t(Δ)G_{\mathsf{EL}}\vdash_{h-1}x:t(p),t(\Gamma^{\prime})\Rightarrow t(\Delta). We proceed as follows:

  t​(Γ′)⇒t​(Δ),x:t​(φ)t(\Gamma^{\prime})\Rightarrow t(\Delta),x:t(\varphi)         x:t​(p),t​(Γ′)⇒t​(Δ)x:t(p),t(\Gamma^{\prime})\Rightarrow t(\Delta)    (→⇒)(\to\Rightarrow)                x:t​(φ)→t​(p),t​(Γ′)⇒t​(Δ)x:t(\varphi)\to t(p),t(\Gamma^{\prime})\Rightarrow t(\Delta)

Since t(x:[φ]p)=x:t(φ)→t(p)t(x:[\varphi]p)=x:t(\varphi)\to t(p), we have

G𝖤𝖫⊢ht(x:[φ]p),t(Γ′)⇒t(Δ).G_{\mathsf{EL}}\vdash_{h}t(x:[\varphi]p),t(\Gamma^{\prime})\Rightarrow t(\Delta).

If ℛ\mathcal{R} is (⇒R​2)(\Rightarrow R2), let the derivation end with:

  x:φ,Γ⇒Δ′,x:¬[φ]ψx:\varphi,\Gamma\Rightarrow\Delta^{\prime},x:\neg[\varphi]\psi    (⇒R​2)(\Rightarrow R2)       Γ⇒Δ′,x:[φ]​¬ψ\Gamma\Rightarrow\Delta^{\prime},x:[\varphi]\neg\psi

By the induction hypothesis, we have G𝖤𝖫⊢h−1x:t(φ),t(Γ)⇒t(Δ′),x:t(¬[φ]ψ)G_{\mathsf{EL}}\vdash_{h-1}x:t(\varphi),t(\Gamma)\Rightarrow t(\Delta^{\prime}),x:t(\neg[\varphi]\psi). We proceed as follows:

  x:t(φ),t(Γ)⇒t(Δ′),x:t(¬[φ]ψ)x:t(\varphi),t(\Gamma)\Rightarrow t(\Delta^{\prime}),x:t(\neg[\varphi]\psi)    (⇒→)(\Rightarrow\to)    t​(Γ)⇒t​(Δ′),x:t​(φ)→t​(¬[φ]​ψ)t(\Gamma)\Rightarrow t(\Delta^{\prime}),x:t(\varphi)\to t(\neg[\varphi]\psi)

Since t(x:[φ]¬ψ)=x:t(φ)→t(¬[φ]ψ)t(x:[\varphi]\neg\psi)=x:t(\varphi)\to t(\neg[\varphi]\psi), we have

G𝖤𝖫⊢ht(Γ)⇒t(Δ′),t(x:[φ]¬p).G_{\mathsf{EL}}\vdash_{h}t(\Gamma)\Rightarrow t(\Delta^{\prime}),t(x:[\varphi]\neg p).

If ℛ\mathcal{R} is (R5⇒)(R5\Rightarrow), let the derivation end with:

  Γ′⇒Δ,x:φ\Gamma^{\prime}\Rightarrow\Delta,x:\varphi         x:Ka​[φ]​ψ,Γ′⇒Δx:K_{a}[\varphi]\psi,\Gamma^{\prime}\Rightarrow\Delta    (R5⇒)(R5\Rightarrow)               x:[φ]​Ka​ψ,Γ′⇒Δx:[\varphi]K_{a}\psi,\Gamma^{\prime}\Rightarrow\Delta

By the induction hypothesis, we have G𝖤𝖫⊢h−1t(Γ′)⇒t(Δ),x:t(φ)G_{\mathsf{EL}}\vdash_{h-1}t(\Gamma^{\prime})\Rightarrow t(\Delta),x:t(\varphi) and G𝖤𝖫⊢h−1x:t(Ka[φ]ψ),t(Γ′)⇒t(Δ)G_{\mathsf{EL}}\vdash_{h-1}x:t(K_{a}[\varphi]\psi),t(\Gamma^{\prime})\Rightarrow t(\Delta). We proceed as follows:

  t​(Γ′)⇒t​(Δ),x:t​(φ)t(\Gamma^{\prime})\Rightarrow t(\Delta),x:t(\varphi)         x:t​(Ka​[φ]​ψ),t​(Γ′)⇒t​(Δ)x:t(K_{a}[\varphi]\psi),t(\Gamma^{\prime})\Rightarrow t(\Delta)    (→⇒)(\to\Rightarrow)                x:t​(φ)→t​(Ka​[φ]​ψ),t​(Γ′)⇒t​(Δ)x:t(\varphi)\to t(K_{a}[\varphi]\psi),t(\Gamma^{\prime})\Rightarrow t(\Delta)

Since t(x:[φ]Kaψ)=x:t(φ)→t(Ka[φ]ψ)t(x:[\varphi]K_{a}\psi)=x:t(\varphi)\to t(K_{a}[\varphi]\psi), we have

G𝖤𝖫⊢ht(x:[φ]Kaψ),t(Γ′)⇒t(Δ).G_{\mathsf{EL}}\vdash_{h}t(x:[\varphi]K_{a}\psi),t(\Gamma^{\prime})\Rightarrow t(\Delta).

If ℛ\mathcal{R} is a reduction rule for (R3), we apply the induction hypothesis to the premise(s), and then apply an inference rule for ∧\land. We illustrate this by the case where ℛ\mathcal{R} is (R3⇒)(R3\Rightarrow).

If ℛ\mathcal{R} is (R3⇒)(R3\Rightarrow), let the derivation end with:

  x:[φ]​ψ1,x:[φ]​ψ2,Γ′⇒Δx:[\varphi]\psi_{1},x:[\varphi]\psi_{2},\Gamma^{\prime}\Rightarrow\Delta    (R3⇒)(R3\Rightarrow)     x:[φ]​(ψ1∧ψ2),Γ′⇒Δx:[\varphi](\psi_{1}\land\psi_{2}),\Gamma^{\prime}\Rightarrow\Delta

By induction hypothesis, we have G𝖤𝖫⊢h−1x:t([φ]ψ1),x:t([φ]ψ2),t(Γ′)⇒t(Δ)G_{\mathsf{EL}}\vdash_{h-1}x:t([\varphi]\psi_{1}),x:t([\varphi]\psi_{2}),t(\Gamma^{\prime})\Rightarrow t(\Delta). We proceed as follows:

  x:t​([φ]​ψ1),x:t​([φ]​ψ2),t​(Γ′)⇒t​(Δ)x:t([\varphi]\psi_{1}),x:t([\varphi]\psi_{2}),t(\Gamma^{\prime})\Rightarrow t(\Delta)    (∧⇒)(\land\Rightarrow)    x:t​([φ]​ψ1)∧t​([φ]​ψ2),t​(Γ′)⇒t​(Δ)x:t([\varphi]\psi_{1})\land t([\varphi]\psi_{2}),t(\Gamma^{\prime})\Rightarrow t(\Delta)

Since t(x:[φ](ψ1∧ψ2))=x:t([φ]ψ1)∧t([φ]ψ2)t(x:[\varphi](\psi_{1}\land\psi_{2}))=x:t([\varphi]\psi_{1})\land t([\varphi]\psi_{2}), we have

G𝖤𝖫⊢ht(x:[φ](ψ1∧ψ2)),t(Γ′)⇒t(Δ).G_{\mathsf{EL}}\vdash_{h}t({x:{[\varphi](\psi_{1}\land\psi_{2})}}),t(\Gamma^{\prime})\Rightarrow t(\Delta).

If ℛ\mathcal{R} is a reduction rule for (R6), then we simply apply the induction hypothesis to the premise.

Thus completes the proof.

Remark 15

Since 𝖯𝖠𝖫\mathsf{PAL} is more succinct than 𝖤𝖫\mathsf{EL} (see [11, 8]), one might expect that a derivation of a sequent Γ⇒Δ\Gamma\Rightarrow\Delta in G𝖯𝖠𝖫G_{\mathsf{PAL}} is strictly shorter (with respect to derivation height) than a derivation of t​(Γ)⇒t​(Δ)t(\Gamma)\Rightarrow t(\Delta) in G𝖤𝖫G_{\mathsf{EL}}. This is not the case for G𝖯𝖠𝖫G_{\mathsf{PAL}} and G𝖤𝖫G_{\mathsf{EL}} as shown in Theorem 14. This is because a derivation for Γ⇒Δ\Gamma\Rightarrow\Delta in G𝖯𝖠𝖫G_{\mathsf{PAL}} is obtained by executing the translation function tt (encoded by the reduction rules) in a derivation for t​(Γ)⇒t​(Δ)t(\Gamma)\Rightarrow t(\Delta) in G𝖤𝖫G_{\mathsf{EL}}, which increases the length of the derivation.

Corollary 16

The following structural rules are admissible in G𝖯𝖠𝖫G_{\mathsf{PAL}}:

(w⇒)Γ⇒Δx:φ,Γ⇒Δ\displaystyle(w\Rightarrow)~{}\frac{\Gamma\Rightarrow\Delta}{x:\varphi,\Gamma\Rightarrow\Delta} (⇒w)Γ⇒ΔΓ⇒Δ,x:φ\displaystyle(\Rightarrow w)~{}\frac{\Gamma\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,x:\varphi}
(c⇒)x:φ,x:φ,Γ⇒Δx:φ,Γ⇒Δ\displaystyle(c\Rightarrow)~{}\frac{x:\varphi,x:\varphi,\Gamma\Rightarrow\Delta}{x:\varphi,\Gamma\Rightarrow\Delta} (⇒c)Γ⇒Δ,x:φ,x:φΓ⇒Δ,x:φ\displaystyle(\Rightarrow c)~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi,x:\varphi}{\Gamma\Rightarrow\Delta,x:\varphi}
(cR⇒)x∼ay,x∼ay,Γ⇒Δx∼ay,Γ⇒Δ\displaystyle(c_{R}\Rightarrow)~{}\frac{x\sim_{a}y,x\sim_{a}y,\Gamma\Rightarrow\Delta}{x\sim_{a}y,\Gamma\Rightarrow\Delta} (⇒cR)Γ⇒Δ,x∼ay,x∼ayΓ⇒Δ,x∼ay\displaystyle(\Rightarrow c_{R})~{}\frac{\Gamma\Rightarrow\Delta,x\sim_{a}y,x\sim_{a}y}{\Gamma\Rightarrow\Delta,x\sim_{a}y}
(C​u​t)​Γ⇒Δ,x:φx:φ,Γ′⇒Δ′Γ,Γ′⇒Δ,Δ′\displaystyle(Cut)~{}\frac{\Gamma\Rightarrow\Delta,x:\varphi\quad x:\varphi,\Gamma^{\prime}\Rightarrow\Delta^{\prime}}{\Gamma,\Gamma^{\prime}\Rightarrow\Delta,\Delta^{\prime}}
Proof

It follows directly from Theorem 4 and Theorem 14. Take (C​u​t)(Cut) as an example. Assume that G𝖯𝖠𝖫⊢Γ⇒Δ,x:φG_{\mathsf{PAL}}\vdash\Gamma\Rightarrow\Delta,x:\varphi and x:φ,Γ′⇒Δ′x:\varphi,\Gamma^{\prime}\Rightarrow\Delta^{\prime}. By Theorem 14, G𝖤𝖫⊢t​(Γ)⇒t​(Δ),x:t​(φ)G_{\mathsf{EL}}\vdash t(\Gamma)\Rightarrow t(\Delta),x:t(\varphi) and G𝖤𝖫⊢x:t​(φ),t​(Γ′)⇒t​(Δ′)G_{\mathsf{EL}}\vdash x:t(\varphi),t(\Gamma^{\prime})\Rightarrow t(\Delta^{\prime}). Then by admissibility of cut in G𝖤𝖫G_{\mathsf{EL}} (Theorem 4), G𝖤𝖫⊢t(Γ),t(Γ′)⇒t(Δ),t(Δ′)G_{\mathsf{EL}}\vdash t(\Gamma),t(\Gamma^{\prime})\Rightarrow t(\Delta),t(\Delta^{\prime}). By Theorem 14 again, G𝖯𝖠𝖫⊢Γ,Γ′⇒Δ,Δ′G_{\mathsf{PAL}}\vdash\Gamma,\Gamma^{\prime}\Rightarrow\Delta,\Delta^{\prime}.

Theorem 17 (Soundness and Completeness)

For any ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-formula φ\varphi, φ∈𝖯𝖠𝖫\varphi\in\mathsf{PAL} iff G𝖯𝖠𝖫⊢⇒φG_{\mathsf{PAL}}\vdash\Rightarrow\varphi.

Proof

For the left-to-right direction, it suffices to show that each axiom in the Hilbert-style axiomatization for 𝖯𝖠𝖫\mathsf{PAL} is derivable in G𝖯𝖠𝖫G_{\mathsf{PAL}} and that (MP) and (GKa) are admissible in G𝖯𝖠𝖫G_{\mathsf{PAL}}. Since G𝖯𝖠𝖫G_{\mathsf{PAL}} is an extension of G𝖤𝖫G_{\mathsf{EL}}, derivability of axioms in 𝖤𝖫\mathsf{EL}. Admissibility of (MP) follows from admissibility of cut in G𝖯𝖠𝖫G_{\mathsf{PAL}} (Corollary 16). Admissibility of (GK)a{}_{a}) in G𝖯𝖠𝖫G_{\mathsf{PAL}} follows from admissibility of (GK)a{}_{a}) in G𝖤𝖫G_{\mathsf{EL}} and Theorem 14. For the reduction axioms, since each reduction axiom has a corresponding pair of sequent rules in G𝖯𝖠𝖫G_{\mathsf{PAL}}, their derivations can be obtained by direct root-first search. One derivation of (R5) is given in Example 11.

For the right-to-left direction, it suffices to show that each sequent rule in G𝖯𝖠𝖫G_{\mathsf{PAL}} is valid. This is routine. We omit the proof here.

5 Decidability

In this section we show that G𝖯𝖠𝖫G_{\mathsf{PAL}} allows terminating proof search. This result can be proved indirectly by Theorems 5 and 14. In this section we present a direct proof.

Readers familiar with the proof for terminating proof search in G𝖤𝖫G_{\mathsf{EL}} may notice that the proof for terminating proof search in G𝖯𝖠𝖫G_{\mathsf{PAL}} is essentially the same as that in G𝖤𝖫G_{\mathsf{EL}} because G𝖯𝖠𝖫G_{\mathsf{PAL}} is an extension of G𝖤𝖫G_{\mathsf{EL}} with some reduction rules. For this reason, we sketch the proof in this section and refer to [14] for a detailed description.

To show that G𝖯𝖠𝖫G_{\mathsf{PAL}} allows terminating proof search, first we extend the notion of subformulas for ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-formulas, because active formulas are not subformulas of the principal formula in the usual sense in the reduction rules of G𝖯𝖠𝖫G_{\mathsf{PAL}}.

Definition 18

Let φ\varphi be a ℒ𝖯𝖠𝖫\mathcal{L}_{\mathsf{PAL}}-formula. Formula ψ\psi is called a semi-subformula of φ\varphi if one of the following conditions hold:

  1. (1)

    ψ\psi is a subformula of φ\varphi;

  2. (2)

    φ=[ϕ]∗χ\varphi=[\phi]\ast\chi and ψ=∗[ϕ]χ\psi=\ast[\phi]\chi, where ∗∈{¬,Ka}\ast\in\{\neg,K_{a}\};

  3. (3)

    φ=[ϕ]​(χ1⋆χ2)\varphi=[\phi](\chi_{1}\star\chi_{2}) and ψ=[ϕ]​χ1\psi=[\phi]\chi_{1} or ψ=[ϕ]​χ2\psi=[\phi]\chi_{2}, where ⋆∈{∧,→}\star\in\{\land,\to\};

  4. (4)

    φ=[ϕ]​[χ]​ξ\varphi=[\phi][\chi]\xi and ψ=[ϕ∧[ϕ]​χ]​ξ\psi=[\phi\land[\phi]\chi]\xi.

The set of semi-subformulas of φ\varphi is denoted by S​S​u​b​(φ)SSub(\varphi). We say that ψ\psi is a proper semi-subformula of φ\varphi if ψ\psi is a semi-subformula of φ\varphi and ψ≠φ\psi\not=\varphi.

By Definition 8, the complexity of a proper semi-subformula of φ\varphi is strictly smaller than that of φ\varphi.

Definition 19

A derivation in G𝖯𝖠𝖫G_{\mathsf{PAL}} satisfies the weak subformula property if all expressions in the derivation are either semi-subformulas of formulas φ\varphi in labelled formulas x:φx:\varphi in the endsequent of the derivation, or relational atoms of the form x∼ayx\sim_{a}y.

It is easy to verify that each derivation in G𝖯𝖠𝖫G_{\mathsf{PAL}} satisfies the weak subformula property.

The potential sources of non-terminating proof search in G𝖯𝖠𝖫G_{\mathsf{PAL}} are as follows:

  1. (1)

    (T​r​a​n​sa)(Trans_{a}), (S​y​ma)(Sym_{a}) (read root-first) can be applied infinitely on the same principal formulas.

  2. (2)

    (R​e​fa)(Ref_{a}) (read root-first) can be applied infinitely to introduce new relational atoms.

  3. (3)

    (Ka⇒){(K_{a}\Rightarrow)} (read root-first) can be applied infinitely on the same principal formulas.

  4. (4)

    By (T​r​a​n​sa)(Trans_{a}) and its iteration with (⇒Ka)(\Rightarrow K_{a}) that brings in new accessible worlds, we can build chains of accessible worlds on which (Ka⇒)(K_{a}\Rightarrow) can be applied infinitely.

To show that the space of root-first proof search is finite, it is useful to look at minimal derivations, that is, derivations where shortenings are not possible.

For (1), since no rules, read root first, can change a relational atom, any application of (T​r​a​n​sa)(Trans_{a}) or (S​y​ma)(Sym_{a}) on the same principal formulas will make the derivation fail to be minimal. Therefore, this case should be excluded when searching for minimal derivation.

For (2), we need the following lemma:

Lemma 20

All variables in relational atoms of the form x∼axx\sim_{a}x removed by (R​e​fa)(Ref_{a}) in a minimal derivation of a sequent Γ⇒Δ\Gamma\Rightarrow\Delta in G𝖯𝖠𝖫G_{\mathsf{PAL}} are variables in Γ\Gamma or Δ\Delta.

Proof

It can be proved by tracing the relational atom x∼axx\sim_{a}x up in the derivation. For a detailed proof, see Lemma 6.2 of [14].

For (3), we need to show the following lemma:

Lemma 21

Rule (Ka⇒)(K_{a}\!\Rightarrow) permutes down with respect to (⇒Ka)(\Rightarrow\!K_{a}) in case the principal relational atom of (Ka⇒)(K_{a}\!\Rightarrow) is not active in (⇒Ka)(\Rightarrow\!K_{a}). Moreover, rule (Ka⇒)(K_{a}\!\Rightarrow) permutes down with respect to all other rules.

Then we can prove the following proposition:

Proposition 22

(Ka⇒)(K_{a}\!\Rightarrow) and (⇒Ka)(\Rightarrow\!K_{a}) cannot be applied more than once on the same pair of principal formulas on any branch in any derivation in G𝖯𝖠𝖫G_{\mathsf{PAL}}.

For (4) we need to prove the following proposition:

Proposition 23

In a minimal derivation of a sequent in G𝖯𝖠𝖫G_{\mathsf{PAL}}, for each formula x:Ka​φx:K_{a}\varphi in its positive part there are at most n​(Ka)n(K_{a}) applications of (⇒Ka)(\Rightarrow K_{a}) iterated on a chain of accessible worlds x∼ax1,x1∼ax2,…x\sim_{a}x_{1},x_{1}\sim_{a}x_{2},\ldots with principal formula xi:Ka​φx_{i}:K_{a}\varphi, where n​(Ka)n(K_{a}) denotes the number of KaK_{a} in the negative part of Γ⇒Δ\Gamma\Rightarrow\Delta.

6 Conclusion, comparison and future research

In this paper we proposed a labelled sequent calculus for 𝖯𝖠𝖫\mathsf{PAL}. It is based on a proof system for 𝖤𝖫\mathsf{EL}, namely poly-modal 𝖲𝟧\mathsf{S5}, extended with sequent rules to deal with announcement operators that directly mirror the 𝖯𝖠𝖫\mathsf{PAL} reduction rules. We also determined that the obtained system allows terminating proof search, and compared our system with the calculus for 𝖤𝖫\mathsf{EL} on matters such a height preservation of derivations.

Various proposals for sequent calculi for PAL have been made in [2, 3, 13, 16]. The labelled sequent calculi in [2, 16] for 𝖯𝖠𝖫\mathsf{PAL} are based on a reformulation of the semantics for 𝖯𝖠𝖫\mathsf{PAL}. The notion of a model restriction to a (single) formula is generalized in these works to that of a model restriction to a list of formulas. Denote by α\alpha or β\beta finite lists (φ1,…,φn)(\varphi_{1},\ldots,\varphi_{n}) of formulas, and by ϵ\epsilon the empty list. For any list α=(φ1,…,φn)\alpha=(\varphi_{1},\ldots,\varphi_{n}) of formulas, define ℳα\mathcal{M}^{\alpha} recursively as follows: ℳα:=ℳ\mathcal{M}^{\alpha}:=\mathcal{M} (if α=ϵ)\alpha=\epsilon), and ℳα:=(ℳβ)φn=(Wβ,φn,(∼aβ,φn)a∈𝖠𝗀,Vβ,φn)\mathcal{M}^{\alpha}:=(\mathcal{M}^{\beta})^{\varphi_{n}}=(W^{\beta,\varphi_{n}},(\sim^{\beta,\varphi_{n}}_{a})_{a\in\mathsf{Ag}},V^{\beta,\varphi_{n}}) (if α=β,φn\alpha=\beta,\varphi_{n}).

Then an equivalent semantics for 𝖯𝖠𝖫\mathsf{PAL} is defined as follows:

ℳα,φ,w⊩piffℳα,w⊩φ​ and ​ℳα,w⊩pℳα,w⊩¬φiffℳα,w⊮φℳα,w⊩φ∧ψiffℳα,w⊩φ​and​ℳα,w⊩ψℳα,w⊩φ→ψiffℳα,w⊮φ​or​ℳα,w⊩ψℳα,w⊩Ka​φifffor all​v∈W,w∼aαv​implies​ℳα,v⊩φℳα,w⊩[φ]​ψiffℳα,w⊩φ​implies​ℳα,φ,w⊩ψ\begin{array}[]{lll}\mathcal{M}^{\alpha,\varphi},w\Vdash p&~{}\text{iff}{}&\mathcal{M}^{\alpha},w\Vdash\varphi\text{~{}and~{}}\mathcal{M}^{\alpha},w\Vdash p\\ \mathcal{M}^{\alpha},w\Vdash\neg\varphi&~{}\text{iff}{}&\mathcal{M}^{\alpha},w\nVdash\varphi\\ \mathcal{M}^{\alpha},w\Vdash\varphi\land\psi&~{}\text{iff}{}&\mathcal{M}^{\alpha},w\Vdash\varphi~{}\text{and}~{}\mathcal{M}^{\alpha},w\Vdash\psi\\ \mathcal{M}^{\alpha},w\Vdash\varphi\to\psi&~{}\text{iff}{}&\mathcal{M}^{\alpha},w\nVdash\varphi~{}\text{or}~{}\mathcal{M}^{\alpha},w\Vdash\psi\\ \mathcal{M}^{\alpha},w\Vdash K_{a}\varphi&~{}\text{iff}{}&\text{for~{}all}~{}v\in W,w\sim^{\alpha}_{a}v~{}\text{implies}~{}\mathcal{M}^{\alpha},v\Vdash\varphi\\ \mathcal{M}^{\alpha},w\Vdash[\varphi]\psi&~{}\text{iff}{}&\mathcal{M}^{\alpha},w\Vdash\varphi~{}\text{implies}~{}\mathcal{M}^{\alpha,\varphi},w\Vdash\psi\end{array}

With this semantics, Balbiani [2] and Nomura et al. [16]555Nomura et al. [15] extended the method developed in [16] to action modal logic. developed different labelled sequent calculi for 𝖯𝖠𝖫\mathsf{PAL}, simultaneously repairing some perceived deficiencies in the previously published in Maffezioli and Negri [13]. The calculus in Balbiani [2] admits cut and allows terminating proof search, and the calculus in Nomura et al. [16] also admits cut. Note that these calculi, unlike ours, are for 𝖯𝖠𝖫\mathsf{PAL} based on the normal modal logic 𝖪\mathsf{K}, whereas we took 𝖯𝖠𝖫\mathsf{PAL} as an extension of 𝖲​5\mathsf{S}5 (like [9, 13]). We therefore also include the usual inference rules for 𝖲​5\mathsf{S}5 (i.e., (R​e​fa)(Ref_{a}), (T​r​a​n​sa)(Trans_{a}) and (S​y​ma)(Sym_{a})) into our calculus. Further, our calculus uses sequent rules based on 𝖯𝖠𝖫\mathsf{PAL} reduction axioms to deal with the announcement operators.

This method can be directly applied to action model logic [7] since this logic is also an extension of 𝖤𝖫\mathsf{EL} with some reduction axioms, of which PAL is a special case.

There are many extensions of other logics with public announcement that also involve reduction axioms for such announcements, such as intuitionistic PAL [12], bilattice PAL [18], Łukasiewicz PAL [6], and variations/extensions of action model logic like bilattice logic of epistemic actions and knowledge [1]. We can try to develop calculi for these logics with the steps similar to those for 𝖯𝖠𝖫\mathsf{PAL}.

References

  • [1] Bakhtiari, Z., van Ditmarsch, H., Rivieccio, U.: Bilattice logic of epistemic actions and knowledge. Annals of Pure and Applied Logic 171(6), 102790 (2020)
  • [2] Balbiani, P., Demange, V., Galmiche, D.: A sequent calculus with labels for PAL. In: Advances in Modal Logic (2014)
  • [3] Balbiani, P., van Ditmarsch, H., Herzig, A., De Lima, T.: Tableaux for public announcement logic. Journal of Logic and Computation 20(1), 55–76 (2010)
  • [4] Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcements, common knowledge, and private suspicions. In: Gilboa, I. (ed.) Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge (TARK VII). pp. 43–56. Evanston, Illinois, USA (1998)
  • [5] van Benthem, J.: Logical Dynamics of Information and Interaction. Cambridge University Press (2011)
  • [6] Cabrer, L., Rivieccio, U., Rodriguez, R.O.: Łukasiewicz public announcement logic. In: Information Processing and Management of Uncertainty in Knowledge-Based Systems. pp. 108–122. Springer International Publishing, Cham (2016)
  • [7] van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic, vol. 337. Springer Science & Business Media (2007)
  • [8] French, T., van der Hoek, W., Iliev, P., Kooi, B.: On the succinctness of some modal logics. Artificial Intelligence 197, 56–85 (2013)
  • [9] Hakli, R., Negri, S.: Proof theory for distributed knowledge. In: International Workshop on Computational Logic in Multi-Agent Systems. pp. 100–116. Springer (2007)
  • [10] Hintikka, J.: Knowledge and Belief: An Introduction to the Logic of the Two Notions. Ithaca, NY, USA: Cornell University Press (1962)
  • [11] Lutz, C.: Complexity and succinctness of public announcement logic. In: Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems. pp. 137–143. Hakodate, Japan (2006)
  • [12] Ma, M., Palmigiano, A., Sadrzadeh, M.: Algebraic semantics and model completeness for intuitionistic public announcement logic. Annals of Pure and Applied Logic 165(4), 963–995 (2014)
  • [13] Maffezioli, P., Negri, S.: A Gentzen-style analysis of public announcement logic. In: Azzarola, X., Ponte, M. (eds.) Proceedings of the International Workshop on Logic and Philosophy of Knowledge, Communication and Action. pp. 293–313. University of the Basque Country Press (2010)
  • [14] Negri, S.: Proof analysis in modal logic. Journal of Philosophical Logic 34(5), 507–544 (2005)
  • [15] Nomura, S., Ono, H., Sano, K.: A cut-free labelled sequent calculus for dynamic epistemic logic. Journal of Logic and Computation 30(1), 321–348 (2020)
  • [16] Nomura, S., Sano, K., Tojo, S.: Revising a labelled sequent calculus for public announcement logic. In: Structural Analysis of Non-Classical Logics, pp. 131–157. Springer (2016)
  • [17] Plaza, J.: Logics of public announcements. In: Proceedings 4th International Symposium on Methodologies for Intelligent Systems: Poster Session Program. pp. 201–216 (1989)
  • [18] Rivieccio, U.: Bilattice public announcement logic. In: Goré, R., Kooi, B.P., Kurucz, A. (eds.) Advances in Modal Logic. pp. 459–477. College Publications (2014)