ora-0073

4.11 Assimilation as conservative lifting

For an evidence extension \(u:T\to T'\) under a fixed doctrine \(\mathbb T\), restriction gives

\[ u^*:\mathsf H_{\mathbb T}(T') \longrightarrow \mathsf H_{\mathbb T}(T). \]

Suppose the learner currently holds \(M\in \mathsf H_{\mathbb T}(T)\).

Definition 4.9 Categorical assimilation

An assimilation of \(T'\) into \(M\) is a choice \(M'\in \mathsf H_{\mathbb T}(T')\) together with a registered comparison \(u^*M'\to M\) that preserves a declared subtheory of settled queries. It is conservative when that comparison is an equivalence on the settled subtheory.

Assimilation need not leave every belief unchanged. It enriches a model with new objects, arrows, composites, or overlap warrants while requiring the validated part of the old interpretation to survive. The declaration of the settled subtheory prevents “preservation” from becoming an all-or-nothing condition.

Proposition 4.10 Persistence under conservative assimilation

Let \(\mathcal Q_0\) be a settled query subtheory. If \(M'\) conservatively assimilates \(T'\) into \(M\), then every answer in \(\operatorname {Th}_{\mathcal Q_0}(M)\) is preserved by \(M'\).

Proof ▼

By definition the comparison \(u^*M'\to M\) is an equivalence for the semantics of every query in \(\mathcal Q_0\). Query answers invariant under that equivalence therefore agree.

The content lies in choosing \(\mathcal Q_0\) before seeing the desired outcome. If the learner is free to declare every overwritten conclusion unsettled after the fact, the persistence claim is vacuous.