Pairing Traditional and Generic Common Knowledge

Abstract

Common Knowledge C is a standard tool in epistemic logics. Generic Common Knowledge J is an alternative which has desirable logical behavior such as cut-elmination and which can be used in place of C in the analysis of many games and epistemic senarios. In order to compare their deductive strengths directly we define the multi-agent logic $\mathsf{S4}_n^{CJ}$ built on a language with both C and J operators in addition to agents’ $K_i$s so that any finite prefix of modal operators is acceptable. We prove $\mathsf{S4}_n^{CJ}$ is complete, decidable, and that $J\varphi \rightarrow C\varphi$ though not $C\varphi \rightarrow J\varphi$. Additional epistemic scenarios may be investigated which take advantage of this dual layer of common knowledge agents.

1 Introduction

In systems of multiple knowers, or agents, it is natural to consider what information is publicly known. The most investigated such concept is that of common knowledge. Informally, if a sentence or proposition $\varphi$ is common knowledge, $C\varphi$, then everyone knows it ($E\varphi$), and everyone knows everyone knows it ($EE\varphi$), and everyone knows everyone knows everyone knows it, etc., i.e., iterated knowledge of $\varphi$, $I\varphi$. Common knowledge has overwhelmingly been formalized as an equivalence of $C\varphi$ and $I\varphi$ via a finite set of axioms. In each multi-agent system, C is unique.

However, there is a more general and eventually simpler conception of common knowledge, generic common knowledge, J. While $J\varphi$ is sufficient to yield iterated knowledge, it is not necessarily equivalent to $I\varphi$. This alternative offers a broader view of common knowledge as it allows for a choice between multiple logically non-equivalent common knowledge operators. Moreover, generic common knowledge which is not the traditional common knowledge naturally appears in some canonical epistemic scenarios. For example, a public announcement of an atomic fact A creates not common knowledge but rather universal knowledge (an instance of generic common knowledge) of A since A, a posteriori, holds at all worlds, not only at all reachable worlds. In the belief revision situations, such as the well-known Stalnaker-Halpern game, the revision function overspills to another reachability cluster of worlds and hence no longer should obey the common knowledge assumption [4].

The generic common knowledge was introduced by McCarthy in [11] as ‘any fool knows’ and independently by Artemov in [6] as ‘justified common knowledge’ who later termed it ‘generic common knowledge.’ In [6] it was the implicit ‘forgetful projection’ counterpart to the explicit constructive knowledge LP component of $\mathsf{S4}_n$ LP, a logic in the family of justification logics. J differs from C in logical behavior: its addition to a system does not hinder straightforward completeness proofs and as the cut-rule can be eliminated the way is paved for its Realization to an explicit justification logic counterpart e.g. the realization of $\mathsf{S4}_n^J$ in $\mathsf{S4}_n\mathsf{LP}$ [5, 6] or in ${\mathsf{LP}}_n$(LP) [2]. These realizations impart a rich semantics: $J\varphi$ asserts that $\varphi$ is common knowledge arising from a proof of $\varphi$. In applications, J can be used in place of C whenever common knowledge is assumed as a premise, rather than being the desired outcome [3]. The cut-rule for traditional common knowledge has been investigated in [1] and syntactic elimination obtained for some systems as in [9].

This paper defines a multi-agent epistemic logic $\mathsf{S4}_n^{CJ}$ which expands on the n-agent logic $\mathsf{S4}_n$ to encompass two formulations common knowledge C and J. Completeness for this logic is shown, providing a basis for direct comparison of the deductive strength of J and C. We shall see that $J\varphi \rightarrow C\varphi$ though not the converse.

2 Axiomatization of $\mathsf{S4}_n^{CJ}$

In $\mathsf{S4}_n^{CJ}$ we can consider formulas which may contain both C and J as well as $K_i$ modalities.

Definition 1

The language $\mathcal {L}_{\mathsf{S4}_n^{CJ}}$ is an extension of the propositional language:

$$\begin{aligned} \mathcal {L}_{\mathsf{S4}_n^{CJ}} :=\{ Var , \wedge , \vee , \rightarrow , \lnot , K_i, C, J \} \end{aligned}$$

for $i\in \{1,2,\dots ,n\}$ where Var is the set of propositional variables. Formulas are defined by the grammar

$$\begin{aligned} \varphi := p \ | \ \varphi \wedge \varphi \ | \ \varphi \vee \varphi \ | \ \varphi \rightarrow \varphi \ | \ \lnot \varphi \ | \ K_i\varphi \ | \ C\varphi \ | \ J\varphi \ \end{aligned}$$

where $p\in$ Var.

The formula $K_1K_2\varphi$ has the intended semantics of ‘agent 1 knows that agent 2 knows $\varphi$’ while $C\varphi$ and $J\varphi$ have the intended semantics of ‘$\varphi$ is common knowledge’ and ‘$\varphi$ is generic common knowledge’ respectively.

Definition 2

The axioms and rules of $\mathsf{S4}_n^{CJ}$, for $i\in \{1,2,\dots ,n\}$ where $\Box$ is $K_i$ or J or C:

Proposition 1

Both $C\varphi$ and $J\varphi$ satisfy X in the Fixed Point Axiom,

$$\begin{aligned} X\leftrightarrow E(\varphi \wedge X). \end{aligned}$$

Proof

$J\varphi \leftrightarrow E(\varphi \wedge J\varphi )$:

