5.6 The creative target package

Chapter 2’s status-bearing extension dossier can therefore be refined. The following tuple is the structural extension subrecord of that dossier, not a replacement for the status-bearing dossier \(\Xi \):

where:

Presentation \(\mathbb S^+\).

The new sorts, generators, equations, cones, cocones, symmetries, or covers.

Doctrine \(\mathfrak D^+\).

The proposed preservation contract: finite products, finite limits, symmetric tensor, geometric structure, or another explicitly defined doctrine.

Model semantics.

For every registered target category, the category of structure-preserving model functors.

Theory map \(\iota :\mathbb S\to \mathbb S^+\).

The relation between the old and proposed presentations.

Doctrine comparison \(\delta _{\mathfrak D}\).

A declaration of whether the old doctrine is retained, strengthened, weakened, or replaced, together with the compatibility needed to compare old and new models.

Restriction \(\iota ^*\).

When the presentation and doctrine comparisons make it well-defined, the functor sending an expanded model back to its old-theory reduct.

Here the dash in \(\operatorname {Mod}_{\mathfrak D^+}(\mathbb S^+,-)\) denotes the registered family of target categories for which the doctrine and its change-of-target semantics have actually been defined; it does not assert functoriality in every category. To recover the complete Chapter 2 dossier, take the presentation component of \(\Upsilon \) to be \(J=\iota \), let \(\mathbb S^+\) denote the presented theory specified by \(\mathbb S^+\), \(\mathfrak D^+\), and its registered model semantics, and let \(D^+\) denote the current realization of that theory. Record any chosen model transport in \(\tau \), and retain \(\omega \), \(\gamma \), \(\Pi \), and \(\sigma \) with their earlier meanings. Models, countermodels, proofs, simulations, and other admission evidence belong to that provenance-bearing dossier. They are not proposer-controlled fields of \(\mathfrak T^+_{\mathrm{str}}\).

When the doctrine comparison permits it, the restriction functor

is especially informative. Its fiber over an old model records the model’s possible expansions. An essentially unique expansion is evidence compatible with a definitional extension, but does not prove definitionality by itself; that stronger claim requires the registered theory-equivalence criterion. Several inequivalent expansions expose genuinely new choices. An empty fiber means that the new theory excludes the old model and owes an explanation.

A concrete restriction-fiber example.

Return to the monoid theory above and extend its presentation by an inverse operation \(i:X\to X\), together with the two equations saying that multiplying an element by its inverse on either side yields the unit. The expanded presentation is the theory of groups, and restriction forgets the inverse:

For a given monoid \(M\), the fiber of \(\iota ^*\) is empty when some element of \(M\) is not invertible. When every element is invertible, its inverse is unique, so the compatible group expansion is essentially unique. The example makes two points visible at once. Adding a generator need not create an arbitrary new degree of freedom, because equations can determine it uniquely; yet the extension is not definitional over all monoids, because it excludes models that do not satisfy the new existence requirement. A creative system must therefore report both the new syntax and what happens to old models.

Presentation changes also require quotienting. Two sketches can present equivalent model theories. Renaming a generator, adding a definable operation, or changing to a more convenient presentation should not automatically count as transformational creativity. The appropriate comparison may be an equivalence of model categories, a Morita-style equivalence, or a stronger doctrine-specific invariant. Which comparison is required must be registered before evaluation.