How do we qualify the successor function and other maps of large classes

functionsset-theory

When I took a course in set theory last year, I remember being rather intrigued by the definition of the successor function/operation
$ S(x) = x \cup \lbrace x \rbrace $
, given that it is not a "function" or "map" in the usual sense of those words, in that the domain and codomain are not themselves [small] sets.

In the case of this particularly simple operation, we can view
$ S(x) = x \cup \lbrace x \rbrace $
as nothing more than a bit of notation, where $S$ does not represent a mathematical object. But what about more interesting maps between large/universal sets or categories? For example, the cartesian product $\prod$ as a unary operator
$ \prod \mathcal{F} = {\prod_{x \in \mathcal{F}} x } $
and a morphism of $\mathsf{Set}$.

I was poking around the Wikipedia pages on primitive recursive functions and of course the ZF axioms, where in the axiom of infinity we see that $S(x)$ is used as an "abbreviation" as I proposed above; and that didn't get me very far. Any relevant info or resources on category theory would be appreciated.

Best Answer

You're describing the concept of extension by definitions. If your underlying theory (say ZFC) is strong enough to prove that your proposed function is in fact well defined (in other words, if it can prove $\forall x_1 \ldots x_n \exists ! y \phi (y, x_1 \ldots x_n)$, where $\phi$ is the formula defining your proposed function), then you can extend the language by an additional function symbol $f$ defined by $\phi$.

This extension will always be conservative. Any statement that's true in the base language remains true in the extended language and you can always find a statement in the base language that is provably equivalent to a statement in the extended language.