Normal modals are those with K axiom and subject to necessitation (R2). Each J axiom or rule has a C counterpart. Thus, as J satisfies the fixed point axiom, so does C.

Proposition 2

$\mathsf{S4}_n^{CJ}\vdash J\varphi \rightarrow C\varphi$.

Proof

Reasons from propositional calculus are not listed.

That the converse does not hold must wait till Proposition 4, after $\mathsf{S4}_n^{CJ}$ is shown to be sound and complete.

We will use the following proposition in the completeness proof (Theorem 2).

Proposition 3

$\mathsf{S4}_n^{CJ}\vdash C\varphi \rightarrow EC\varphi$.

Proof

Just as lines 1. – 3. in the forward direction of proof of Proposition 1.

Definition 3

An $\mathsf{S4}_n^{CJ}$-model is $M^{CJ}=\langle W, R_1,\dots ,R_n, R_C,R_J,\Vdash \rangle$ such that

• $W\ne \emptyset$ is a set of worlds;

• $R_i\subseteq W\times W$ is reflexive and transitive for $i\in \{1,\dots ,n\}$;

• $R_C=\big (\bigcup \limits _{i=1}^n R_i \big )^{TC}$, the transitive closure of the union of $R_i$s;

• $R_J\subseteq W\times W$ is reflexive and transitive and $R_C\subseteq R_J$;

• $\Vdash \ \subseteq W \times Var$ so that for $w\in W, p\in Var,\ \ w\Vdash p$ iff p holds at w;

• $\Vdash$ is extended to correspond with Boolean connectives at each world and so the asccessibility relations $R_i, R_C$, and $R_J$ corresponds to the modalities $K_i, C$, and J respectively, so that in $M^{CJ}$

  $$\begin{aligned} u\Vdash K_i\varphi \mathrm { \ iff \ }(\forall v\in W) (uR_iv\Rightarrow v\Vdash \varphi ), \end{aligned}$$
  $$\begin{aligned} u\Vdash C\varphi \mathrm { \ iff \ }(\forall v\in W)(uR_Cv\Rightarrow v\Vdash \varphi ), \end{aligned}$$
  $$\begin{aligned} u\Vdash J\varphi \mathrm { \ iff \ }(\forall v\in W)(uR_Jv\Rightarrow v\Vdash \varphi ). \end{aligned}$$

Note that the accessibility relation of C corresponds to reachability in each connected component of the model and is exactly prescribed by the agents’ relations. On the other hand there is flexibility for $R_J$ to be any reflexive transitive relation as small as $R_C$ or a large as the total relation.

Theorem 1

$\mathsf{S4}_n^{CJ}$ is sound with respect to $M^{CJ}$ models.

Proof

(Soundness). Let M be an arbitrary $\mathsf{S4}_n^{CJ}$-model. Assume $\chi$ is provable and show it holds in each world of M. It is enough to show that all the axioms and rules are valid.

• $\chi$ is a propositional variable: $u\Vdash \chi$ for all worlds in the model M implies $\chi$ is valid by definition.

• $\chi =\lnot \varphi \ | \ \varphi \wedge \psi \ | \ \varphi \vee \psi \ | \ \varphi \rightarrow \psi$. If $\chi$ is formed by Boolean connectives, it is valid by the definition of these connectives at each world.

• modus ponens: Suppose $u\Vdash \varphi \rightarrow \psi$. Then by the definition of the connectives, either $u\not \Vdash \varphi$ or $u\Vdash \psi$. If also $u\Vdash \varphi$, then $u\Vdash \psi$. So if $\varphi \rightarrow \psi$ and $\varphi$ hold at any world, so does $\psi$.

• K axioms: Shown for $K_i$ but analogous for C and J. $\chi =K_i(\varphi \rightarrow \psi )\rightarrow (K_i\varphi \rightarrow K_i\psi )= (K_i(\varphi \rightarrow \psi ) \wedge K_i\varphi )\rightarrow K_i\psi$. Suppose $u\Vdash K_i(\varphi \rightarrow \psi )\wedge K_i\varphi$, then for all v such that $uR_iv$, $v\Vdash \varphi \rightarrow \psi$ and $v\Vdash \varphi$. So as modus ponens is valid $v\Vdash \psi$, and hence $u\Vdash K_i\psi$. Therefore $u\Vdash K_i(\varphi \rightarrow \psi )\rightarrow (K_i\varphi \rightarrow K_i\psi )$ is valid.

• T axioms: Shown for $K_i$ but analogous for C and J. $\chi =K_i\varphi \rightarrow \varphi$. Suppose $u\Vdash K_i\varphi$, then for all v such that $uR_iv$, $v\Vdash \varphi$. Since $R_i$ is reflexive, $uR_iu$, and so $u\Vdash \varphi$. Thus $u\Vdash K_i\varphi \rightarrow \varphi$ is valid. $R_C$ is reflexive as it is the transitive closure of a union of reflexive relations.

• 4 axioms: Shown for $K_i$ but analogous for C and J. Suppose $u\Vdash K_i\varphi$, then for all v such that $uR_iv$, $v\Vdash \varphi$. As $R_i$ is transitive, for all w such that $vR_iw$, $uR_iw$ and so $w\Vdash \varphi$ and so $v\Vdash K_i\varphi$ and hence $u\Vdash K_iK_i\varphi$. Therefore $u\Vdash K_i\varphi \rightarrow K_iK_i\varphi$ is valid.

