5.3 From products to finite limits

Finite products express total, many-input operations. Some theories require more discriminating domains of definition. A finite-limit theory is a small category \(\mathbb T_{\mathrm{fl}}\) with finite limits. Its models in a finitely complete category \(\mathcal C\) are finite-limit-preserving functors

A finite-limit sketch presents such a theory by specifying only the equations and finite-limit cones needed as generators.

The extra expressiveness is important. Internal categories, for instance, have an object of arrows, an object of objects, source and target maps, and a composition defined on the pullback of composable pairs. The pullback is not merely a product: it selects pairs whose target and source match. Finite-limit logic can therefore describe essentially algebraic structures with partially defined operations whose domains are themselves specified structurally.

Passing from product preservation to finite-limit preservation is not a cosmetic strengthening. It changes which models count as valid and which countermodels can refute a candidate theory. A creative system must declare the preservation doctrine it intends; otherwise it can silently move between different notions of model.