9.2 Declaration interventions

At the level of presentations, a common case is a sketch map

Several forms of theory surgery should be distinguished.

1. Definitional extension adds names or operations explicitly definable from the old theory and is conservative under a stated definitional criterion.

2. Constraint extension adds an equation or universal property, excluding some old models.

3. Ontology extension adds a genuinely new sort, operation, latent object, or interface with several possible realizations.

4. Resolution change splits a type, passes to a quotient, or changes which distinctions count as observable.

5. Doctrine change alters the class of limits, colimits, exponentials, enrichment, or differential structure that models must preserve.

These operations have different epistemic force. Merely naming a definable term can improve reasoning without enlarging model content, but unique expansion by itself is only evidence for definitionality, not a proof of definitional or Morita equivalence. Adding an equation makes the theory more restrictive. A latent object may give some old models several inequivalent expansions and others none. A doctrine change can alter the kind of semantics available altogether.