• modal necessitation: Shown for $K_i$ but analogous for C and J. Assume $\varphi$ is valid in M, then it is true at each world so $u\Vdash \varphi$, and for all worlds v such that $vR_iu$, $v\Vdash \varphi$. Thus $u\Vdash K_i\varphi$. As the world u was arbitrary, $K_i\varphi$ holds at all worlds and so is valid in the model. Therefore $\vdash \varphi \Rightarrow \ \vdash K_i\varphi$ is valid.

• Con axiom: $\chi = J\varphi \rightarrow K_i\varphi$. Suppose $u\Vdash J\varphi$ so that for all v such that $uR_Jv$, $v\Vdash \varphi$. For all i, $R_i\subseteq R_J$ by definition, so for all w such that $uR_iw$, also $uR_Jw$ and so $w\Vdash \varphi$, thus $u\Vdash K_i\varphi$.

• ConC: Analogous to the proof shown above for J’s connection axiom Con.

• IA: $\chi = \varphi \wedge C(\varphi \rightarrow E\varphi ) \rightarrow C\varphi$. Suppose $u\Vdash \varphi \wedge C(\varphi \rightarrow E\varphi )$. Then for all v such that $uR_Cv$, $v\Vdash \varphi \rightarrow E\varphi$ ($**$). We want to show $u\Vdash C\varphi$, i.e. $v\Vdash \varphi$ for all v reachable from u. Proceed by induction on length of path l along $R_i$s from u to v. It is sufficient to show this for paths of length l along the $R_i$s as then the $R_C$ paths are of length $\le l$ (and in fact of length 0 or 1 along $R_C$).

  – If $l=0$ then $u=v$ and by assumption, $u\Vdash \varphi$.

  – Induction Hypothesis: Assume $s\Vdash \varphi$ holds for worlds s reachable from u by a path of length l.

  – Suppose that v is reachable from u by a path of length $l+1$. Then there is a world t reachable from u in l steps and $tR_iv$ for some i. By the induction hypothesis, $t\Vdash \varphi$ but also by ($**$) and modus ponens, $t\Vdash E\varphi$. But $tR_iv$, so $v\Vdash \varphi$. Thus $u\Vdash C\varphi$.

3 Completeness of $\mathsf{S4}_n^{CJ}$

Theorem 2

$\mathsf{S4}_n^{CJ}$ is complete with respect to $M^{CJ}$ models.

To show completeness, the usual approach would be to construct the canonical model. However, here the canonical structure turns out not to be a model of $\mathsf{S4}_n^{CJ}$. So, instead of a single large model which acts as a counter-model for all non-provable $\varphi$, for each non-provable $\varphi$ we construct a finite model with a world at which $\varphi$ does not hold. Filtration techniques on the canonical structure yield these counter-models. The proof of Theorem 2 is delayed until the end of Sect. 3.2 after the presentation on filtrations.

Definition 4

The canonical structure for $\mathsf{S4}_n^{CJ}$ is $M'= \langle W, R_1,\dots ,R_n, R_C, R_J, \Vdash \rangle$ where

• $W=\{\varGamma \ | \ \varGamma$ is a maximally consistent set of $\mathsf{S4}_n^{CJ}$ formulas$\}$;

• $\Vdash \ \subseteq W\times Var$ such that $\varGamma \Vdash p \mathrm { \ iff \ } p\in \varGamma$ for $p\in$ Var;

• $\varGamma R_i\varDelta \mathrm { \ iff \ } \varGamma ^i\subseteq \varDelta$, where $\varGamma ^i:=\{\varphi \ | \ K_i\varphi \in \varGamma \}$;

• $\varGamma R_C\varDelta \mathrm { \ iff \ } \varGamma ^C\subseteq \varDelta$, where $\varGamma ^C:=\{\varphi \ | \ C\varphi \in \varGamma \}$;

• $\varGamma R_J\varDelta \mathrm { \ iff \ } \varGamma ^J\subseteq \varDelta$, where $\varGamma ^J:=\{\varphi \ | \ J\varphi \in \varGamma \}.$

Lemma 1

(Truth Lemma). $M'$ satisfies the Truth Lemma: for all $\varGamma$

$$\begin{aligned} M', \varGamma \Vdash \varphi \Leftrightarrow \varphi \in \varGamma . \end{aligned}$$

(1)

Proof

The proof by induction on $\varphi$ is standard and mimics the $\mathsf{S4}_n$ case but we reproduce it here.

• base case: $\varphi = p$ for $p\in$ Var. Holds by definition of $\Vdash$.

• Induction Hypothesis: Assume that the Truth Lemma holds for formulas of lower complexity.

• Boolean cases: by extension of $\Vdash$, the induction hypothesis, and maximality of $\varGamma$.

• modal case: Shown for $K_i$ but analogous for C and J. $\varphi = K_i\varphi$ ($\Leftarrow$) Assume $K_i\varphi \in \varGamma$. Then for all $\varDelta$ such that $\varGamma R_i\varDelta$, $\varphi \in \varDelta$ so by the induction hypothesis, $\varDelta \Vdash \varphi$. Thus $\varGamma \Vdash K_i\varphi$. ($\Rightarrow$) Assume $K_i\varphi \notin \varGamma$. Then $\varGamma ^i\cup \{\lnot \varphi \}$ must be consistent by the maximality of $\varGamma$, for otherwise $\varphi$ would be provable and hence (by necessitation) so would $K_i\varphi$, which would contradict the consistency of $\varGamma$. If $\varDelta$ is any maximally consistent set containing $\varGamma ^i\cup \{\lnot \varphi \}$, then $\varGamma R_i\varDelta$ by definition of $R_i$. So $\varGamma \not \Vdash K_i\varphi$.

