Coalition and Relativised Group Announcement Logic

There are several ways to quantify over public announcements. The most notable are reflected in arbitrary, group, and coalition announcement logics (APAL, GAL, and CAL correspondingly), with the latter being the least studied so far. In the present work, we consider coalition announcements through the lens of group announcements, and provide a complete axiomatisation of a logic with coalition announcements. To achieve this, we employ a generalisation of group announcements. Moreover, we study some logical properties of both coalition and group announcements that have not been studied before.

1. A counterexample was given by Louwe Kuijer and can be found at https://personal.us.es/hvd/APAL_counterexample.pdf.

2. As any formula of \({\mathcal {L}}_{PAL}\) can be translated into an equivalent formula of \({\mathcal {L}}_{EL}\) (Plaza 2007), for succinctness’ sake, we use the former rather than the latter in the scope of knowledge modalities in group announcements.

3. The original idea of an infinite-grid counterexample is by Tim French (personal communication). Here we present its finite and reworked version.

4. Note that in Ågotnes et al. (2010) (as well as in van Ditmarsch 2012) it was claimed that the generalised Church–Rosser principle holds for GAL.

5. French et al. (2019) use the same operators under the name of ‘half-coalition’ announcements. In this paper we use different syntax, which we think is more succinct.

I am very grateful to Natasha Alechina for her help with the previous, conference, version of this paper, and her comments on the current, journal, one. I would also like to thank Thomas Ågotnes, Hans van Ditmarsch, and Tim French for discussions of different parts of this paper on various occasions. Finally, I thank two anonymous reviewers of this journal. Their comments and corrections helped to make this paper both more readable and technically sound.

Authors and Affiliations

1. University of Bergen, Bergen, Norway

   Rustam Galimullin

Corresponding author

