ora-0049
3.5 A constrained positive regime
Exact finite identification becomes possible when the target category is finite, the learner has a known finite inventory of objects and arrows, and it may query domain, codomain, identity, composition, and equality.
Under the preceding assumptions, a fair active categorical informant identifies the target category after finitely many queries, up to an isomorphism preserving the declared inventory.
There are finitely many structure-table entries: identity assignments, composable pairs, their composites, and equalities among the named arrows. Fairness reveals every entry after finite time. The completed tables determine a category on the inventory, and soundness makes it isomorphic to the target.
This proposition is intentionally modest. Removing the known inventory, allowing finite presentations with undecidable word problems, or restricting the learner to positive text reopens the identification problem.
The same proof admits a structured refinement. Suppose the finite inventory also names the realization of every sort, arrow, diagram, and designated cone in a finite core sketch. Querying the structure tables and the interpretation tables identifies not only \(\mathcal C_\star \) but the pair \((\mathcal C_\star ,M_\star )\), up to a core-preserving isomorphism. The extra conclusion requires the extra tables: identifying the ambient category alone does not identify which objects realize agents, magnitudes, or social contexts.