Corollary 1

As a consequence of the Truth Lemma, any maximal consistent set of formulas is satisfiable in $M'$.

Thus $\mathsf{S4}_n^{CJ}\vdash \varphi \Rightarrow M',\varGamma \Vdash \varphi$, so soundness holds for the canonical structure.

Lemma 2

The canonical structure $M'$ is not a model of $\mathsf{S4}_n^{CJ}$ (cf. [12] p. 50).

In $M'$, all accessibility relations are reflexive and transitive and $R_C\subseteq R_J$. However, $R_C\not = \big (\bigcup \limits _{i=1}^nR_i\big )^{\mathrm {TC}}$ as we only have $\big (\bigcup \limits _{i=1}^nR_i\big )^{\mathrm {TC}}\subset R_C$, thus $M'$ is not a model of $\mathsf{S4}_n^{CJ}$.

Proof

It suffices to show that $R_C\not \subset \big (\bigcup \limits _{i=1}^nR_i\big )^{\mathrm {TC}}$. Consider a set of formulas

$$\begin{aligned} \varPhi = \{Ep, EEp,EEEp,\dots \}\cup \{\lnot Cp\} \end{aligned}$$

(2)

for some $p\in Var$ and abbreviate EEEp as $E^3p$, etc.

Claim

$\varPhi$ is ${ \mathsf S4}_n^{CJ}$-consistent.

Proof

(of Claim). Suppose $\varPhi$ is inconsistent. Then there is a finite $\varDelta \subset \varPhi$ which is already inconsistent so say $\varDelta =\{E^{k_1}p, E^{k_2}p,\dots ,E^{k_m}p\ |\ k_i<k_{i+1}\ for\ i<m\}\cup \{\lnot Cp\}$. (If $\varDelta$ were already inconsistent, including $\{\lnot Cp\}$ would keep $\varDelta$ inconsistent.) Consider the model $N=\langle W, R_1,R_2, R_C, R_J,\Vdash \rangle$t where

• $W=\mathbb {N}$;

• $R_1=\{(n,n) \ | \ n\in \mathbb {N}\}\cup \{(n,n+1), (n+1,n) \ | \ n\in \mathbb {N}$ and n even$\}$;

• $R_2=\{(n,n) \ | \ n\in \mathbb {N}\}\cup \{(n,n+1), (n+1,n) \ | \ n\in \mathbb {N}$ and n odd$\}$;

• $R_J=R_C=(R_1\cup R_2)^{\mathrm {TC}}$;

• $x\Vdash p \mathrm { \ iff \ } x\le k_m+1$.

Fig. 1.

This shows the frame of N with the reflexive arrows of $R_1$ and $R_2$ suppressed.

For this model $R_C$ is an equivalence relation with one class, $mR_Cn$ for all $m,n\in \mathbb {N}$. But $N,1\Vdash \varDelta$. To see why, consider an example where $k_m=3$ thus

Since $1\Vdash E^3p\wedge \lnot Cp$, this $\varDelta$ is satisfied and hence is consistent. Since no finite subset of $\varDelta$ is inconsistent, $\varPhi$ is consistent.$_{{ Claim}}$

