A Characterization Theorem for Trackable Updates

Abstract

The information available to some agents can be represented with several mathematical models, depending on one’s purpose. These models differ not only in their level of precision, but also in how they evolve when the agents receive new data. The notion of tracking was introduced to describe the matching of information dynamics, or ‘updates’, on different structures.

We expand on the topic of tracking, focusing on the example of plausibility and evidence models, two central structures in the literature on formal epistemology. Our main result is a characterization of the trackable updates of a certain class, that is, we give the exact condition for an update on evidence models to be trackable by a an update on plausibility models. For the positive cases we offer a procedure to compute the other update, while for the negative cases we give a recipe to construct a counterexample to tracking. To our knowledge, this is the first result of this kind in the literature.

A Appendix: Application of Theorem 2

In this appendix we show how our main result can be applied, deriving the update ‘collapse of X’ (Definition 7) from the update ‘evidence weakening of X’ (Definition 6). This will showcase how our characterization result solves the problem of finding the tracking companion for a given update.

We start by encoding evidence weakening in a formula $\alpha$ of the evidence language, using P as the unary predicate that is meant to be interpreted on X:

$$ \alpha (n, P, \mathcal {E}) := \exists n' (\mathcal {E}(n')\wedge \forall x\, x\in n \leftrightarrow (x\in n'\vee Px)) $$

Intuitively this formula is saying ‘a set n is a piece of evidence in the updated model iff there exists an evidence set $n'$ in the original model such that $n = n'\cup X$’. Note that this is a simple update, where $\phi (x, n', P) = (x\in n'\vee Px)$ and $\theta (x, n', P) = \top$.

Evidence weakening satisfies the premises of our Theorem; this ensures that we can apply the procedure to find its tracking companion. As we know from Proposition 4, it is sufficient to show that, for $\alpha (n, P, \mathcal {E})$ as above, the formula

$$ \forall n (\alpha (n, P, \mathcal {E})\rightarrow (y\in n\rightarrow x\in n)) $$

is equivalent to a formula $\beta (x, y, P, \le _{\mathcal {E}})\in FOL(P, \le _{\mathcal {E}})$. Thus we proceed manipulate the formula syntactically exploiting various first-order and propositional laws. Starting from

$$ \forall n (\alpha (n, P, \mathcal {E})\rightarrow (y\in n\rightarrow x\in n)) $$

we plug in $\alpha$ and obtain

$$ \forall n ( \exists n' (\mathcal {E}(n')\wedge \forall z\, z\in n \leftrightarrow (z\in n'\vee Pz))\rightarrow (y\in n\rightarrow x\in n)) $$

From this formula we extract the existential quantifier:

$$ \forall n, \forall n' (\mathcal {E}(n')\wedge \forall z\, z\in n \leftrightarrow (z\in n'\vee Pz))\rightarrow (y\in n\rightarrow x\in n) $$

Now we eliminate the quantifier over n exploiting the bi-conditional, substituting the instances of $x\in n$ and $y\in n$:

$$ \forall n' (\mathcal {E}(n')\rightarrow ((y\in n'\vee Py)\rightarrow (x\in n'\vee Px))) $$

We proceed to split the first disjunction into two implications.

$$ \forall n' (\mathcal {E}(n')\rightarrow ([(y\in n')\rightarrow (x\in n'\vee Px)]\wedge [( Py)\rightarrow (x\in n'\vee Px)])) $$

We can then distribute the outermost implication and the quantifier over the conjunction, obtaining

$$\begin{aligned}&\forall n' (\mathcal {E}(n')\rightarrow [(y\in n')\rightarrow (x\in n'\vee Px)]) \wedge \\&\forall n' (\mathcal {E}(n')\rightarrow [(Py)\rightarrow (x\in n'\vee Px)]) \end{aligned}$$

The next step is to rewrite the innermost disjunctions as implications.

$$\begin{aligned}&\forall n' (\mathcal {E}(n')\rightarrow [(y\in n')\rightarrow (\lnot Px \rightarrow x\in n' )]) \wedge \\&\forall n' (\mathcal {E}(n')\rightarrow [(Py)\rightarrow (\lnot Px \rightarrow x\in n')]) \end{aligned}$$

Since $n'$ does not feature in the literals Px or Py or their negations, we can pull out these formulas from the quantifications.

$$\begin{aligned}&[\lnot Px \rightarrow \forall n' (\mathcal {E}(n')\rightarrow ((y\in n')\rightarrow ( x\in n' )))] \wedge \\&[(Py \wedge \lnot Px) \rightarrow \forall n' (\mathcal {E}(n')\rightarrow x\in n')] \end{aligned}$$

Finally, using the definition of $\le _{\mathcal {E}}$, we can rewrite the last formula as

$$ \beta (x, y, P, \le _{\mathcal {E}}) :=[\lnot Px \rightarrow x\le _{\mathcal {E}} y] \wedge [(Py \wedge \lnot Px) \rightarrow \forall z\, x\le _{\mathcal {E}} z] $$

The equivalence of $\forall z\, x\le _{\mathcal {E}} z$ and $\forall n' (\mathcal {E}(n')\rightarrow x\in n')$ over evidence models is an easy check.

Proposition 4 argued that the tracking companion of evidence weakening is defined by $\beta (x, y, P, \le )$ (which is just $\beta (x, y, P, \le _{\mathcal {E}})$ where we have substituted the relation $\le _{\mathcal {E}}$ with $\le$). In this case this means that two elements a and b are in the new, updated relation if and only if they satisfy $\beta (x, y, P, \le )$. Is is easy to see that $\beta (x, y, P, \le )$ defines exactly the collapse update of Definition 7: $(a, b)\in coll(\le )$ if and only if $\beta (x, y, P, \le )$ is true when instantiated to (a, b) if and only if one of the following is the case

• $a\in X$ (recall that P is interpreted on the set X);

• $a\not \in X$, $b\not \in X$ and $a \le b$;

• $a\not \in X$, $b\in X$ and $\forall z\, a \le z$.

The reader is invited to contrast this with Definition 7. The manipulations showed in this section are part of a general strategy to reduce the updates of the right shape into formulas of the fragment $FOL(P, \le _{\mathcal {E}})$, giving us a procedure to compute the tracking companion.