Logic of Expertise¶
Note: the paper derived from this work was accepted at the ESSLLI 2021 summer school, and won the prize for “best long paper”.
Syntax¶
We introduce a logical language to express statements about the expertise of an agent. Let \(\prop\) be a countable set of propositional variables, and consider the language \(\cL\) given by the following grammar:
where \(p \in \prop\). Here \(\forall\phi\) is read as the universal modality: \(\phi\) holds everywhere. We read \(E\phi\) as “the agent has expertise on \(\phi\)” and \(S\phi\) as “it is sound for the agent to report \(\phi\)”, in that \(\phi\) is correct up to the lack of expertise of the agent. Note that we allow iterated \(E\) and \(S\) modalities for simplicity, although we shall not have much need for them.
We introduce other binary connectives (\(\or\), \(\rightarrow\), \(\leftrightarrow\)), logical constants (\(\top\), \(\falsum\)) and dual modalities (\(\exists\)) as abbreviations. The propositional language built from \(\prop\) is denoted by \(\cL_\prop\).
Semantics¶
Semantically, we will model expertise via a partition, with the intuition that states in the same partition cell are indistinguishable to the agent.
Definition 1 (Frame, Model)
A partition frame is a pair \(F = (X, \pi)\), where \(X\) is a set of states and \(\pi\) is a partition of \(X\). A partition model is a triple \(M = (X, \pi, v)\) where \((X, \pi)\) is a partition frame and \(v: \prop \to 2^X\) is a valuation function.
Definition 2 (Truth conditions)
Let \(M = (X, \pi, v)\) be a partition model. For \(x \in X\), we set
where \(\|\phi\|_M = \{x \in X \mid M, x \sat \phi\}\). As usual, write \(M \sat \phi\) if \(M, x \sat \phi\) for all \(x \in X\), and \(\sat \phi\) if \(M \sat \phi\) for all partition models \(M\); we say that \(\phi\) is valid in this case. Write \(\phi \equiv \psi\) iff \(\sat \phi \leftrightarrow \psi\).
Remarks. We have the following for all models \(M\) and \(\phi, \psi \in \cL\):
\(E\phi \equiv \forall E \phi \equiv E \neg\phi\)
\(M \sat E\phi \leftrightarrow \top\) or \(M \sat E\phi \leftrightarrow \falsum\)
\(\sat E\top \and E\falsum \and EE\phi\)
\(\sat E\phi \and E\psi \rightarrow E(\phi \and \psi)\)
The distribution axiom K for \(E\) (that is, \(E(\phi \rightarrow \psi) \rightarrow (E\phi \rightarrow E\psi)\)) is not valid
\(\sat \phi \rightarrow S\phi\)
The following result gives an equivalent condition for \(M, x \sat E\phi\).
Lemma 1
Let \(M = (X, \pi, v)\) and \(x \in X\). Then
Proof.
“\(\implies\)”: Suppose \(M, x \sat E\phi\). Then there is a collection of cells \(A \subseteq \pi\) such that \(\|\phi\|_M = \bigcup A\). Let \(y \in \|\phi\|_M\). Then there is some set in \(A\) containing \(y\). But \(\pi[y]\) is the only set in \(\pi\) containing \(y\), so we must have \(\pi[y] \in A\). Conversely, any set in \(A\) is of the form \(\pi[y]\) for some \(y \in X\). We have \(y \in \pi[y] \subseteq \bigcup A = \|\phi\|_M\), i.e. \(y \in \|\phi\|_M\). This shows that \(A = \{\pi[y] \mid y \in \|\phi\|_M\}\), which proves the result.
“\(\impliedby\)”: Set \(A = \{\pi[y] \mid y \in \|\phi\|_M\}\). Clearly \(\bigcup A = \|\phi\|_M\), so \(M, x \sat E\phi\).
Since our notion of expertise is based on partitions of states, it is perhaps unsurprising that there is a close connection with S5 epistemic logic (where the accessability relation for the knowledge modality \(K\) is an equivalence relation). Consider the language \(\cL^*\) defined by
where \(p \in \prop\). We define a translation \(f\) between \(\cL\) and \(\cL^*\) recursively by
For any partition model \(M = (X, \pi, v)\), let \(M^* = (X, R, v)\) denote its corresponding Kripke frame, where \(R\) is the equivalence relation corresponding to \(\pi\). Then \(M^*, x \sat \phi\) is defined in the usual way for a formula \(\phi \in \cL^*\), i.e. \(M^*, x \sat K\phi\) iff \(M^*, y \sat \phi\) for all \(y \in X\) with \(xRy\), and \(M^*, x \sat \forall\phi\) iff \(M^*, y \sat \phi\) for all \(y \in X\).
Proposition 1
Let \(M = (X, \pi, v)\) be a partition model and \(\phi \in \cL\). Then for all \(x \in X\):
Proof.
We go by induction on \(\cL\) formulas.
\(M, x \sat p\) iff \(x \in v(p)\) iff \(M^*, x \sat f(p)\), since \(p = f(p)\) and \(M\) and \(M^*\) share the same valuation \(v\).
\(M, x \sat \phi \and \psi\) iff both \(M, x \sat \phi\) and \(M, x \sat \psi\); by the inductive hypothesis this holds iff \(M^*, x \sat f(\phi)\) and \(M^*, x \sat f(\psi)\), i.e. \(M^*, x \sat f(\phi) \and f(\psi)\). By definition of \(f\), this holds iff \(M^*,x \sat f(\phi \and \psi)\).
Again by the definition of \(f\) and the inductive hypothesis, we have \(M, x \sat \neg \phi\) iff \(M, x \not\sat \phi\) iff \(M^*, x \not\sat f(\phi)\) iff \(M^*, x \sat \neg f(\phi)\) iff \(M^*, x \sat f(\neg\phi)\).
Suppose \(M, x \sat E\phi\). Let \(y \in X\). We need to show that \(M^*, y \sat f(\phi) \rightarrow Kf(\phi)\). Suppose \(M^*, y \sat f(\phi)\). By the inductive hypothesis, \(M, y \sat \phi\), i.e. \(y \in \|\phi\|_M\). Since \(M, x \sat E\phi\), Lemma 1 gives \(\pi[y] \subseteq \|\phi\|_M\). Now take any \(z \in X\) such that \(yRz\). Then, since \(R\) is the equivalence relation corresponding to \(\pi\), we have \(z \in \pi[y]\). Consequently \(z \in \|\phi\|_M\), i.e. \(M, z \sat \phi\). By the inductive hypothesis again, \(M^*, z \sat f(\phi)\). This shows that \(M^*, y \sat Kf(\phi)\). All together we have shown that, for any \(y\), \(M^*, y \sat f(\phi) \rightarrow Kf(\phi)\). Hence \(M^*, x \sat \forall(f(\phi) \rightarrow Kf(\phi))\).
Conversely, suppose \(M^*, x \sat \forall(f(\phi) \rightarrow Kf(\phi))\). We show that the equality on the RHS in the statement of Lemma 1 holds; this will show that \(M, x \sat E\phi\). The right-to-left inclusion is clear since \(y \in \pi[y]\) for all \(y\). For the left-to-right inclusion, suppose \(z \in \pi[y]\) for some \(y \in \|\phi\|_M\). Then \(M^*, y \sat f(\phi)\), and since \(M^*, x \sat \forall(f(\phi) \rightarrow Kf(\phi))\) by assumption, \(M^*, y \sat f(\phi) \rightarrow Kf(\phi)\). Hence \(M^*, y \sat Kf(\phi)\). Since \(z \in \pi[y]\) we have \(yRz\), and thus – by definition of the truth condition for \(K\) – we have \(M^*, z \sat f(\phi)\), i.e. \(M, z \sat \phi\) and \(z \in \|\phi\|_M\). By Lemma 1 we are done.
Suppose \(M, x \sat S\phi\). Then there is some \(y \in \pi[x]\) with \(M, y \sat \phi\), i.e. there is \(y\) with \(xRy\) and \(M^*, y \sat f(\phi)\) (by the inductive hypothesis). Equivalently, \(M^*, y \not\sat \neg f(\phi)\). This shows that \(M^*, x \not\sat K\neg f(\phi)\), i.e. \(M^*, x \sat \neg K \neg f(\phi)\).
Now suppose \(M^*, x \sat \neg K \neg f(\phi)\), i.e. \(M^*, x \not\sat K \neg f(\phi)\). Then there is \(y\) such that \(xRy\) and \(M^*, y \not\sat \neg f(\phi)\), i.e. \(M^* y \sat f(\phi)\) and \(M, y \sat \phi\). Hence \(y \in \pi[x] \cap \|\phi\|_M\), so \(M, x \sat S\phi\).
Finally, \(M, x \sat \forall \phi\) iff \(M, y \sat \phi\) for all \(y \in X\), which by the inductive hypothesis holds iff \(M^*, y \sat f(\phi)\) for all \(y\), i.e. if and only if \(M^*, x \sat \forall f(\phi)\).
This result shows that our soundness operator \(S\) is just the dual of an S5 knowledge operator \(K\), and \(\phi\) is sound if the agent does not know that \(\phi\) is false. Similarly the agent has expertise on \(\phi\) if at any possible state, if \(\phi\) were true then the agent would know it. Note that the equivalence between \(E\phi\) and \(f(E\phi)\) does not hold without the universal modality \(\forall\), since one can construct models \(M\) such that \(M^*, x \sat f(\phi) \rightarrow Kf(\phi)\) at some \(x\) but \(M, x \not\sat E\phi\). 1
Also note that since both \(E\phi\) and \(S\phi\) can be expressed in terms of \(K\) in \(\cL^*\), we can use Proposition 1 to express \(E\phi\) in terms of \(S\phi\). 2
Proposition 2
For any \(\phi \in \cL\),
Proof.
Let \(M\) be a model and \(x \in X_M\). Note that \(\alpha \equiv \beta\) implies \(\forall \alpha \equiv \forall\beta\), so we have
Recall from an earlier remark that \(E\phi \equiv E\neg\phi\). Hence
Hence \(M, x \sat E\phi \leftrightarrow \forall(S\phi \rightarrow \phi)\).
As a consequence of Proposition 2 we also have
where \(\exists\) is an abbreviation for \(\neg\forall\neg\), and the second equivalence comes from the first together with \(E\phi \equiv E\neg\phi\). That is, the agent does not have expertise on \(\phi\) exactly when there is some state where \(\phi\) is false but sound for the agent to claim, or equivalently when there is a state where \(\phi\) is true but its negation is sound.
Axiomatisation¶
Proposition 1 gives a hint that our logic is “S5 in disguise”. Since S5 is axiomatised by the KT5 axioms:
\(K(\phi \rightarrow \psi) \rightarrow (K\phi \rightarrow K\psi)\)
\(K\phi \rightarrow \phi\)
\(\neg K\phi \rightarrow K \neg K \phi\)
there is some hope that the appropriate reformulations of these axioms will also axiomatise the logic of partition frames. This is indeed the case, as we show in this section.
Let \(\sL\) be the logic defined by the following axioms:
All substitution instances of propositional tautlogies
\((\text{K}_S)\): \(S\phi \and \neg S\psi \rightarrow S(\phi \and \neg\psi)\)
\((\text{T}_S)\): \(\phi \rightarrow S\phi\)
\((5_S)\): \(S\neg S\phi \rightarrow \neg S\phi\)
\((\text{K}_\forall)\): \(\forall(\phi \rightarrow \psi) \rightarrow (\forall \phi \rightarrow \forall \psi)\)
\((\text{T}_\forall)\): \(\forall \phi \rightarrow \phi\)
\((5_\forall)\): \(\neg\forall\phi \rightarrow \forall\neg\forall\phi\)
\((\text{ES})\): \(E\phi \leftrightarrow \forall(S\phi \rightarrow \phi)\)
\((\text{Inc})\): \(\forall\phi \rightarrow \neg S \neg \phi\)
and inference rules
\((\text{MP})\): from \(\phi\) and \(\phi \rightarrow \psi\) infer \(\psi\)
\((\text{Nec}_\forall)\): from \(\phi\) infer \(\forall \phi\)
\((\text{R}_S)\): from \(\phi \leftrightarrow \psi\) infer \(S\phi \leftrightarrow S\psi\)
Theorem 1
\(\sL\) is sound and complete with respect to the class of all partition frames.
Soundness is completely routine for the \(\forall\) axioms and inference rules. The \(S\) axioms are also easy (but tedious) to show, and \((\text{ES})\) was shown to be valid in Proposition 2.
For completeness we use a modification of the standard canonical model construction. 3 Let \(\cL_{S,\forall}\) denote the fragment of \(\cL\) without any \(E\phi\) formulas. Let \(\sL_{S,\forall}\) denote the axiom system \(\sL\) without \((\text{ES})\). We write \(\entails \phi\) if \(\phi \in \cL\) and \(\phi\) is a theorem of \(\sL\), and \(\entails_{S,\forall} \phi\) if \(\phi \in \cL_{S,\forall}\) and \(\phi\) is a theorem of \(\sL_{S,\forall}\).
An augmented partition model is a tuple \(N = (X, \pi, R, v)\), where \((X, \pi, v)\) is a partition model and \(R \subseteq X \times X\) is an equivalence relation such that \(x \in \pi[y]\) implies \(xRy\). We introduce a satisfaction relation \(\sataug\) between states in augmented models and \(\cL_{S,\forall}\) formulas, where
and all other formulas interpreted as in regular partition models. That is, we modify the truth condition for \(\forall\phi\) to be interpreted standarly according to the relation \(R\), so that \(\forall\) is not a universal modality in augmented models.
For brevity in what follows, let \(\hat{S}\phi\) be an abbreviation for \(\neg S \neg \phi\). The following lemma shows that the axioms obtained by replacing \(\forall\) with \(\hat{S}\) in \((\text{K}_\forall)\), \((\text{T}_\forall)\) and \((5)_\forall\) are also theorems of \(\sL_{S,\forall}\).
Lemma 2
For any \(\phi, \psi \in \cL_{S,\forall}\),
\(\entails_{S,\forall}\hat{S}(\phi \rightarrow \psi) \rightarrow (\hat{S}\phi \rightarrow \hat{S}\psi)\)
\(\entails_{S,\forall}\hat{S}\phi \rightarrow \phi\)
\(\entails_{S,\forall}\neg\hat{S}\phi \rightarrow \hat{S}\neg\hat{S}\phi\)
Proof.
For the first statement, we start by applying \((\text{K}_S)\) with \(\phi\) and \(\psi\) swapped and negated:
\(S\neg\psi \and \neg S \neg\phi \rightarrow S(\neg\psi \and \neg\neg\phi)\) (instance of \((\text{K}_S)\))
\(\neg S(\neg\psi \and \neg\neg\phi) \rightarrow \neg(S\neg\psi \and \neg S \neg\phi)\) (1, PL)
\(S(\neg\psi \and \neg\neg\phi) \leftrightarrow S\neg(\phi \rightarrow \psi)\) (PL, \((\text{R}_S)\))
\(\neg S(\neg\psi \and \neg\neg\phi) \leftrightarrow \hat{S}(\phi \rightarrow \psi)\) (PL, 3, abbreviation)
\(\hat{S}(\phi \rightarrow \psi) \rightarrow \neg (S \neg\psi \and \neg S \neg \phi)\) (2, 4)
\(\hat{S}(\phi \rightarrow \psi) \rightarrow (\neg S \neg \psi \or \neg\neg S \neg \phi)\) (5, PL)
\(\hat{S}(\phi \rightarrow \psi) \rightarrow (\hat{S}\psi \or \neg \hat{S}\phi)\) (6, abbreviation)
\((\hat{S}\psi \or \neg\hat{S}\phi) \leftrightarrow (\hat{S}\phi \rightarrow \hat{S}\psi)\) (Pl)
\(\hat{S}(\phi \rightarrow \psi) \rightarrow (\hat{S}\phi \rightarrow \hat{S}\psi)\) (7, 8, PL)
For the second statement, we have:
\(\neg\phi \rightarrow S\neg\phi\) (instance of \((\text{T}_S)\))
\(\neg S \neg\phi \rightarrow \neg\neg\phi\) (1, PL)
\(\hat{S}\phi \rightarrow \phi\) (abbreviation, PL)
and for the third:
\(S\neg S\neg\phi \rightarrow \neg S \neg\phi\) (instance of \((5_S)\))
\(S\neg S\neg\phi \rightarrow \hat{S}\phi\) (1, abbreviation)
\(\neg\hat{S}\phi \rightarrow \neg S\neg S\neg\phi\) (2, PL)
\(\neg\hat{S}\phi \rightarrow \neg S\hat{S}\phi\) (3, abbreviation)
\(\hat{S}\phi \leftrightarrow \neg\neg\hat{S}\phi\) (PL)
\(S\hat{S}\phi \leftrightarrow S\neg\neg\hat{S}\phi\) (5, \((\text{R}_S)\))
\(\neg\hat{S}\phi \rightarrow \neg S\neg\neg\hat{S}\phi\) (4, 6, PL)
\(\neg\hat{S}\phi \rightarrow \hat{S}\neg\hat{S}\phi\) (7, abbreviation)
We now show that \(\sL_{S,\forall}\) is complete for augmented frames.
Lemma 3
\(\sL_{S,\forall}\) is complete for \(\cL_{S,\forall}\) with respect to augmented partition frames.
Proof.
Let us introduce some standard terminology and notation. For a set of formulas \(\Gamma \subseteq \cL_{S,\forall}\), write \(\Gamma \entails_{S,\forall} \phi\) if there are \(\psi_1,\ldots,\psi_n \in \Gamma\) such that \(\entails_{S,\forall} \psi_1 \and \cdots \and \psi_n \rightarrow \phi\). Say \(\Gamma\) is inconsistent if \(\Gamma \entails_{S,\forall} \falsum\). Otherwise \(\Gamma\) is consistent. \(\Gamma\) is maximally consistent if is it consistent and \(\Gamma \subset \Gamma'\) implies \(\Gamma'\) is inconsistent.
The following is standard, but I write up the proof as an exercise.
Claim (Lindenbaum’s lemma): For every consistent \(\Gamma\) there is \(\Delta \supseteq \Gamma\) such that \(\Delta\) is maximally consistent.
Proof: Since \(\prop\) is countable, \(\cL_{S,\forall}\) is also countable. Let \((\phi_n)_{n \in \N}\) be an enumeration of \(\cL_{S,\forall}\). Set \(\Delta_0 = \Gamma\), and for each \(n \in \N\):
\[\Delta_{n} = \begin{cases} \Delta_{n-1} \cup \{\phi_n\},& \Delta_{n-1} \cup \{\phi_n\} \text{ consistent} \\ \Delta_{n-1},& \text{ otherwise} \end{cases}\]Note that \(\Delta_{n-1} \subseteq \Delta_n\). Since \(\Delta_0 = \Gamma\) is consistent by assumption, induction on \(n\) shows that \(\Delta_n\) is consistent for all \(n \in \N_0\).
Set \(\Delta = \bigcup_{n \in \N_0}{\Delta_n}\). Clearly \(\Delta \supseteq \Delta_0 = \Gamma\). Suppose for contradiction that \(\Delta\) is inconsistent. Then there are \(\psi_1, \ldots, \psi_k \in \Delta\) and \(\entails_{S,\forall} \psi_1 \and \ldots \and \psi_k \rightarrow \falsum\). For each \(i\), let \(N_i\) be the smallest index such that \(\psi_i \in \Delta_{N_i}\). Set \(N = \max\{N_1,\ldots,N_k\}\). Since the \(\Delta_n\) are \(\subseteq\)-increasing with \(n\), we have \(\Delta_{N_i} \subseteq \Delta_N\) for each \(i\). Hence \(\psi_1,\ldots,\psi_k \in \Delta_N\). But this contradicts consistency of \(\Delta_N\).
It only remains to show that \(\Delta\) is maximal. Suppose \(\Delta \subset \Delta'\). Then there is \(n \in \N\) such that \(\phi_n \in \Delta' \setminus \Delta\). In particular, \(\phi_n \notin \Delta_n\). By definition of \(\Delta_n\), we must have that \(\Delta_{n-1} \cup \{\phi_n\}\) is inconsistent. But \(\Delta_{n-1} \cup \{\phi_n\} \subseteq \Delta'\), so \(\Delta'\) is also inconsistent. This completes the proof.
The following is also useful.
Claim: If \(\Gamma\) is maximally consistent, then
\(\Gamma \entails_{S,\forall} \phi\) implies \(\phi \in \Gamma\)
\(\phi \notin \Gamma\) implies \(\neg\phi \in \Gamma\)
Proof:
By definition, there are \(\psi_1,\ldots,\psi_n \in \Gamma\) such that \(\entails_{S,\forall} \psi_1 \and \cdots \and \psi_n \rightarrow \phi\). This implies that if \(\Gamma \cup \{\phi\}\) were inconsistent, \(\Gamma\) would be too. Hence \(\Gamma \cup \{\phi\}\) is consistent. Since \(\Gamma\) is maximal and \(\Gamma \subseteq \Gamma \cup \{\phi\}\), we must in fact have \(\Gamma = \Gamma \cup \{\phi\}\), i.e. \(\phi \in \Gamma\).
If \(\phi \notin \Gamma\) then \(\Gamma \cup \{\phi\}\) is inconsistent (by maximality). Hence there are \(\psi_1,\ldots,\psi_n \in \Gamma\) such that \(\entails_{S,\forall} \psi_1 \and \cdots \and \psi_n \and \phi \rightarrow \falsum\) (note that \(\phi\) must be included in the conjunction since \(\Gamma\) is consistent). By propositional calculus, \(\entails_{S,\forall} \psi_1 \and \cdots \and \psi_n \rightarrow \neg\phi\), i.e. \(\Gamma \entails_{S,\forall} \neg\phi\). By (1), \(\neg\phi \in \Gamma\).
We construct the canonical (augmented) model. Let \(X\) be the set of all maximally consistent sets. Define relations \(R_S, R_\forall\) on \(X\) by
Claim: \(R_\forall\) is an equivalence relation
Proof: We show reflexivity and the Euclidean property (\(\tilde{\Gamma} R_\forall \Gamma_1\) and \(\tilde{\Gamma} R_\forall \Gamma_2\) implies \(\Gamma_1 R_\forall \Gamma_2\)) which together imply \(R_\forall\) is an equivalence relation. 4
Let \(\Gamma \in X\). Suppose \(\forall\phi \in \Gamma\). By \((\text{T}_\forall)\), \(\entails_{S,\forall} \forall\phi \rightarrow \phi\). Hence \(\Gamma \entails_{S,\forall} \phi\). By maximal consistency, \(\phi \in \Gamma\). This shows \(\Gamma R_\forall \Gamma\), and \(R_\forall\) is reflexive.
For the Euclidean property, suppose \(\tilde{\Gamma} R_\forall \Gamma_1\) and \(\tilde{\Gamma} R_\forall \Gamma_2\). Let \(\forall \phi \in \Gamma_1\). First suppose \(\forall \phi \notin \tilde{\Gamma}\). By part (2) of the ealier claim, \(\neg\forall\phi \in \tilde{\Gamma}\). By \((5_\forall)\), \(\tilde{\Gamma} \entails_{S,\forall} \forall\neg\forall\phi\), so \(\forall\neg\forall\phi \in \tilde{\Gamma}\). Since \(\tilde{\Gamma} R_\forall \Gamma_1\), we get \(\neg\forall\phi \in \Gamma_1\) by definition of \(R_\forall\). But \(\forall\phi \in \Gamma_1\) by assumption, so this contradicts consistency of \(\Gamma_1\). Hence we must have \(\forall\phi \in \tilde{\Gamma}\), and \(\tilde{\Gamma} R_\forall \Gamma_2\) gives \(\phi \in \Gamma_2\). This shows \(\Gamma_1 R_\forall \Gamma_2\).
Note that \(R_S\) is defined in exactly the same way as \(R_\forall\), just with \(\hat{S}\) replacing \(\forall\). The proof that \(R_\forall\) is an equivalence relation only relied on the axioms \((\text{T}_\forall)\) and \((5_\forall)\). By Lemma 2, these axiom schemes also hold in \(\sL_{S,\forall}\) with \(\forall\) replaced by \(\hat{S}\). Therefore an identical proof to the one above shows that \(R_S\) is also an equivalence relation. 5
We also have \(R_S \subseteq R_\forall\). Indeed, if \(\Gamma_1 R_S \Gamma_2\) and \(\forall\phi \in \Gamma_1\), then \(\hat{S}\phi \in \Gamma_1\) by \((\text{Inc})\) and thus \(\phi \in \Gamma_2\); this shows \(\Gamma_1 R_\forall \Gamma_2\).
Now, let \(\pi\) be the partition of \(X\) corresponding to \(R_S\). Set \(N = (X, \pi, R_\forall, v)\), where \(v\) is the canonical valuation
Note that we have \(\Gamma \in \pi[\Gamma'] \implies \Gamma R_\forall \Gamma'\) by \(R_S \subseteq R_\forall\), so \(N\) is an augmented partition model.
Claim (Truth Lemma): For all \(\phi \in \cL_{S,\forall}\) and \(\Gamma \in X\):
\[N, \Gamma \sataug \phi \iff \phi \in \Gamma\]Proof: We proceed by induction on \(\phi\). For \(p \in \prop\) we have by definition of the canonical valuation \(v\) that \(N, \Gamma \sataug p \iff \Gamma \in v(p) \iff p \in \Gamma\). The case for the Boolean connectives \(\neg\phi\) and \(\phi \and \psi\) are straightforward using properties of maximally consistent sets.
Suppose the claim holds for \(\phi\), and consider \(\forall\phi\). First suppose \(\forall\phi \in \Gamma\). Take \(\Gamma'\) such that \(\Gamma R_\forall \Gamma'\). By definition of \(R_\forall\) we have \(\phi \in \Gamma'\). By the inductive hypothesis, \(N, \Gamma' \sataug \phi\). This shows \(N, \Gamma \sataug \forall\phi\).
For the reverse direction we show the contrapositive. Suppose \(\forall\phi \notin \Gamma\). Write
\[Q = \{\psi \mid \forall\psi \in \Gamma\}\]We claim that \(Q \cup \{\neg\phi\}\) is consistent. If not, there are \(\psi_1,\ldots,\psi_k \in Q\) such that
\[\entails_{S,\forall} \psi_1 \and \cdots \and \psi_n \rightarrow \phi \]We can convert this formula to \(n\) nested implications, bring an \(\forall\) infront by \((\text{Nec}_\forall)\), and repeatedly apply \((\text{K}_\forall)\) to move the \(\forall\)s inside the implications:
\(\psi_1 \and \cdots \and \psi_n \rightarrow \phi\) (assumption)
\(\psi_1 \rightarrow ( \cdots \rightarrow (\psi_n \rightarrow \phi) \cdots )\) (PL)
\(\forall(\psi_1 \rightarrow ( \cdots \rightarrow (\psi_n \rightarrow \phi) \cdots ))\) (\((\text{Nec}_\forall)\))
\(\forall\psi_1 \rightarrow \forall(\psi_2 \rightarrow ( \cdots \rightarrow (\psi_n \rightarrow \phi) \cdots ))\) (\((\text{K}_\forall)\), \((\text{MP})\))
\(\forall\psi_1 \rightarrow (\forall\psi_2 \rightarrow \forall(\psi_3 \rightarrow (\cdots\rightarrow(\psi_n\rightarrow\phi)\cdots)))\) (PL, \((\text{K}_\forall)\))
\(\cdots\)
\(\forall\psi_1 \rightarrow ( \cdots \rightarrow (\forall\psi_n \rightarrow \forall\phi) \cdots )\)
\(\forall\psi_1 \and \cdots \and \forall\psi_n \rightarrow \forall\phi\) (PL)
Therefore
\[\entails_{S,\forall} \forall\psi_1 \and \cdots \and \forall\psi_n \rightarrow \forall\phi\]Since \(\forall\psi_i \in \Gamma\) for each \(i\), we get \(\Gamma \entails_{S,\forall} \forall\phi\). But since \(\Gamma\) is maximally consistent, this would imply \(\forall\phi \in \Gamma\), which is not the case. So \(Q \cup \{\neg\phi\}\) must in fact be consistent. By Lindenbaum’s lemma, there is a maximally consistent set \(\Delta \supseteq Q \cup \{\neg\phi\}\). By definition of \(Q\) we have \(\Gamma R_\forall \Delta\). Moreover, \(\neg\phi \in \Delta\) implies \(\phi \notin \Delta\) (by consistency), and \(N, \Delta \not\sataug \phi\) (by the inductive hypothesis). By definition of the semantic clause for \(\forall\phi\) in \(\sataug\), we see \(N, \Gamma \not\sataug \forall\phi\), as required.
Finally, we come to \(S\phi\). If \(S\phi \notin \Gamma\) then \(\neg S\phi \in \Gamma\), and using rule \((\text{R}_S)\) we have \(\hat{S}\neg\phi \in \Gamma\). Let \(\Gamma' \in \pi[\Gamma]\). Then \(\Gamma R_S \Gamma'\), so by definition of \(R_S\), \(\neg \phi \in \Gamma'\). Hence \(\phi \notin \Gamma'\), and by the inductive hypothesis, \(N, \Gamma' \not\sataug \phi\). This shows that \(\pi[\Gamma] \cap \|\phi\|_N = \emptyset\), i.e. \(N, \Gamma \not\sataug S\phi\).
Conversely, suppose \(S\phi \in \Gamma\). As before, write
\[Q = \{\psi \mid \hat{S}\psi \in \Gamma\}\]This time we claim \(Q \cup \{\phi\}\) is consistent. If not, there are \(\psi_1,\ldots,\psi_n \in Q\) such that
\[\entails_{S,\forall} \psi_1 \and \cdots \and \psi_n \rightarrow \neg\phi \]By \((\text{Nec}_\forall)\), \((\text{Inc})\) and \((\text{MP})\) we get
\[\entails_{S,\forall} \hat{S}(\psi_1 \and \cdots \and \psi_n \rightarrow \neg\phi) \]and by propositional calulus
\[\entails_{S,\forall} \hat{S}( \psi_1 \rightarrow (\cdots\rightarrow(\psi_n \rightarrow \neg\phi)\cdots) ) \]Note that this is identical to the formula reached in the proof above for \(\forall\phi\), except that \(\forall\) is replaced with \(\hat{S}\) and \(\phi\) with \(\neg\phi\). In that proof we repeatedly applied \((\text{K}_\forall)\). Since this axiom also holds when \(\forall\) is replaced by \(\hat{S}\) (by Lemma 2), a near identical proof in \(\sL_{S,\forall}\) shows that
\[\entails_{S,\forall} \hat{S}\psi_n \and \cdots \and \hat{S}\psi_n \rightarrow \hat{S}\neg\phi\]Since \(\hat{S}\psi_i \in \Gamma\) for each \(i\), we have \(\Gamma \entails_{S,\forall} \hat{S}\neg\phi\), i.e. \(\hat{S}\neg\phi \in \Gamma\). Expanding the abbreviation and applying \((\text{R}_S)\), we have \(\entails_{S,\forall} \hat{S}\neg\phi \leftrightarrow \neg S \phi\). Hence \(\neg S \phi \in \Gamma\). But \(S\phi \in \Gamma\) by assumption, so this contradicts consistency of \(\Gamma\).
Thus \(Q \cup \{\phi\}\) is indeed consistent, and by Lindenbaum’s lemma there is some maximally consistent \(\Delta \supseteq Q \cup \{\phi\}\). By construction of \(Q\) we have \(\Gamma R_S \Delta\), so \(\Delta \in \pi[\Gamma]\). Also, \(\phi \in \Delta\) implies \(N, \Delta \sataug \phi\) by the inductive hypothesis, i.e. \(\Delta \in \|\phi\|_N\). Hence \(\Delta \in \pi[\Gamma] \cap \|\phi\|_N\). In particular, this set is non-empty, so \(N, \Gamma \sataug S\phi\).
We are finally ready to show completeness. We show the contrapositive. Suppose \(\not\entails_{S,\forall}\phi\). Then \(\{\neg\phi\}\) is consistent. Let \(\Delta\) be a maximally consistent set containing \(\neg\phi\). By the truth lemma, \(N, \Delta \sataug \neg\phi\), so \(N, \Delta \not\sataug \phi\), i.e. \(\phi\) is not valid in all augmented partition frames.
This allows us to prove the same result for non-augmented frames.
Lemma 4
\(\sL_{S,\forall}\) is complete for \(\cL_{S,\forall}\) with respect to (non-augmented) partition frames.
Proof.
Again, we show the contrapositive. Suppose \(\not\entails_{S,\forall} \phi\), where \(\phi \in \cL_{S,\forall}\). Then by Lemma 3, there is an augmented model \(N = (X, \pi, R, v)\) and a point \(x \in X\) such that \(N, x \not\sataug \phi\). Let \(X' = \{y \in X \mid xRy\}\) be the equivalence class of \(x\) in \(R\). Note that if \(y \in X'\) and \(yRz\), then \(z \in X'\) too. We can therefore consider the generated sub-model \(N' = (X', \pi', R', v')\) where
It is easy to see that \(\pi'\) is a partition of \(X'\). Since \(X'\) is an equivalence class of \(R\), we see that \(R' = X' \times X'\); in particular, \(R'\) is an equivalence relation over \(X'\), and \(y \in \pi'[z]\) implies \(yR'z\). Hence \(N'\) is an augmented model.
It follows that \(N, y \sataug \psi\) iff \(N', y \sataug \psi\) for all \(\psi\) and \(y \in X'\), since the identity relation on \(X'\) is a bisimulation between \(N\) and \(N'\) [BVB07]. But for the sake of self-containment, we show this directly.
Claim: For any \(\psi \in \cL_{S,\forall}\) and \(y \in X'\),
\[N', y \sataug \psi \iff N, y \sataug \psi \]Proof: As usual, we proceed by induction on formulas. The cases for atomic formulas, negations and conjunctions are straightforward.
If \(N', y \sataug S\psi\), there is \(z \in \pi'[y]\) such that \(N', z \sataug \psi\). By definition of \(\pi'\) and the inductive hypothesis, \(z \in \pi[y]\) and \(N, z \sataug \psi\). Hence \(N, y \sataug S\psi\). Conversely, if \(N, y \sataug S\psi\) there is \(z \in \pi[y]\) such that \(N, z \sataug \psi\). By definition of an augmented model, \(z \in \pi[y]\) implies \(zRy\), which implies \(yRz\) by symmetry of \(R\). Since \(y \in X'\), this shows \(z \in X'\) too. Hence \(z \in \pi[y] \cap X' = \pi'[y]\), and \(N', z \sataug \psi\) by the inductive hypothesis. Hence \(N', y \sataug S\psi\).
Now suppose \(N', y \sataug \forall \psi\). Let \(z \in X\) such that \(yRz\). Then, since \(y \in X'\), \(xRz\) by transitivity of \(R\), and \(z \in X'\). Hence \(yR'z\), so \(N', z \sataug \psi\). By the inductive hypothesis, \(N, z \sataug \psi\). This shows that \(N, y \sataug \forall\psi\). Finally, suppose \(N, y \sataug \forall\psi\). Suppose \(yR'z\). Then \(yRz\) and \(z \in X'\). This means \(N, z \sataug \psi\) and \(N', z \sataug \psi\) by the inductive hypothesis. This shows \(N', y \sataug \forall\psi\), as required.
Now, let \(M' = (X', \pi', v')\) be the partition model obtained by simply dropping the \(R'\) component of \(N'\). Then \(M'\) satisfies exactly the same formulas under the standard partition model semantics as \(N'\) does under the augmented semantics:
Claim: For any \(\psi \in \cL_{S,\forall}\) and \(y \in X'\),
\[M', y \sat \psi \iff N', y \sataug \psi\]Proof: We go by induction on formulas. Note that the truth conditions for atomic formulas, negations, conjunctions and formulas of the form \(S\psi\) are exactly the same for \(\sat\) and \(\sataug\), and do not refer to the relation \(R\). Since \(M'\) and \(N'\) share the same partition and valuation, these cases are trivial. We only need to show that, assuming the claim holds for \(\psi\),
\[M', y \sat \forall \psi \iff N', y \sataug \forall\psi\]The RHS holds if and only if \(N', z \sataug \psi\) for all \(z \in X'\) with \(yR'z\). By the inductive hypothesis, this is equivalent to \(M', z \sat \psi\) for all such \(z\). But recall that, by definition of \(R'\) and choice of \(X'\), \(R'\) is the universal relation \(R' = X' \times X'\). Thus the set \(\{z \in X' \mid yR'z\}\) is just \(X'\). Hence the RHS is equivalent to \(M', z \sat \psi\) for all \(z \in X'\), i.e. \(M', y \sat \forall\psi\), and we are done.
Combining the two claims, we see that \(N, x \not\sataug \phi\) implies \(N', x \not\sataug \phi\) (since clearly \(x \in X'\)), which in turn implies \(M', x \not\sat \phi\). Consequently, \(M'\) is a partition model in which \(\phi\) is refuted, so \(\not\sat \phi\). This proves the completeness result.
We return to the full language \(\cL\) and axiom system \(\sL\) by showing that every \(\cL\) formula has an \(\cL_{S,\forall}\) counterpart to which it is both semantically equivalent and \(\sL\)-equivalent.
Lemma 5
For all \(\phi \in \cL\) there is \(\psi \in \cL_{S,\forall}\) such that \(\entails \phi \leftrightarrow \psi\) and \(\phi \equiv \psi\).
Proof.
Define \(g: \cL \to \cL_{S,\forall}\) by
That is, \(g\) simply recursively replaces \(E\phi\) with \(\forall(S\phi \rightarrow \phi)\). Straightforward induction shows that \(\entails \phi \leftrightarrow g(\phi)\). For \(S\phi\) we use \((\text{R}_S)\); for \(\forall\phi\) we use \((\text{Nec}_\forall)\) and \((\text{K}_\forall)\); and for \(E\phi\) we use these axioms and rules together with \((\text{ES})\). The other cases only require the propositional calculus.
The semantic equivalence \(\phi \equiv g(\phi)\) is also easy to show by induction, using Proposition 2 for the \(E\phi\) case.
We put these results together to obtain the completeness required for Theorem 1.
Lemma 6
\(\sL\) is complete for \(\cL\) with respect to partition frames.
Proof.
Suppose \(\phi \in \cL\) is valid in all partition frames. By Lemma 5 there is \(\psi \in \cL_{S,\forall}\) such that \(\entails \phi \leftrightarrow \psi\) and \(\phi \equiv \psi\). Hence \(\psi\) is also valid. By completeness of \(\sL_{S,\forall}\) (Lemma 4) we get \(\entails_{S,\forall} \psi\). Since \(\sL\) extends \(\sL_{S,\forall}\), we also have \(\entails \psi\). Finally, since \(\entails \phi \leftrightarrow \psi\), we get \(\entails \phi\).
Belief Revision¶
Consider a function which, given a sequence of reports from the agent which are assumed to be sound, aims to infer the expertise of the agent.
Definition 3
An operator is a function \(B: (\cL_\prop)^* \to 2^\cL\) mapping each finite sequence \(\mu = (\phi_1,\ldots,\phi_n)\) to a belief set \(B(\mu)\).
Notation. For \(\Gamma, \Delta \subseteq \cL\), write \(\cn{\Gamma} = \{\phi \in \cL \mid \Gamma \entails \phi\}\) 6 and \(\Gamma + \Delta = \cn{\Gamma \cup \Delta}\). For a sequence \(\mu\) write
We can state AGM-like postulates for \(B\).
(B1) \(\cn{B(\mu)} = B(\mu)\)
(B2) \(B(\mu) \entails \Psi_\mu\)
(B3) \(B(\mu) \not\entails \falsum\)
(B4) If \(\entails \Psi_\mu \leftrightarrow \Psi_\delta\) then \(B(\mu) = B(\delta)\)
(B5) \(B(\mu \concat \delta) \subseteq B(\mu) + \{\Psi_\delta\}\)
(B6) If \(B(\mu) \not\entails \neg\Psi_\delta\) then \(B(\mu \concat \delta) \supseteq B(\mu) + \{\Psi_\delta\}\)
For a semantic perspective, fix a set \(X\) and valuation \(v\) on \(X\). For a partition \(\pi\) of \(X\), form a model \(M_\pi = (X, \pi, v)\). Then to each \(\sigma\) we can associate a set
of state/partition pairs which satisfy all formulas in the belief set.
We can also consider extending the definition of an operator to allow for historical reports, where the agent reported \(\phi\), say, at some previous time at which \(\alpha\) was known to be true. Again assuming that reports are sound, this situation is represented by the formula
The input to \(B\) now becomes a sequence of elements of the form \((\alpha, \phi)\) or \(({?}, \phi)\), where \(\alpha,\phi \in \cL_\prop\) and \(?\) is a constant symbol. For a sequence \(\sigma\) of this form we can define \(\Psi_\sigma = \bigand_{(\alpha,\phi)\in\sigma}{S_\alpha\phi} \and \bigand_{({?},\phi)\in\sigma}{S\phi}\), and the postulates above remain much the same.
Alternative Semantics¶
Note that in taking relational-style semantics, the partition \(\pi\) used to evaluate the \(E\phi\) and \(S\phi\) formulas is fixed across the whole model. An alternative approach is to drop the fixed partition from a model and evaluate formulas at pairs \((x, \pi)\), where \(x\) is a state and \(\pi\) a partition. This puts the states and partitions on equal footing, which may appear more natural.
Formally, a model is a pair \(M=(X, v)\) where \(X\) is a set of states and \(v: \prop \to 2^X\) a valuation. The valuation \(v\) may be extended to the propositional language \(\cL_\prop\) by setting \(v(\neg\phi) = X \setminus v(\phi)\) and \(v(\phi \and \psi) = v(\phi) \cap v(\psi)\). For each \(x \in X\) and each partition \(\pi\) of \(X\), define
Note that we have restricted the modal operators to act on propositional formulas only (e.g. we do not define what it means for formulas such as \(ESp\) to be satisfied in a model). This seems necessary if one wishes to evaluate formulas at pairs \((x, \pi)\).
Remarks.
Under these semantics it is no longer the case that \(E\phi \equiv \forall(S\phi \rightarrow \phi)\), since \(\forall\) quantifies over partitions as well as states. To recover some relation between \(E\) and \(S\) we could introduce a new modality \(\forall_\mathcal{X}\), where
\[x, \pi \sat_M \forall_\mathcal{X}\phi \iff x', \pi \sat_M \phi \text{ for all } x' \in X\]Then we have \(E\phi \equiv \forall_\mathcal{X}(S\phi \rightarrow \phi)\).
We might not need the level of generality afforded by an abstract set of states \(X\) with a valuation \(v\) determining the truth of the propositional variables. Instead, we could just fix \(X\) to be the set of propositional valuations over \(\prop\) so that the notion of a model \(M = (X, v)\) is no longer needed.
- 1
For example, take \(X = \{1,2,3,4\}\) and \(\pi = \{\{1,2\}, \{3,4\}\}\). Take some variable \(p \in \prop\), and define \(v\) by \(v(p) = \{1,2,3\}\) and \(v(q) = \emptyset\) for \(q \ne p\). Then \(\|p\|_M = \{1,2,3\}\), and it easily observed that \(M \sat \neg Ep\). However, \(M^*, 4 \sat p \rightarrow Kp\) since \(p\) is false at \(4\).
In fact, this model remains a counterexample even if we consider a stronger candidate for \(f(Ep)\):
\[(p \rightarrow Kp) \and (\neg p \rightarrow K\neg p) \]For example, \(M^*, 1 \sat p \and Kp\), so \(M^*, 1 \sat (p \rightarrow Kp) \and (\neg p \rightarrow K\neg p)\), yet \(M, 1 \not\sat Ep\).
- 2
Note that this result is also easy to prove directly, without going via Proposition 1.
- 3
The ideas come from the proof of the axiomatisation in [Bon05] and references therein.
- 4
For symmetry, note that if \(\Gamma_1 R_\forall \Gamma_2\) then, since \(\Gamma_1 R_\forall \Gamma_1\) by reflexivity, \(\Gamma_2 R_\forall \Gamma_1\) by the Euclidean property. For transitivity, note that if \(\Gamma_1 R_\forall \Gamma_2\) and \(\Gamma_2 R_\forall \Gamma_3\), then by symmetry \(\Gamma_2 R_\forall \Gamma_1\), and the Euclidean property gives \(\Gamma_1 R_\forall \Gamma_3\).
- 5
Note that we could have just stated the axioms for \(S\) in the desired form directly, and saved some work here. However, I feel the axioms have more intuitive meaning expressed in terms of \(S\) as compared to \(\hat{S}\).
- 6
Note that \(\Gamma \entails \phi\) implies \(\Gamma \sat \phi\) by soundness of \(\sL\). The converse holds for finite \(\Gamma\) by completeness. The converse holds for arbitrary \(\Gamma\) if \(\cL\) is compact; that is, if any \(\Gamma \subseteq \cL\) is guaranteed to be satisfiable whenever all of its finite subsets \(\Delta \subseteq \Gamma\) are satisfiable. I do not know whether we have compactness here.