ora-0191

17.2 The first next rung: finite doctrine stabilization

The exact finite identification theorem of Chapter 7 works inside one residual hypothesis fiber. Doctrine learning requires the version space itself to range over fibers. Let

\[ p:\mathcal E\longrightarrow \mathcal B \]

be the hypothesis fibration, with doctrines $b\in \mathcal B$ and realizations $M\in \mathcal E_b$. A doctrinal candidate is a pair $(b,M)$. The declared query family $\mathcal Q$ induces an equivalence

\[ \begin{aligned} (b,M)\simeq _{\mathcal Q}(b’,M’) \quad \Longleftrightarrow \quad & \text{every admissible query has equivalent}\\[-2pt]& \text{answers on $M$ and $M'$.} \end{aligned} \]

This quotient is essential. Interaction may identify what a world answers without identifying the syntax, presentation, or doctrine used to express it.

At time $t$, let $V_t$ be the set of viable $\simeq _{\mathcal Q}$-classes after the transcript $T_t$. A sound response restricts $V_t$ to the classes compatible with that response. Call such a response informative when $V_{t+1}\subsetneq V_t$. A probe policy is eventually separating on $V_t$ when, whenever more than one class remains, it obtains an informative response after finitely many further steps. This permits uninformative observations between eliminations and is therefore weaker than requiring every probe to separate.

Theorem 17.1 Finite conservative doctrine stabilization

Suppose that:

the initial doctrinal version space $V_0$ contains $N{\lt}\infty $ query-equivalence classes;
a realizable target class $v_\star \in V_0$ generates sound responses and is never eliminated;
the probe policy is eventually separating; and
every assimilation or accommodation comparison is conservative on the previously settled query family, and settled query families grow monotonically.

Then after at most $N-1$ informative responses there is a finite time $\tau $ for which

\[ V_t=\{ v_\star \} \qquad (t\geq \tau ). \]

Consequently the execution behaviorally stabilizes on every admissible query answered by the target class, while every previously settled answer persists through all subsequent doctrine changes.

Proof ▼

Soundness retains $v_\star $ in every $V_t$. Whenever $V_t$ has more than one class, eventual separation supplies, after finitely many steps, an informative response. That response strictly decreases the positive integer $|V_t|$ without deleting $v_\star $. Hence at most $N-1$ informative responses leave the singleton $\{ v_\star \} $; eventual separation makes the time of the last such response finite. Later sound evidence cannot remove the target or restore an eliminated class, so the singleton persists.

All representatives of $v_\star $ give equivalent answers to every query in $\mathcal Q$, which proves behavioral stabilization. Each update is conservative on the already settled queries. Closure of conservativity under reindexing and composition, as in Proposition 7.3, therefore preserves those answers through every finite composite of later assimilations and accommodations.

The theorem is a finite categorical identification-in-the-limit result. Its conclusion is stronger than ordinary finite UOCL identification in one fiber: an informative response may eliminate entire doctrines, and the execution may cross fibers before stabilizing. Yet it deliberately does not claim that the displayed base path

\[ b_0\longrightarrow b_1\longrightarrow \cdots , \qquad \widehat M_t\in \mathcal E_{b_t}, \]

becomes literally constant.

Corollary 17.2 When the doctrine itself stabilizes

Under the hypotheses of Theorem 17.1, suppose in addition that the target class has a unique minimal representing doctrine $b_\star $, up to equivalence in $\mathcal B$, and that after the version space becomes a singleton the selection rule chooses this minimal representative and changes doctrine only in response to a separating defect. Then $b_t\simeq b_\star $ for all sufficiently large $t$.

Proof ▼

After time $\tau $, only the target class remains. The selection rule then chooses its unique minimal representative. No later sound response separates that representative from the target class, so the stipulated trigger permits no further doctrinal change.

Without minimality, different doctrines may be Morita-equivalent, present equivalent model categories, or merely agree on all admitted probes. Without the selection condition, a learner may wander forever among such representatives while answering every query correctly. Thus “the true doctrine” is identifiable only when the presentation and probes expose a unique minimal base object; the theorem itself guarantees exactly the stronger defensible invariant—stabilization of answers together with conservative persistence of settled knowledge.