4.4.1. Set-theoretic intuition for Bénabou's definability [002Q]
To motivate Bénabou’s general notion of definability, we will first develop an alternative perspective on definability for classes of sets in terms of families of sets.
Let $\mathfrak{C}\subseteq\mathscr{M}$ be a class of sets; there exists a class $\bar{\mathfrak{C}}$ of families of sets that contains $\prn{S\Sub{i}}\Sub{i\in I}$ exactly when each $S\Sub{i}$ lies in $\mathfrak{C}$. We will refer to $\bar{\mathfrak{C}}$ as the closure under base change of $\mathfrak{C}$, a name motivated by the fact that when $\prn{S\Sub{i}}\Sub{i\in I}$ lies in $\bar{\mathfrak{C}}$, then for any $u:J\to I$, the base change $\prn{S\Sub{uj}}\Sub{j\in J}$ also lies in $\bar{\mathfrak{C}}$.
Conversely to Construction 4.4.1·a [002M] we may take a class of families of sets $\mathfrak{F}$ to the the class of sets $\mathfrak{F}\Sub{1}\subseteq{\mathscr{M}}$ spanned by sets $S$ such that the singleton family $\brc{S}$ lies in $\mathfrak{C}$.
A class of families of sets $\mathfrak{F}$ is said to be definable when it is stable and moreover, for any family of sets $\prn{S\Sub{i}}\Sub{i\in I}$, there exists a subset $J\subseteq I$ such that the base change $\prn{S\Sub{j}}\Sub{j\in J}$ lies in $\mathfrak{F}$, and moreover, such that $u:K\to I$ factors through $J\subseteq I$ whenever the base change $\prn{S\Sub{uk}}\Sub{k\in K}$ lies in $\mathfrak{F}$.
In other words, a stable class of families of sets is definable when any family of sets can be restricted to a “biggest” subfamily that lies in the class.
Let $\mathfrak{C}\subseteq\mathscr{M}$ be a class of sets; then $\bar{\mathfrak{C}}$ is a definable class of families of sets if and only if $\mathfrak{C}$ is a definable class of sets.
Proof. Suppose that $\mathfrak{C}$ is a definable class of sets. To check that $\bar{\mathfrak{C}}$ is a definable class of families of sets, we fix a family $\prn{S\Sub{i}}\Sub{i\in I}$ not necessarily lying in $\bar{\mathfrak{C}}$. Because $\mathfrak{C}$ is definable, the intersection $\mathfrak{C}\cap \bigcup\Sub{i\in I}S\Sub{i}$ is represented by a set $U$. We therefore take the subset $J = \brc{i \in I\mid S_i\in U}\subseteq I$, and verify that the base change $\prn{S\Sub{j}}\Sub{j\in J}$ is the largest approximation of $\prn{S\Sub{i}}\Sub{i\in I}$ by a family lying in $\bar{\mathfrak{C}}$.
Conversely suppose that $\bar{\mathfrak{C}}$ is a definable class of families of sets. To see that $\mathfrak{C}$ is definable, we fix a class $\mathfrak{U}$ represented by a set $U\in\mathscr{M}$ to check that $\mathfrak{C}\cap\mathfrak{U}$ is representable. We consider the family of sets $\prn{u}\Sub{u\in U}$; because $\bar{\mathfrak{C}}$ is definable, there is a largest subset $V\subseteq U$ such that the change of base $\prn{v}\Sub{v\in V}$ lies in $\bar{\mathfrak{C}}$, i.e. such that each $v\in V$ lies in $\mathfrak{C}$. Therefore $\mathfrak{C}\cap\mathfrak{U}$ is represented by the set $V$. ∎