Is $\mathbb{L}$ literally the smallest model of $\sf ZF(C)$ ? (In $\sf NBG$)

Question

I was reading somewhere that $\mathbb{L}$ was "the smallest transitive model of $\sf ZFC$ that contains all the ordinals" (Gödel's constructible universe)

I was wondering if : 1. This was true and 2. This could be made precise in $\sf NBG$ (Von Neumann-Bernays-Gödel set theory)

So my first question is : is it true ?

Then about point 2., I was thinking this : in $\sf NBG$ you can talk about proper classes, and if a transitive model of $\sf ZFC$ contains all the ordinals, it has to be a proper class. So to be able to say that $\mathbb{L}$ is the smallest such, one way would be to use the fact that $\sf NBG$ can talk about proper classes and compare their "size" (inclusion-wise).

In NBG one can define a set of variables, symbols and so on, to, in the end, get a set which we can denote $\mathcal{ZFC}$ which is a set of first order sentences that represent $\sf ZFC$. Then probably one can define the notion $C\models \phi$ for $C$ a class and $\phi$ a first-order sentence (written "inside" $\sf NBG$) that only uses logical symbols, $\simeq$ and $\epsilon$ (denoting $=$ and $\in$). I haven't lingered on the details here, but I assume it can be done in the same way as $\models$ is usually defined in model theory.

Once one has done that one can define $C\models \mathcal{ZFC}$ for $C$ a class, and also "$C$ is transitive" and "$C$ contains all the ordinals" can be defined.

So in $\sf NBG$ my question can be rewritten as : is it true that $\forall C, C\models \mathcal{ZFC}\land C$ is transitive $\land \, C$ contains all the ordinals $\implies \mathbb{L}\subset C$ ? (I abbreviate the conditions on $C$ by $Mod(C)$)

Because otherwise one can define $\mathbb{S} = \{x\mid \forall C, Mod(C)\implies x\in C\}$, and then I wouldn't be surprised if we had $Mod(\mathbb{S})$ (I haven't checked the details but it seems reasonable), and thus $\mathbb{S}$ would be the smallest transitive model of $\sf ZFC$ containing all the ordinals.

So my second question is : would this last construction work, and if so would one have $\mathbb{L}=\mathbb{S}$ ? Has this been done before as an alternative way of defining $\mathbb{L}$ ? If the answer to these is yes, would replacing $\sf ZFC$ by $\sf ZF$ work and if so, could one prove directly ( without explicitly giving a construction of $\mathbb{L}$) that $\mathbb{L}\models AC$ ?

Answer 1

The problem is with $L\models\sf ZFC$. Because if that would be provable from $\sf NBG$, then $\sf NBG$ would prove the consistency of $\sf ZFC$. Since $\mathsf{NBG}$ is a conservative extension, the statement is not provable. And sure enough, truth predicates for proper classes would require impredicative class comprehension.

But what is in fact true, is that $\sf ZF$ already proves that if $\varphi$ defines a transitive class which:

1. Contains all the ordinals,
2. Is closed under Gödel operations,
3. Almost universal,

Then every set satisfying the property of being a member of $L$ is satisfying $\varphi$. Namely, any model of $\sf ZF$ will include $L$. Note that the three properties only imply that for every axiom of $\sf ZF$, its relativization to $\varphi$ is provable, but these proofs are not uniform.