We now finish the proof of Lemma 2. Since $\varPhi$ is consistent, it is contained in some maximal consistent set $\varPhi '$. Let $\varTheta =\{\lnot p\}\cup \{\theta \ | \ C\theta \in \varPhi '\}$. Note that $\varTheta$ is consistent. As $\{\theta \ | \ C\theta \in \varPhi '\}\subseteq \varPhi '$ which is maximal consistent, $\varTheta$ could only be inconsistent if $\lnot p\wedge p\in \varTheta$. As $\lnot Cp\in \varPhi$, Cp is not in $\varPhi '$, so p is not in $\varTheta$, so $\varTheta$ is consistent, and so contained in some maximal consistent set $\varTheta '$. Observe that $\varPhi '^C\subseteq \varTheta '$ so that in $M'$, $\varPhi ' R_C\varTheta '$. However $(\varPhi ', \varTheta ')\not \in \big (\bigcup \limits _{i=1}^nR_i\big )^{\mathrm {TC}}$ as for each m, $E^mp\in \varPhi '$, but $\lnot p\in \varTheta '$. Therefore, $M'$ is not a model of $\mathsf{S4}_n^{CJ}$.

Essentially, $M'$ fails to be an appropriate model because $Ip\not \rightarrow Cp$, where I is iterated knowledge.

3.1 Filtrations: The General Modal Case

Filtration is an established technique for producing a finite model from an infinite one so that validity of subformulas is maintained. As in $M^{CJ}$ there are already only a finite number of $R_i$, a finite model must be one in which W is finite. Each world in the finite model will be an equivalency class of worlds in the original model. We look first at a general modal case, where our modality is ‘$\Box$.’ In the following section we apply these techniques to $M'$ to produce finite counter-models to those formulas not provable in $\mathsf{S4}_n^{CJ}$, concluding the proof of completeness.

Definition 5

For a given finite set of formulas $\varPhi$, say two worlds in a model M are equivalent if they agree on all formulas in $\varPhi$:

$$\begin{aligned} s\equiv _\varPhi t\mathrm { \ iff \ }(\forall \psi \in \varPhi )(M,s\Vdash \psi \Leftrightarrow M,t\Vdash \psi ) \end{aligned}$$

and define an equivalence class of worlds

$$\begin{aligned}{}[s]_\varPhi :=\{t \ | \ s\equiv _\varPhi t\}, \end{aligned}$$

or simply [s] if $\varPhi$ is clear.

Note that $\equiv _\varPhi$ is indeed an equivalence relation.

Definition 6

A model $N=\langle S, T_1,\dots ,T_n, \Vdash _N\rangle$ is a filtration of M through $\varPhi$ if M is a model $\langle W, R_1,\dots ,R_n, \Vdash \rangle$ and the following hold:

• $\varPhi$ is a finite set of formulas closed under subformulas;

• $S=\{[w] \ | \ w\in W\}$, which is finite as $\varPhi$ is finite;

• $w\Vdash p \Leftrightarrow [w]\Vdash _Np$ for $p\in Var \cap \varPhi$ and $\Vdash _N$ is extended to all formulas;

• Each relation $T_i$ satisfies the following two properties for all modals $\Box$:

  $min(T_i/R_i):(\forall [s],[t]\in S)(\mathrm {if\ } s'R_it',\ s'\in [s], \mathrm {\ and\ }\ t'\in [t], \mathrm {\ then\ }\ [s]T_i[t])$

  $max(T_i/R_i): (\forall [s], [t]\in S)(\mathrm {if\ } [s]T_i[t], \mathrm {\ then\ }(\forall \Box \psi \in \varPhi )[M,s\Vdash \Box \psi \Rightarrow M,t\Vdash \psi ]).$

The condition $min(T_i/R_i)$ ensures that $T_i$ simulates $R_i$ while $max(T_i/R_i)$ permits adding pairs to $T_i$ independently of $R_i$ if it respects $\Box$. Note that a filtration will always exist as you can define the $T_i$ by reconsidering either condition as a bi-implication. This will give the smallest and largest (not necessarily distinct) filtrations, respectively [8].

Theorem 3

Let N be a filtration of M through $\varPhi$, then

$$\begin{aligned} (\forall \psi \in \varPhi )(\forall s\in W)(M,s\Vdash \psi \Leftrightarrow N,[s]\Vdash _N\psi ). \end{aligned}$$

(3)

Proof

By induction on the complexity of $\psi \in \varPhi$.

• $\psi =p$: by definition of $\Vdash _N$.

• I.H.: As $\varPhi$ closed under subformulas, $M,s\Vdash \psi \Leftrightarrow N,[s]\Vdash _N\psi$ holds for $\psi$ of lower complexity.

• $\psi =\lnot \varphi$: $\ M,s\Vdash \lnot \varphi \Leftrightarrow M,s\not \Vdash \varphi \Leftrightarrow \mathrm {(by\ I.H.)\ }N,[s]\not \Vdash _N\varphi \Leftrightarrow N,[s]\Vdash _N\lnot \varphi$.

• $\psi =\varphi \wedge \varphi '$: $\ M,s\Vdash _M \varphi \wedge \varphi ' \Leftrightarrow$ $M,s\Vdash _M\varphi$ and $M,s\Vdash _M\varphi ' \Leftrightarrow \mathrm {(by\ I.H.)\ }N,[s]\Vdash _N\varphi$ and $N,[s]\Vdash _N\varphi '\Leftrightarrow N,[s]\Vdash _N\varphi \wedge \varphi '$.

• $\psi =\Box \varphi$: $(\Rightarrow )$ Suppose $M,s\Vdash \Box \varphi$. Let [t] be such that [s]T[t]. By $max(T/R),\ M,t\Vdash \varphi$. By I.H. $N,[t]\Vdash _N\varphi$. As [t] was arbitrary, $N,[s]\Vdash _n\Box \varphi$. ($\Leftarrow$) Suppose $N,[s]\Vdash _N\Box \varphi$, so $\forall [t]$ such that $[s]T[t],\ N,[t]\Vdash _N\varphi$. Let $u\in W$ be any state such that sRu, then by $min(T/R)\ [s]T[u]$ so that $N,[u]\Vdash _N\varphi$. By I.H. $M,u\Vdash \varphi$ and since u was an arbitrary world accessible from s, $M,s\Vdash \Box \varphi$.

3.2 Filtrations: The Canonical Structure $M'$ Case

We now consider filtrations in the context of $\mathsf{S4}_n^{CJ}$.

Definition 7

A formula $\varphi$ has a suitable set of subformulas $\varPhi$ if $\varPhi =\varPhi _1\cup \varPhi _2\cup \varPhi _3\cup \varPhi _4$ where for $i\in \{1,\dots ,n\}$:

• $\varPhi _1=\{\psi , \lnot \psi \ | \ \psi$ is a subformula of $\varphi \}$;

• $\varPhi _2=\{K_iK_i\psi , \lnot K_iK_i\psi \ | \ K_i\psi \in \varPhi _1\}$;

• $\varPhi _3=\{K_iJ\psi , \lnot K_iJ\psi , K_i\psi , \lnot K_i\psi \ | \ J\psi \in \varPhi _1\}$;

• $\varPhi _4=\{K_iC\psi , \lnot K_iC\psi , K_i\psi , \lnot K_i\psi \ | \ C\psi \in \varPhi _1\}.$

Crucially, a suitable set is finite and closed under subformulas.

Corollary 2

Let $\varPhi$ be a suitable set for $\varphi$ and M a model such that $M,s\Vdash \varphi$. If N is a filtration of M through $\varPhi$, then $N,[s]\Vdash _N\varphi$.

Proof

By Theorem 3 and $\varphi \in \varPhi$.

Definition 8

For $M'=\langle {W}, {R_1},\dots ,{R_n}, {R_C}, {R_J}, {\Vdash } \rangle$, the canonical structure of $\mathsf{S4}_n^{CJ}$, and a suitable set $\varPhi$ for a consistent formula $\varphi$, define a model $N=\langle S, T_1,\dots ,T_n,T_C,T_J,\Vdash _N\rangle$ such that, for $i\in \{1,2,\dots ,n\}$:

• $S=\{[w] \ | \ w\in W\}$, which is finite as $\varPhi$ is finite;

• $w\ {\Vdash }\ p \Leftrightarrow [w]\Vdash _N p$ for $p\in Var \cap \varPhi$ and $\Vdash _N$ is extended to all formulas;

• $T_i\subseteq S\times S$ such that $[s]T_i[t]\mathrm {\ iff\ }(s\Vdash K_i\psi \Rightarrow t\Vdash \psi )\mathrm {\ for\ those\ }K_i\psi \in \varPhi$;

• $T_C=\big (\bigcup \limits _{i=1}^nT_i\big )^{\mathrm {TC}}$;

• $T_J\subseteq S\times S$ such that $[s]T_J[t]\mathrm {\ iff\ }(s\Vdash J\psi \Rightarrow t \Vdash \psi )\mathrm {\ for\ those\ }J\psi \in \varPhi$.

We now drop the subscript on $\Vdash _N$ to simplify notation. As worlds in N are equivalency classes, it will be clear as to which model is in question.

Lemma 3

N is a model of $\mathsf{S4}_n^{CJ}$ (see Definition 3).

Proof

All accessibility relations are reflexive and transitive and $T_i\subseteq T_C \subseteq T_J$.

• $T_i$ is reflexive: For an arbitrary $s\in [s]$, $(s\Vdash K_i\psi \Rightarrow s\Vdash \psi )$ always holds. If the antecedent is true, then by the definition of $\Vdash$ and the reflexivity of $R_i$, the consequence follows. If the antecedent fails, the implication is vacuously true. Thus for all $[s]\in S,\ [s]T_i[s]$, so $T_i$ is reflexive.

• $T_i$ is transitive: Suppose $[s]T_i[t]$ and $[t]T_i[u]$ and $s\Vdash K_i\psi$ for $K_i\psi \in \varPhi$. As $\varPhi$ is suitable, also $K_iK_i\psi \in \varPhi$. As $R_i$ is transitive, the 4 axiom is sound so we have $(s\Vdash K_i\psi \Rightarrow s\Vdash K_iK_i\psi )$, so as $[s]T_i[t]$ and $K_iK_i\psi \in \varPhi$, ($s\Vdash K_iK_i\psi \Rightarrow t\Vdash K_i\psi$). Since $K_i\psi \in \varPhi$ and $[t]T_i[u]$, $(t\Vdash K_i\psi \Rightarrow u\Vdash \psi )$ so $u\Vdash \psi$. Thus for $K_i\psi \in \varPhi$, $(s\Vdash K_i\psi \Rightarrow u\Vdash \psi )$ holds so $[s]T_i[u]$, hence $T_i$ is transitive.

• $T_C$ is reflexive as for every $[s]\in S$, $[s]T_i[s]$ and $T_i\subseteq T_C$. $T_C$ is transitive by definition.

• $T_J$ is reflexive and transitive by the same reasoning as for $T_i$. It must also be shown that $T_C\subseteq T_J$. Suppose $[s]T_i[t]$, then we want to show $[s]T_J[t]$, i.e. for $J\psi \in \varPhi$, ($s\Vdash J\psi \Rightarrow t\Vdash \psi$) holds. If $J\psi \in \varPhi$, then as $\varPhi$ is suitable, $K_iJ\psi \in \varPhi$. Suppose $s\Vdash J\varphi$, then as $M'$ is sound and $\mathsf{S4}_n^{CJ}\vdash J\varphi \rightarrow K_iJ\varphi$, $s\Vdash K_iJ\varphi$. Then since $[s]T_i[t]$, ($s\Vdash K_iJ\psi \Rightarrow t\Vdash J\psi$) holds, so $t\Vdash J\varphi$ holds, and since $R_J$ is reflexive, $t\Vdash \psi$. Thus for $J\psi \in \varPhi$ and $[s]T_i[t]$, ($s\Vdash J\psi \Rightarrow t\Vdash \psi$) holds, so $[s]T_J[t]$. Since $T_i\subseteq T_J$, $T_C\subseteq T_J$.

Lemma 4

(Definability Lemma). Let $S=\{[s]\ | \ s\in W\}$ for some suitable set $\varPhi$. Then for each subset $D\subseteq S$ there is some characteristic formula $\chi _D$ such that for all $[s]\in S$, $s\Vdash \chi _D\mathrm { \ iff \ }[s]\in D.$ Note that all D are finite as S is.

Proof

Let the set $\bigwedge \{s\}$ be the conjunction of all $\psi \in \varPhi$ that are true at s. By definition of [s], $t \Vdash \bigwedge \{s\}$ iff $[s]=[t]$. Let $\chi _D=\bigvee \limits _{[t]\in D}(\bigwedge \{s\})$.

$$\begin{aligned} s\Vdash \chi _D\Leftrightarrow \ s\Vdash \bigvee \limits _{[t]\in D}\left( \bigwedge \{s\}\right) \Leftrightarrow s\Vdash \bigwedge \{t\}\mathrm {\ for\ some\ }t\in [t]\in D \end{aligned}$$

$$\begin{aligned} \Leftrightarrow [s]=[t]\mathrm {\ for\ some\ }t\in [t]\in D \Leftrightarrow [s]\in D. \end{aligned}$$

Theorem 4

N of Definition 8 is a filtration of $M'$ through $\varPhi$ (cf. [12]).

A relation T is a filtration of R if it satisfies min(T/R) and max(T/R).

Proof

It needs only to be confirmed that the accessibility relations $T_i$, $T_C$, and $T_J$ meet the conditions min(T/R) and max(T/R).

• $T_i:$ $T_i$ satisfies $max(T_i/R_i)$ by definition so it remains to check $min(T_i/R_i)$. Suppose $[s],[t]\in S$ with $s'\in [s]$ and $t'\in [t]$ such that $s'R_it'$. For $K_i\psi \in \varPhi$ we have

  $$\begin{aligned} s\vdash K_i\psi \Leftrightarrow s'\vdash K_i\psi \Rightarrow t'\vdash \psi \Rightarrow t\vdash \psi . \end{aligned}$$

  Thus $[s]T_i[t]$ by definition, satisfying $min(T_i/R_i)$.

• $T_J:$ $T_J$ is a filtration of $R_J$ by the same reasoning as in the $T_i$ case, thus $min(T_J/R_J)$ and $max(T_J/R_J)$ are satisfied.

• $T_C:$ To see that $T_C$ satisfies $min(T_C/R_C)$, suppose that $sR_Ct$. Let $D=\{[w]\in S\ | \ [s]T_C[w]\}$, the set of worlds reachable from [s] by $T_C$. It is sufficient to show

  $$\begin{aligned} s\Vdash C\chi _D, \end{aligned}$$

  (4)

  as then $sR_Ct$ gives $t\Vdash \chi _D$ and so by definition of $\chi _D$, $[t]\in D$ and so $[s]T_C[t]$. Now we show (4).

  As IA is valid in the canonical structure,

  $$\begin{aligned} s\Vdash C(\chi _D\rightarrow E\chi _D)\rightarrow (\chi _D\rightarrow C\chi _D). \end{aligned}$$

  (5)

  To see that $s\Vdash C(\chi _D\rightarrow E\chi _D)$ holds, consider the following. Suppose for some w, $sR_Cw$ and $w\Vdash \chi _D$. We want to show $w\Vdash E\chi _D$, i.e., for all i, $w\Vdash K_i\chi _D$, i.e. for all u, $wR_iu$, $u\Vdash \chi _D$. Since $w\Vdash \chi _D$, $[w]\in D$ so $[s]T_C[w]$. This means there is a path of length l from [s] to [w] along the union of $T_i$s. As each $T_i$ is a filtration of $R_i$ we also have for all those worlds u accessible from w, $[w]T_i[u]$. Thus there is a path of length $l+1$ along the $T_i$s from [s] to [u] and so $[s]T_C[u]$. This means that $u\Vdash \chi _D$, so $w\Vdash E\chi _D$. Since the antecedent of (5) holds, we have $s\Vdash \chi _D\rightarrow C\chi _D$ so in order to conclude (4), we must show $s\Vdash \chi _D$. Which we have by the reflexivity of $T_C$. Thus $T_C$ satisfies $min(T_C/R_C)$.

  $T_C$ must also satisfy $max(T_C/R_C)$. Suppose that $[s]T_C[t]$ and for some $s\in [s]$, $s\Vdash C\psi$ for $C\psi \in \varPhi$. We must show that $t\Vdash \psi$. Note that as $\varPhi$ is suitable, for each i, $K_iC\psi$, i.e. $EC\psi \in \varPhi$ as well. Recall from Proposition 3 that $\mathsf{S4}_n^{CJ}\vdash C\psi \rightarrow EC\psi$ so by soundness, $s\Vdash C\psi \Rightarrow s\Vdash EC\psi$. As $[s]T_C[t]$ and $T_C$ is built from filtrations of the $R_i$s, there is a path of length l along the $R_i$s from s to t. As $s\Vdash EC\psi$ and $EC\psi \in \varPhi$, $C\psi$ also holds at the next world on this path towards t, for whichever $R_i$ used. By induction on the length of the path we get $t\Vdash C\psi$. Since $T_C$ is reflexive we have $t\Vdash \psi$. Thus $T_C$ satisfies $max(T_C/R_C)$.

We can now finish the proof of Theorem 2 that $\mathsf{S4}_n^{CJ}$ is sound and complete with respect to $\mathsf{S4}_n^{CJ}$-models. Soundness was shown in Theorem 1.

Proof

(Proof of Completeness). Suppose $\mathsf{S4}_n^{CJ}\not \vdash \varphi$. Then $\{\lnot \varphi \}$ is contained in some maximal consistent set $\varTheta$ and for the canonical structure $M'$ we have $M',\varTheta \Vdash \lnot \varphi$. Defining a suitable set $\varPhi$ of subformulas of $\lnot \varphi$, we can construct an $\mathsf{S4}_n^{CJ}$-model N (Lemma 3), which, as it happens to be a filtration of $M'$ through $\varPhi$ (Theorem 4), agrees with $M'$ on formulas of $\varPhi$ (Theorem 3) and so $N,[\varTheta ]\not \Vdash \varphi$.

Corollary 3

$\mathsf{S4}_n^{CJ}$ exhibits the Finite Model Property and so is decidable.

Soundness yields the following two propositions.

Proposition 4

$\mathsf{S4}_n^{CJ}\not \vdash C\varphi \rightarrow J\varphi$, as was promised after Proposition 1.

Proof

Consider a model of $\mathsf{S4}_2^{CJ}$ with $W=\{a,b\}$ such that $R_1=R_2=R_C=\{(a,a), (b,b)\}$ and $R_J=\{(a,a), (b,b), (a,b)\}$. Let only $a\Vdash p$ and all other propositional variable fail at both worlds. While $a\Vdash Cp$, $a\not \Vdash Jp$ so $a\not \Vdash Cp\rightarrow Jp$ so $a\Vdash \lnot (C\varphi \rightarrow J\varphi )$, so by soundness $\mathsf{S4}_n^{CJ}\not \vdash (C\varphi \rightarrow J\varphi )$.

Proposition 5

$\mathsf{S4}_n^{CJ}$ is a conservative extension of both $\mathsf{S4}_n^J$ and $\mathsf{S4}_n^C$.

The axiomatization and models of $\mathsf{S4}_n^J$ and $\mathsf{S4}_n^C$ can be obtained by removing C or J, respectively, from the language and axiomatization of $\mathsf{S4}_n^{CJ}$ and $R_C$ or $R_J$ from its models. For more on $\mathsf{S4}_n^J$ see [2, 5, 6]. For more on $\mathsf{S4}_n^C$ see [8, 10, 12].

Proof

Conservativity of $\mathsf{S4}_n^{CJ}$ over $\mathsf{S4}_n^J$: We need to show that for each $\mathsf{S4}_n^J$-formula F, if $\mathsf{S4}_n^{CJ}\vdash F$, then $\mathsf{S4}_n^J\vdash F$. By contraposition, suppose $\mathsf{S4}_n^J\not \vdash F$. Then, by the completeness theorem for $\mathsf{S4}_n^J$, there is a $\mathsf{S4}_n^J$-model M such that F does not hold in M. Now we transform M into an $\mathsf{S4}_n^{CJ}$-model $M^*$ by adding the reachability relation $R_C$. This can always be done and leaves the other components of M unaltered. Since the modal C does not occur in F, the truth values of F in M and in $M^*$ remains unchanged at each world, hence F does not hold in $M^*$. By soundness of $\mathsf{S4}_n^{CJ}$, $\mathsf{S4}_n^{CJ}\not \vdash F$.

Conservativity of $\mathsf{S4}_n^{CJ}$ over $\mathsf{S4}_n^C$: Let G be an $\mathsf{S4}_n^C$-formula not derivable in $\mathsf{S4}_n^C$. We have to show that G is not derivable in $\mathsf{S4}_n^{CJ}$ either. By completeness of $\mathsf{S4}_n^C$ there is an $\mathsf{S4}_n^C$-countermodel N for G. Make N into an $\mathsf{S4}_n^{CJ}$-model $N^*$ by the addition of $R_J$ as the total relation (alternatively, we could put $R_J=R_C$). As G contains no J, at each world, these models agree on the valuation of G, thus G does not hold in $N^*$ either. By soundness, $\mathsf{S4}_n^{CJ}\not \vdash G$.

4 Conclusions

$\mathsf{S4}_n^{CJ}$ is a sound and complete system in which we can directly compare J and C. As $J\varphi \rightarrow C\varphi$, J can be used in place of C in situations in which common knowledge is used, such as in the assumption of common knowledge about game rules or public announcement statements. One advantage of using J over C is the possibility to realize these statements in a explicit justification logic, another is that it maybe a more accurate representation of these scenarios [4, 6]. Another opportunity this logic provides is to examine or develop an interesting class of epistemic scenarios which exploit these nested yet distinct forms of common knowledge. Keeping in mind the connection axioms Con and ConC, C might represent an oracle-like agent while J might also be an infallible agent but one whose statements can be confirmed by evidence if needed.

There is also potential for future syntactic developments. As can be noted by the models of $\mathsf{S4}_n^{CJ}$, the logical strength of J can be chosen independently from that the other agents. For instance, while the $K_i$ and C remain S4 modalities, J could be S5 or perhaps weaker such as K4 to represent belief, while maintaining Con. The logic can also be expanded to encompass multiple distinct J operators.

$\mathsf{S4}_n^{CJ}$ is a logic which provides a context in which to investigate distinct forms of common knowledge. This, together with the conservativity results of Proposition 5, indicate that generic common knowledge is useful generalization of common knowledge with technical and semantic advantages.