Given a (set-sized) logic $\mathcal{L}$, let $\mathcal{L}'$ be gotten from $\mathcal{L}$ by adding the ability to quantify over $\mathcal{L}$-definable relations. (I'm being a bit vague here, since e.g. we would want to be able to say "Every $\{+\}$-definable set is periodic" in $(\mathbb{N};+,\times)$ for monotonicity reasons; see this earlier post of mine) for the detailed definition.) For $\alpha$ an ordinal, let $\mathcal{L}^{(\alpha)}$ be gotten by iterating the $'$-operation along $\alpha$, taking unions at limit ordinals. Note that $\mathcal{L}^{(\alpha)}$ can quantify over $\mathcal{L}^{(\beta)}$-definable relations for each fixed $\beta<\alpha$. A priori we have that the class-sized logic $\mathcal{L}^{(\infty)}=\bigcup_{\alpha\in\mathsf{Ord}}\mathcal{L}^{(\alpha)}$ is contained in the closure of $\mathcal{L}$ under all set-sized Boolean combinations, call this $\mathbb{I}_{\infty,\omega}(\mathcal{L})$.
My question is the following:
Is it consistent with $\mathsf{ZFC}$ (in particular, does it follow from large cardinals) that $\mathcal{L}^{(\infty)}<\mathbb{I}_{\infty,\omega}(\mathcal{L})$ for every set-sized logic $\mathcal{L}$ extending first-order logic?
I know that this does hold for a wide variety of logics. For example:
If $\mathcal{L}$ has a downward Lowenheim-Skolem number (= some $\kappa$ such that for all finite languages $\Sigma$, every $\Sigma$-structure has an $\mathcal{L}$-elementary substructure of size $\le\kappa$), then the result holds.
If $\mathcal{L}$ is at least as strong as $\mathsf{SOL}$, then the result holds.
However, this still leaves a large gap. The only "big-hammer" theorem I can think of that feels relevant is Makowsky's result that $\mathsf{VP}\implies$ every logic has a strong compactness cardinal, but I don't really see how to apply that here.
Here are sketches of the proofs of the above results.
The first is basically just a lift of the proof that "gap ordinals" exist in the $L$-hierarchy. Let $\kappa$ be the downward Lowenheim-Skolem number of $\mathcal{L}$ (and assume $\mathcal{L}$ has $<\kappa$-many formulas in a finite language), and consider the $\mathcal{L}$-analogue of the $L$-hierarchy-with-urelements built on the structure $(\kappa;<)$. Applying dLS to an appropriate level of this hierarchy, we get that there is some ordinal $\lambda<\kappa^+$ such that no new subsets of $\kappa$ get added at stage $\lambda+1$. This gives that every $\mathcal{L}^{(\infty)}$-definable subset of $\kappa$ appears in this hierarchy by level $\lambda$, but this means we miss lots of subsets of $\kappa$ (and every subset of $\kappa$ is $\mathbb{I}_{\infty,\omega}(\mathsf{FOL})$-definable).
For the second fact, the point is that on pure sets if $\mathcal{L}\ge\mathsf{SOL}$ then $\mathcal{L}\equiv\mathcal{L}'$ and so $\mathcal{L}\equiv\mathcal{L}^{(\infty)}$. By the weakest pigeonhole principle, then, there are nonisomorphic $\mathcal{L}^{(\infty)}$-equivalent pure sets. On the other hand, every pure set is characterized up to isomorphism by an $\mathbb{I}_{\infty,\omega}(\mathsf{SOL})$-sentence.
- The first sentence of this argument uses a subtlety of the definition of $\mathcal{L}'$: for example, we can't in $\mathsf{SOL}'$ say something like "For every set $X$, every $X$-definable-in-$\mathsf{SOL}$ set has [...]." This is a side-effect of setting up the $-'$-construction in the framework of standard abstract model theory, where we don't really have a logic-independent notion of "free second-order variable." Arguably this is not the right notion of "jump of a logic" to work with when considering logics closed under second-order quantifiers, but for now I am focusing on it nonetheless.
