Learning-based truth tracking (1)¶
Introduction¶
What can be learned on the basis of unreliable reports?
We investigate this question using notions of verifiability and learnability from [BGS16][GK17][KSH97].
We consider both learning facts about the world as well as the epistemic state of information sources.
We use modal epistemic logic to describe both aspects
Framework¶
Syntax¶
Fix a countable set of propositional atoms \(\prop\), and let \(\lprop\) be the propositional language built from \(\prop\) with the usual connectives. Let \(\S\) be a finite set of sources, and let \(\l\) be the modal language defined by the following grammar:
where \(p \in \prop\) and \(i \in \S\). We read \(\K_i\phi\) as “\(i\) knows \(\phi\)” and \(\A\phi\) as “\(\phi\) holds in every state”.
Semantics¶
A model is a triple \(M = (X, (R_i)_{i \in \S}, V)\) where \(X\) is a set of states, \(R_i\) is an equivalence relation on \(X\) for each \(i \in \S\), and \(V: \prop \to 2^X\) is a valuation. We extend \(V\) to \(\lprop\) in the obvious way. A pointed model is a pair \((M, x)\) where \(x\) is a state in \(M\). The truth conditions for \(\l\) formulas at a pointed model \((M, x)\) are defined inductively in the standard way:
For a set \(\Gamma \subseteq \l\), write \(M, x \models \Gamma\) iff \(M, x \models \phi\) for all \(\phi \in \Gamma\).
Call a pair \(\D = (X, V)\), where \(X\) is a set and \(V\) a valuation on \(X\), a domain. Let \(\Omega_\D\) be the set of pointed models \((M, x)\) where \(M\) is a model with \(X\) and \(V\) as its state space and valuation, respectively. For a set of formulas \(\Gamma \subseteq \l\) and a domain \(\D\), write
for the set of pointed models (over \(\D\)) satisfying all formulas in \(\Gamma\). For sets \(\Gamma, \Delta \subseteq \l\), write \(\Gamma \models_\D \Delta\) iff \(\|\Gamma\|_\D \subseteq \|\Delta\|_\D\).
Learners¶
Let \(\Sigma = (\S \times \lprop)^*\) be the set of finite sequences of pairs \((i, \alpha)\), for a source \(i\) and a propositional formula \(\alpha\). A learner is a function \(L: \Sigma \to 2^\l\), i.e. \(L\) produces a belief set \(L(\sigma)\) for each finite sequence of reports \(\sigma \in \Sigma\).
Verifiability¶
The definitions in this section will be made with respect to a fixed domain \(\D = (X, V)\). We will think of a pointed model \(w = (M, x) \in \Omega_\D\) as a “possible world”, for \(w\) carries with it a notion of what is true of the world (via the “actual” state \(x \in X\)) and the epistemic state of the sources (via the relations \(R_i\) in \(M\)).
Supposing \(w\) is the “actual” world, we suppose that the sources reveal their epistemic state over time by making reports. To start with, we will assume sources (eventually) report all that they consider possible. 1 Formally, a stream for \(w = (M, x)\) is an infinite sequence \(\rho \in (\S \times \lprop)^\infty\) such that
If \((i, \alpha) \in \rho\) then \(M, x \models \neg\K_i\neg\alpha\)
If \(M, x \models \neg\K_i\neg\alpha\) then \((i, \alpha) \in \rho\)
For \(n \in \N\), write \(\rho[n] \in \Sigma\) for the finite initial segment of \(\rho\) of length \(n\). A set \(I \subseteq \N\) is cofinite iff its complement \(\N \setminus I\) is finite.
Definition 1
A learner \(L\) verifies a set of formulas \(\Gamma \subseteq \l\) iff for all \((M, x) \in \Omega_\D\) and all streams \(\rho\) for \((M, x)\),
That is, \(L\) verifies \(\Gamma\) if, for every world and every possible stream, \(\Gamma\) is true if and only if \(L\) eventually converges to belief in \(\Gamma\). Say \(\Gamma\) is verifiable if there is some \(L\) which verifies \(\Gamma\). Say \(\phi\) is verifiable if \(\{\phi\}\) is.
Examples¶
Example 1. Suppose \(\alpha \in \lprop\) is such that \(\emptyset \subset V(\alpha) \subset X\), i.e. both \(\alpha\) and \(\neg\alpha\) are both satisfiable. Then \(\alpha\) is not verifiable.
This comes from the fact that it is possible for all sources to have “no knowledge”, i.e. know only the validities of a model. In this case a stream carries no information about \(\alpha\), so a learner cannot deduce anything about \(\alpha\) from the stream alone.
Proof.
Take \(x \in V(\alpha)\) and \(y \in X \setminus V(\alpha)\). Let \(M\) be the model over \(X, V\) where \(R_i = X \times X\) for all \(i \in \S\). Then \(M, z \models \K_i\phi\) iff \(M, z \models \A\phi\) for each \(z \in X\) and \(i \in \S\), i.e. sources only know the validities of \(M\). Set \(w_1 = (M, x)\) and \(w_2 = (M, y)\). It follows that \(w_1 \models \K_i\phi\) iff \(w_2 \models \K_i\phi\).
For contradiction, suppose there is some learner \(L\) which verifies \(\alpha\). Let \(\rho\) be any stream for \(w_1\). Since \(w_1 \models \alpha\), we have \(\alpha \in L(\rho[n])\) for sufficiently large \(n\).
But since \(w_1\) and \(w_2\) satisfy the same knowledge formulas, it follows that \(\rho\) is also a stream for \(w_2\). Since \(w_2 \not\models \alpha\), verifiability gives \(\alpha \notin L(\rho[n])\) for infinitely many \(n\) – contradiction.
Example 2. Write \(\KW_i\phi\) as an abbreviation for \(\K_i\phi \lor \K_i\neg\phi\), i.e. \(i\) “knows whether” or not \(\phi\) holds. Then \(\KW_i\alpha\) is verifiable.
Proof.
Fix \(i \in \S\) and \(\alpha \in \lprop\). Define a learner \(L\) as follows:
That is, we believe \(i\) knows whether \(\alpha\) unless \(i\) explicitly reports both \(\alpha\) and \(\neg\alpha\). We show \(L\) verifies \(\KW_i\alpha\). Take any \(w = (M, x) \in \Omega_\D\) and let \(\rho\) be a stream for \(w\).
First suppose \(w \models \KW_i\alpha\). We show that \((i, \alpha)\) and \((i, \neg\alpha)\) do not both appear in \(\rho\). Indeed, suppose \((i, \alpha) \in \rho\). Then by condition (1) in the definition of a stream, \(w \models \neg\K_i\neg\alpha\). From \(w \models \KW_i\alpha\) we get \(w \models \K_i\alpha\), so \(w \not\models \neg\K_i\neg\neg\alpha\). By condition (1) again, \((i, \neg\alpha) \notin \rho\). Consequently we have that \(\rho[n]\) always falls into the second case in the definition of \(L\) for any \(n\), and thus \(\KW_i\alpha \in L(\rho[n])\).
For the other direction, suppose \(w \not\models \KW_i\alpha\). Then \(w \models \neg\K_i\alpha \land \neg\K_i\neg\alpha\). By condition (2) in the definition of a stream, we have \((i, \alpha), (i, \neg\alpha) \in \rho\). Thus \(\rho[n]\) falls into the first case of the definition of \(L\) for sufficiently large \(n\), and hence \(\KW_i\alpha \notin L(\rho[n])\) for all such \(n\). In particular, \(\KW_i\alpha \notin L(\rho[n])\) for infinitely many \(n\), so the condition in Definition 1 is satisfied.
Background knowledge¶
Example 1 shows that no nontrivial facts about the world can be verified if we know nothing about the epistemic state of the sources. Can the situation improve if our learners are given some “background knowledge” about the sources?
More generally we can consider arbitrary background knowledge.
Definition 2
A learner \(L\) verifies \(\Gamma\) with respect to background knowledge \(\Delta\) iff for all \((M, x) \in \|\Delta\|_\D\) and all streams \(\rho\) for \((M, x)\),
This is a simple modification of Definition 1, in which we require convergence to belief in \(\Gamma\) iff \(\Gamma\) holds only for worlds which satisfy \(\Delta\). Here we can imagine that the learner \(L\) has knowledge \(\Delta\) “built in”. 2 Say \(\Gamma\) is verifiable wrt \(\Delta\) if there is a learner which verifies \(\Gamma\) wrt \(\Delta\).
Example 3. Both \(\alpha\) and \(\neg\alpha\) are verifiable wrt \(\KW_i\alpha\).
Proof. We define a single learner which verifies both \(\alpha\) and \(\neg\alpha\) wrt \(\KW_i\alpha\). Set
TODO: finish writing after lunch.