If we have a class like $L$ but allowing a set number of unbounded quantifiers, is it strict superset of $L$?

Question

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$.

Answer 1

Every $L^{\Sigma_n}$, for $n\geq 2$ will be the same as HOD, the class of hereditarily ordinal-definable sets.

This is a consequence of the Myhill-Scott theorem, which asserts that if you form the constructible universe using second-order logic (which means you allow quantifiers over subsets of $X$ only in your set-up), then you get exactly the inner model HOD.

In your set-up, if $n\geq 2$, then you will get access to the power set $P(X)$, and this will allow you to mimic the second-order logic (over $X$) use in the Myhill-Scott theorem. So HOD will be included in your model. But you do not leave HOD, since inductively the sets you add will all be ordinal definable. So your class is exactly HOD.

Various generalizations of the question are well-studied. For example, this previous MO answer shows that if you form the constructible hierarchy using infinitary formulas, then you get all of $V$.

Meanwhile, if you form the constructible hierarchy adding the algebraic classes, rather than only the definable classes, you get the class Imp, introduced in my article: Hamkins, Joel David; Leahy, Cole, Algebraicity and implicit definability in set theory, Notre Dame J. Formal Logic 57, No. 3, 431-439 (2016). doi:10.1215/00294527-3542326, ZBL1436.03264. This class was asked about in this MO question. Further work in: Groszek, Marcia J.; Hamkins, Joel David, The implicitly constructible universe, ZBL07149973.

Juliette Kennedy, Menachem Magidor, and Jouko Väänänen have investigated many other generalizations of the question with various other logics, such as allowing the quantifier "uncountably many" and so on.