Correspondence to Rustam Galimullin.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This paper is partially based on Galimullin and Alechina (2017) (and its corrected version available at Arxiv:1810.02769. Section 3, apart from Propositions 4 and 11, is entirely new. The axiomatisation and the completeness proof in Section 4 are also new, and many overlapping results (e.g. the Lindenbaum Lemma) are significantly improved.

Appendix A: Coalition Annoucement Logic Subsumes Coalition Logic

It is known (Ågotnes and van Ditmarsch 2008) that CAL subsumes CL, i.e. all axioms of CL are valid in CAL, and rules of inference of CL are validity preserving in CAL. However, to the best of our knowledge, a formal proof has not yet been presented.

Proposition 18

All of the following are valid and validity preserving in CAL.

\(\begin{array}{ll} (C0) &{}\text {all instantiations of propositional tautologies},\\ (C1) &{}\lnot \langle \! [ G ] \! \rangle \bot , \\ (C2) &{}\langle \! [ G ] \! \rangle \top , \\ (C3) &{}\lnot \langle \! [ \emptyset ] \! \rangle \lnot \varphi \rightarrow \langle \! [ A ] \! \rangle \varphi ,\\ (C4) &{}\langle \! [ G ] \! \rangle (\varphi _1 \wedge \varphi _2) \rightarrow \langle \! [ G ] \! \rangle \varphi _1, \\ (C5) &{}\langle \! [ G ] \! \rangle \varphi _1 \wedge \langle \! [ H ] \! \rangle \varphi _2 \rightarrow \langle \! [ G \cup H ] \! \rangle (\varphi _1 \wedge \varphi _2),\text { if } G \cap H = \emptyset , \\ (R0) &{}\vdash \varphi , \varphi \rightarrow \psi \Rightarrow \, \vdash \psi ,\\ (R1) &{} \vdash \varphi \leftrightarrow \psi \Rightarrow \, \vdash \langle \! [ G ] \! \rangle \varphi \leftrightarrow \langle \! [ G ] \! \rangle \psi . \end{array}\)

Proof

C0 and R0 are obvious.

C1: It holds that \(\models \top \), and \(\top \) is true in every restriction of a model, i.e. \(\models [ \psi ] \top \). In particular, for some model \(M_s\) and all true formulas \(\psi _G\) and \(\chi _{A {\setminus } G}\): \(M_s \models \langle \psi _G \wedge \chi _{A {\setminus } G} \rangle \top \). We can relax the requirement of \(\psi _G\) being true by adding the formula as an antecedent. Formally, for all (true and false) \(\psi _G\) and some (true) \(\chi _{A {\setminus } G}\): \(M_s \models \psi _G \rightarrow \langle \psi _G \wedge \chi _{A {\setminus } G} \rangle \top \). The latter is \(M_s \models [ \! \langle G \rangle \! ] \top \) by the semantics, and this is equivalent to \(M_s \models \lnot \langle \! [ G ] \! \rangle \bot \) by the duality of the coalition announcement operators.

C2: For any pointed model \(M_s\) and any announcement \(\psi _G \wedge \chi _{A {\setminus } G}\) it holds that \(M_s \models [\psi _G \wedge \chi _{A {\setminus } G}] \top \). The latter implies that for some true \(\psi _G\) and for all \(\chi _{A {\setminus } G}\): \(M_s \models \psi _G \wedge [\psi _G \wedge \chi _{A {\setminus } G}] \top \), which is \(M_s \models \langle \! [ G ] \! \rangle \top \) by the semantics.

C3: Let \(\lnot \langle \! [ \emptyset ] \! \rangle \lnot \varphi \) be true in some arbitrary pointed model \(M_s\). This is equivalent to \(\exists \psi _A\): \(M_s \models \lnot [ \psi _A ] \lnot \varphi \), which is \(M_s \models \langle \! [ A ] \! \rangle \varphi \) by the semantics.

C4: Suppose that for some \(M_s\), \(M_s \models \langle \! [ G ] \! \rangle (\varphi _1 \wedge \varphi _2)\) holds. By the semantics, \(\exists \psi _G, \forall \chi _{A {\setminus } G}\): \(M_s \models \psi _G \wedge [\psi _G \wedge \chi _{A {\setminus } G}] (\varphi _1 \wedge \varphi _2)\). Then, by the axiom of PAL \([\psi ](\varphi \wedge \chi ) \leftrightarrow [\psi ] \varphi \wedge [\psi ] \chi \), we have \(\exists \psi _G, \forall \chi _{A {\setminus } G}\): \(M_s \models \psi _G \wedge [\psi _G \wedge \chi _{A {\setminus } G}] \varphi _1 \wedge [\psi _G \wedge \chi _{A {\setminus } G}] \varphi _2\). The latter implies \(\exists \psi _G, \forall \chi _{A {\setminus } G}\): \(M_s \models \psi _G \wedge [\psi _G \wedge \chi _{A {\setminus } G}] \varphi _1\), which is \(M_s \models \langle \! [ G ] \! \rangle \varphi _1\) by the semantics.

C5: Assume that for some \(M_s\) we have that \(M_s \models \langle \! [ G ] \! \rangle \varphi _1 \wedge \langle \! [ H ] \! \rangle \varphi _2\). Let us consider the first conjunct \(M_s \models \langle \! [ G ] \! \rangle \varphi _1\). By the semantics it is equivalent to \(\exists \psi _G, \forall \chi _{A {\setminus } G}\): \(M_s \models \psi _G \wedge [ \psi _G \wedge \chi _{A {\setminus } G} ] \varphi _1\). Since \(G \cap H = \emptyset \), we can split \(\chi _{A {\setminus } G}\) into \(\chi _{H}\) and \(\chi _{A {\setminus } {G \cup H}}\). Thus we have that \(\exists \psi _G, \forall \chi _H, \forall \chi _{A {\setminus } {(G \cup H)}}\): \(M_s \models \psi _G \wedge [ \psi _G \wedge \chi _{H} \wedge \chi _{A {\setminus } (G \cup H)} ] \varphi _1\). The same holds for the second conjunct: \(\exists \psi _H, \forall \chi _G, \forall \chi _{A {\setminus } {(G \cup H)}}\): \(M_s \models \psi _H \wedge [ \psi _H \wedge \chi _{G} \wedge \chi _{A {\setminus } (G \cup H)} ] \varphi _2\). Since \(\chi _H\) (\(\chi _G\)) quantifies over all formulas known to H (G), we can substitute \(\chi _H\) (\(\chi _G\)) with \(\psi _H\) (\(\psi _G\)). Hence we have

By the axiom of PAL \([\psi ](\varphi \wedge \chi ) \leftrightarrow [\psi ] \varphi \wedge [\psi ] \chi \), we have that

and the latter is equivalent to \(M_s \models \langle \! [ G \cup H ] \! \rangle (\varphi _1 \wedge \varphi _2)\) by the semantics.

\(R1\): Assume that \(\models \varphi \leftrightarrow \psi \). This means that for any pointed model \(M_s\) the following holds: \(M_s \models \varphi \) if and only if \(M_s \models \psi \) (1). Now suppose that for some pointed model \(N_t\) it holds that \(N_t \models \langle \! [ G ] \! \rangle \varphi \). By the semantics, \(\exists \psi _G, \forall \chi _{A {\setminus } G}\): \(N_t \models \psi _G \wedge [\psi _G \wedge \chi _{A {\setminus } G}] \varphi \), which is equivalent to the following: \(N_t \models \psi _G\) and (\(N_t \models \psi _G \wedge \chi _{A {\setminus } G}\) implies \(N^{\psi _G \wedge \chi _{A {\setminus } G}}_t \models \varphi \)). By (1) we have that \(\exists \psi _G, \forall \chi _{A {\setminus } G}\): \(N_t \models \psi _G\) and (\(N_t \models \psi _G \wedge \chi _{A {\setminus } G}\) implies \(N^{\psi _G \wedge \chi _{A {\setminus } G}}_t \models \psi \)), which is \(N_t \models \langle \! [ G ] \! \rangle \psi \) by the semantics. Since \(N_t\) was arbitrary, we have that \(\models \langle \! [ G ] \! \rangle \varphi \rightarrow \langle \! [ G ] \! \rangle \psi \). The same argument holds in the other direction. \(\square \)

Appendix B: Proofs from Sect. 4

Proposition 14 R3 and R4 are truth-preserving.

Proof

(R3) Base case. If for all \(\psi _G\) we have that \(M_s \models \chi \wedge [\psi _G \wedge \chi ] \varphi \), then this is equivalent to \(M_s \models [G, \chi ] \varphi \) by the semantics.

Induction Hypothesis. If for some \(M_s\) it holds that \(M_s \models \eta (\chi \wedge [\psi _G \wedge \chi ] \varphi )\) for all \(\psi _G\), then \(M_s \models \eta ([G, \chi ] \varphi )\).

Case \(\forall \psi _G\): \(\tau \rightarrow \eta (\chi \wedge [\psi _G \wedge \chi ] \varphi )\) for some \(\tau \in {\mathcal {L}}_{CoRGAL}\). This means that \(M_s \models \lnot \tau \) or \(M_s \models \eta (\chi \wedge [\psi _G \wedge \chi ] \varphi )\). By the induction hypothesis we have that \(M_s \models \lnot \tau \) or \(M_s \models \eta ([ G, \chi ] \varphi )\), which is equivalent to \(M_s \models \tau \rightarrow \eta ([ G, \chi ] \varphi )\).

Case \(\forall \psi _G\): \(K_a \eta (\chi \wedge [\psi _G \wedge \chi ] \varphi )\) for some \(a \in A\). By semantics we have that for every \(t \in S\): \(s \sim _a t\) implies \(M_t \models \eta (\chi \wedge [\psi _G \wedge \chi ] \varphi )\). By the induction hypothesis we conclude that for every \(t \in S\): \(s \sim _a t\) implies \(M_t \models \eta ([G, \chi ] \varphi )\), which is equivalent to \(M_s \models K_a \eta ([ G, \chi ] \varphi )\).

Case \(\forall \psi _G\): \([\tau ] \eta (\chi \wedge [\psi _G \wedge \chi ] \varphi )\) for some \(\tau \in {\mathcal {L}}_{CoRGAL}\). This means that \(M_s \models \tau \) implies \(M_s^\tau \models \eta (\chi \wedge [\psi _G \wedge \chi ] \varphi )\). By the induction hypothesis we have that \(M_s \models \tau \) implies \(M_s^\tau \models \eta ([ G, \chi ] \varphi )\), which is equivalent to \(M_s \models [\tau ] \eta ([ G, \chi ] \varphi )\).

(R4) Base case. If for all \(\psi _G\) we have that \(M_s \models \langle A {\setminus } G, \psi _G \rangle \varphi \), then this is equivalent to \(M_s \models [ \! \langle G \rangle \! ] \varphi \) by the semantics.

Induction Hypothesis. If for some \(M_s\) it holds that \(M_s \models \eta (\langle A {\setminus } G, \psi _G \rangle \varphi )\) for all \(\psi _G\), then \(M_s \models \eta ([ \! \langle G \rangle \! ] \varphi )\).

Case \(\forall \psi _G\): \(\tau \rightarrow \eta (\langle A {\setminus } G, \psi _G \rangle \varphi )\) for some \(\tau \in {\mathcal {L}}_{CoRGAL}\). This means that \(M_s \models \lnot \tau \) or \(M_s \models \eta (\langle A {\setminus } G, \psi _G \rangle \varphi )\). By the induction hypothesis we have that \(M_s \models \lnot \tau \) or \(M_s \models \eta ([ \! \langle G \rangle \! ] \varphi )\), which is equivalent to \(M_s \models \tau \rightarrow \eta ([ \! \langle G \rangle \! ] \varphi )\).

Case \(\forall \psi _G\): \(K_a \eta (\langle A {\setminus } G, \psi _G \rangle \varphi )\) for some \(a \in A\). By semantics we have that for every \(t \in S\): \(s \sim _a t\) implies \(M_t \models \eta (\langle A {\setminus } G, \psi _G \rangle \varphi )\). By the induction hypothesis we conclude that for every \(t \in S\): \(s \sim _a t\) implies \(M_t \models \eta ([ \! \langle G \rangle \! ] \varphi )\), which is equivalent to \(M_s \models K_a \eta ([ \! \langle G \rangle \! ] \varphi )\).

Case \(\forall \psi _G\): \([\tau ] \eta (\langle A {\setminus } G, \psi _G \rangle \varphi )\) for some \(\tau \in {\mathcal {L}}_{CoRGAL}\). This means that \(M_s \models \tau \) implies \(M_s^\tau \models \eta (\langle A {\setminus } G, \psi _G \rangle \varphi )\). By the induction hypothesis we have that \(M_s \models \tau \) implies \(M_s^\tau \models \eta ([ \! \langle G \rangle \! ] \varphi )\), which is equivalent to \(M_s \models [\tau ] \eta ([ \! \langle G \rangle \! ] \varphi )\). \(\square \)

Lemma 4 Let \(\varphi , \psi , \chi \in {\mathcal {L}}_{CoRGAL}\). The following inequalities hold.

Proof

The proof is straightforward. We just show cases 5 and 6.

5. Note that \([\! \langle \! \rangle \! ]\)-depth for both sides of the inequality is the same and equals \(d_{[ \! \langle \! \rangle \! ]}(\chi ) + d_{[ \! \langle \! \rangle \! ]} (\varphi )\). In particular, we have the following for the left-hand side: \(d_{[ \! \langle \! \rangle \! ]} (\chi \wedge [\psi _G \wedge \chi ] \varphi )\) \(=\) \(\text {max}\{d_{[ \! \langle \! \rangle \! ]} (\chi ), d_{[ \! \langle \! \rangle \! ]} ([\psi _G \wedge \chi ] \varphi )\} = d_{[ \! \langle \! \rangle \! ]} ([\psi _G \wedge \chi ] \varphi ) = d_{[ \! \langle \! \rangle \! ]} (\psi _G \wedge \chi ) + d_{[ \! \langle \! \rangle \! ]} (\varphi ) = \text {max}\{d_{[ \! \langle \! \rangle \! ]} (\psi _G), d_{[ \! \langle \! \rangle \! ]}(\chi )\}\) \(+\) \(d_{[ \! \langle \! \rangle \! ]} (\varphi ) = d_{[ \! \langle \! \rangle \! ]} (\chi ) + d_{[ \! \langle \! \rangle \! ]} (\varphi )\). For the right-hand side we have that \(d_{[ \! \langle \! \rangle \! ]} ([G, \chi ] \varphi ) = d_{[ \! \langle \! \rangle \! ]}(\chi ) + d_{[ \! \langle \! \rangle \! ]} (\varphi )\).

Since \([ \! \langle \! \rangle \! ]\)-depths are the same, we calculate [, ]-depths. For the left-hand side we have that \(d_{[,]} (\chi \wedge [\psi _G \wedge \chi ]\varphi ) = d_{[,]} (\chi ) + d_{[,]} (\varphi )\). In particular, \(d_{[,]} (\chi \wedge [\psi _G \wedge \chi ]\varphi ) =\) \(\text {max} \{d_{[,]} (\chi ),\) \(d_{[,]} ([\psi _G \wedge \chi ]\varphi )\} =\) \(d_{[,]} ([\psi _G \wedge \chi ]\varphi )=\) \(d_{[,]} (\psi _G \wedge \chi ) + d_{[,]} (\varphi ) = \) \(\text {max}\{d_{[,]}(\psi _G), d_{[,]} (\chi )\} + d_{[,]} (\varphi )= \) \(d_{[,]} (\chi ) + d_{[,]} (\varphi )\). Depth of the right-hand side formula is \(d_{[,]} ([G, \chi ]\varphi ) = \) \(1 + d_{[,]} (\varphi ) + d_{[,]} (\chi )\). Hence, \(\chi \wedge [\psi _G \wedge \chi ]\varphi <^{Size}_{[,], [ \! \langle \! \rangle \! ]} [G, \chi ]\varphi \).

6. On the left-hand side we have that \(d_{[ \! \langle \! \rangle \! ]} (\langle A {\setminus } G, \psi _G \rangle \varphi ) =\) \(d_{[ \! \langle \! \rangle \! ]} (\varphi )\), and on the right-hand side the depth is \(d_{[ \! \langle \! \rangle \! ]} [ \! \langle G \rangle \! ] \varphi = \) \(d_{[ \! \langle \! \rangle \! ]} (\varphi ) + 1\). Hence, \(\langle A {\setminus } G, \psi _G \rangle \varphi <^{Size}_{[,], [ \! \langle \! \rangle \! ]} [ \! \langle G \rangle \! ] \varphi \). \(\square \)

Lemma 6 Let \(\varphi , \psi \in {\mathcal {L}}_{CoRGAL}\). If \(\varphi \rightarrow \psi \) is a theorem, then \(\eta (\varphi ) \rightarrow \eta (\psi )\) is a theorem as well.

Proof

Assume that \(\varphi \rightarrow \psi \) is a theorem. We prove the lemma by induction on \(\eta \).

Base case \(\eta {{:}{=}} \sharp \). Formula \(\varphi \rightarrow \psi \) is a theorem by assumption.

Induction Hypothesis. Assume that for some \(\eta \), \(\eta (\varphi ) \rightarrow \eta (\psi )\) is a theorem.

Case \((\tau \rightarrow \eta (\varphi )) \rightarrow (\tau \rightarrow \eta (\psi ))\) for some \(\tau \in {\mathcal {L}}_{CoRGAL}\). Formula \((\eta (\varphi ) \rightarrow \eta (\psi )) \rightarrow ((\tau \rightarrow \eta (\varphi )) \rightarrow (\tau \rightarrow \eta (\psi )))\) is a propositional tautology, and, hence, a theorem of CoRGAL. Using the induction hypothesis and R0, we have that \((\tau \rightarrow \eta (\varphi )) \rightarrow (\tau \rightarrow \eta (\psi ))\) is a theorem.

Case \(K_a \eta (\varphi ) \rightarrow K_a \eta (\psi )\) for some \(a \in A\). Since \(\eta (\varphi ) \rightarrow \eta (\psi )\) is a theorem by the induction hypothesis, \(K_a (\eta (\varphi ) \rightarrow \eta (\psi ))\) is also a theorem by R1. Next, \(K_a (\eta (\varphi ) \rightarrow \eta (\psi )) \rightarrow (K_a \eta (\varphi ) \rightarrow K_a \eta (\psi ))\) is an instance of A1, and, hence, a theorem. Finally, using R0 we have that \(K_a \eta (\varphi ) \rightarrow K_a \eta (\psi )\) is a theorem.

Case \([\tau ] \eta (\varphi ) \rightarrow [\tau ] \eta (\psi )\) for some \(\tau \in {\mathcal {L}}_{CoRGAL}\). Since \(\eta (\varphi ) \rightarrow \eta (\psi )\) is a theorem by the induction hypothesis, \([\tau ] (\eta (\varphi ) \rightarrow \eta (\psi ))\) is also a theorem by R2. Formula \([\tau ](\eta (\varphi ) \rightarrow \eta (\psi )) \rightarrow ([\tau ]\eta (\varphi ) \rightarrow [\tau ]\eta (\psi ))\) is implied by axiom schema A5. Using R0 we can conclude that \([\tau ]\eta (\varphi ) \rightarrow [\tau ]\eta (\psi )\) is a theorem of CoRGAL. \(\square \)

Lemma 7 Let \(x\) be a theory, \(\varphi , \psi \in {\mathcal {L}}_{CoRGAL}\), and \(a \in A\). The following are theories: \(x + \varphi = \{\psi \mid \varphi \rightarrow \psi \in x\}, K_a x = \{\varphi \mid K_a \varphi \in x\}\), and \([\varphi ]x = \{\psi \mid [\varphi ]\psi \in x\}\).

Proof

Let \(\psi \) be a theorem, i.e. \(\psi \in \mathrm {CoRGAL}\). Then \(\varphi \rightarrow \psi \) is also a theorem, since \(\psi \rightarrow (\varphi \rightarrow \psi ) \in \mathrm {CoRGAL}\) and CoRGAL is closed under R0. Moreover, \(K_a \psi \) and \([\varphi ] \psi \) are theorems as well due to the fact that CoRGAL is closed under R1 and R2. Therefore, \(\psi \in x + \varphi \), \(\psi \in K_a x\), and \(\psi \in [\varphi ] x\), and hence \(\mathrm {CoRGAL} \subseteq x + \varphi , K_a x, [\varphi ] x\).

The rest of the proof is an extension of the one from Balbiani et al. (2008), where it was shown that \(x + \varphi \), \(K_a x\), and \([\varphi ] x\) are closed under R0. We argue that corresponding sets are closed under R3 and R4.

Case \(x + \varphi \). Suppose that \(\eta (\chi \wedge [\psi _G \wedge \chi ]\tau ) \in x + \varphi \) for some given \(\chi \), for all \(\psi _G\), and for some \(\tau \in {\mathcal {L}}_{CoRGAL}\). This means that \(\varphi \rightarrow \eta (\chi \wedge [\psi _G \wedge \chi ]\tau ) \in x\) for all \(\psi _G\). Since \(\varphi \rightarrow \eta (\chi \wedge [\psi _G \wedge \chi ]\tau )\) is a necessity form, and \(x\) is closed under \(R3\) (by Definition 16), we infer that \(\varphi \rightarrow \eta ([G, \chi ] \tau ) \in x\), and, consequently, \(\eta ([G, \chi ] \tau ) \in x + \varphi \). So, \(x + \varphi \) is closed under \(R3\).

Now, let \(\forall \psi _G\): \(\eta (\langle A {\setminus } G, \psi _G \rangle \tau ) \in x + \varphi \). By the definition of \(x+\varphi \) this means that \(\varphi \rightarrow \eta (\langle A {\setminus } G, \psi _G \rangle \tau ) \in x\) for all \(\psi _G\). Since \(\varphi \rightarrow \eta (\langle A {\setminus } G, \psi _G \rangle \tau \) is a necessity form and x is closed under R4, we infer that \(\varphi \rightarrow \eta ( [ \! \langle G \rangle \! ] \tau ) \in x\), and, consequently, \(\eta ( [ \! \langle G \rangle \! ] \tau ) \in x + \varphi \). So, \(x + \varphi \) is closed under \(R4\).

Case \(K_a x\). Suppose that \(\eta (\chi \wedge [\psi _G \wedge \chi ]\tau ) \in K_a x\) for some given \(\chi \), for all \(\psi _G\), and for some \(\tau \in {\mathcal {L}}_{CoRGAL}\). This means that \(K_a \eta (\chi \wedge [\psi _G \wedge \chi ]\tau ) \in x\) for all \(\psi _G\). Since \(K_a \eta (\chi \wedge [\psi _G \wedge \chi ]\tau )\) is a necessity form, and \(x\) is closed under \(R3\) (by Definition 16), we infer that \(K_a \eta ([G, \chi ] \tau ) \in x\), and, consequently, \(\eta ([G, \chi ] \tau ) \in K_a x\). So, \(K_a x\) is closed under \(R3\).

Now, let \(\forall \psi _G\): \(\eta (\langle A {\setminus } G, \psi _G \rangle \tau ) \in K_a x\). By the definition of \(K_a x\) this means that \(K_a \eta (\langle A {\setminus } G, \psi _G \rangle \tau ) \in x\) for all \(\psi _G\). Since \(K_a \eta (\langle A {\setminus } G, \psi _G \rangle \tau \) is a necessity form and x is closed under R4, we infer that \(K_a \eta ( [ \! \langle G \rangle \! ] \tau ) \in x\), and, consequently, \(\eta ( [ \! \langle G \rangle \! ] \tau ) \in K_a x\). So, \(K_a x\) is closed under \(R4\).

Case \([\varphi ] x\). Finally, suppose that \(\eta (\chi \wedge [\psi _G \wedge \chi ]\tau ) \in [\varphi ] x\) for some given \(\chi \), for all \(\psi _G\), and for some \(\tau \in {\mathcal {L}}_{CoRGAL}\). This means that \([\varphi ] \eta (\chi \wedge [\psi _G \wedge \chi ]\tau ) \in x\) for all \(\psi _G\). Since \([\varphi ] \eta (\chi \wedge [\psi _G \wedge \chi ]\tau )\) is a necessity form, and \(x\) is closed under \(R3\) (by Definition 16), we infer that \([\varphi ] \eta ([G, \chi ] \tau ) \in x\), and, consequently, \(\eta ([G, \chi ] \tau ) \in [\varphi ] x\). So, \([\varphi ] x\) is closed under \(R3\).

Now, let \(\forall \psi _G\): \(\eta (\langle A {\setminus } G, \psi _G \rangle \tau ) \in [\varphi ] x\). By the definition of \([\varphi ] x\) this means that \([\varphi ] \eta (\langle A {\setminus } G, \psi _G \rangle \tau ) \in x\) for all \(\psi _G\). Since \([\varphi ] \eta (\langle A {\setminus } G, \psi _G \rangle \tau \) is a necessity form and x is closed under R4, we infer that \([\varphi ] \eta ( [ \! \langle G \rangle \! ] \tau ) \in x\), and, consequently, \(\eta ( [ \! \langle G \rangle \! ] \tau ) \in [\varphi ] x\). So, \([\varphi ] x\) is closed under \(R4\). \(\square \)

Reprints and permissions