The definition of $L$ only permits bounded quantifiers. If we allow a certain number of unbounded quantifiers, does this result in a strict superset of $L$? For example:

$$ \operatorname{Def}^{\Sigma_3}(X) = \{ \{ y \mid \text{ $y \in X$ and $\exists x_1 \forall x_2 \exists x_3. (\operatorname{TC}(\{X, x_1, x_2, x_3\}), \in) \models \phi(y,X,x_1,x_2,x_3,z_1,\dots,z_n)$} \} \\ \mid \text{$\phi$ is a first-order formula with only bounded quantifiers and $z_1,\dots,z_n \in X$}\} $$

We define $L^{\Sigma_3}_\alpha$ as $\bigcup_{\beta<\alpha} \operatorname{Def}^{\Sigma_3}(L^{\Sigma_3}_\beta)$. The class $L^{\Sigma_3}$ is then defined as $\bigcup_{\alpha \in \mathbf{Ord}} L^{\Sigma_3}_\alpha$. (This is in analogue to this definition.) $L^{\Sigma_n}$ for other natural numbers $n$ is defined similarly.

The question is, does $L^{\Sigma_n} = L$, or is it a strict superset of $L$. (Note that $L^{\Sigma_n} = L$ is a separate statement for each $n$.)

$L^{\Sigma_n}$ will be an inner model for essentially the same reason that $L$ is. It may be bigger than $L$ though, since it can refer to higher concepts in the Lévy hierarchy.

It is at least consistent with ZFC that they are the same set, since $L \subseteq L^{\Sigma_n} \subseteq V$ and $V = L$ is consistent with ZFC. $OD = L$ (all ordinal definable sets are constructible) also implies $L^{\Sigma_n} = L$, since $L \subseteq L^{\Sigma_n} \subseteq OD$.

allformulas. (Or in your definition of $\mathsf{Def}^{\Sigma_3}(X)$ are $x_1,x_2,x_3$ not required to be from $X$?) $\endgroup$ – Noah Schweber Nov 5 '20 at 3:56