Consider the sublogic $\mathsf{Stv}$ of full second-order logic $\mathsf{SOL}$ consisting of all formulas $\varphi$ such that, whenever $\mathfrak{A}$ is a substructure of $\mathfrak{B}$ such that $\varphi^\mathfrak{B}\not=\emptyset$, we get $\varphi^\mathfrak{B}\cap\mathfrak{A}^{arity(\varphi)}\not=\emptyset$. (See [this earlier question of mine](https://mathoverflow.net/questions/387138/compactness-number-for-a-fragment-of-second-order-logic) for more detail; there I called this fragment "$\mathsf{SOL}_{TV}$.") $\mathsf{Stv}$ is significantly stronger than first-order logic (for example, $\mathsf{Stv}$ can define well-foundedness), but at the same time it has the full downward Lowenheim-Skolem property and so is  also much weaker than second-order logic.

I'm curious about an analogue of $L$ built using $\mathsf{Stv}$ instead of first-order logic:

 - $X_\alpha=L_\alpha$ for $\alpha\le\omega$.

 - $X_{\omega+1}=L_{\omega+1}\cup\{s\}$, where $s$ is the set of (codes for) second-order formulas in finite languages which are elements of $\mathsf{Stv}$.

 - For $\alpha>\omega+1$, we let $X_{\alpha+1}$ be the set of subsets of $X_\alpha$ which are first-order definable in the expansion of $X_\alpha$ by a binary relation symbol saying which $\mathsf{Stv}$-formulas are true in which finite-language structures in $X_\alpha$. *(Hopefully it's clear what's going on here - the point is that $X_{\alpha+1}$ knows, for example, the $\mathsf{Stv}$-theory of $\mathcal{M}$ for each finite-language structure $\mathcal{M}\in X_\alpha$. I will of course add more detail if desired.)*

 - For $\lambda$ limit, we set $X_\lambda=\bigcup_{\alpha<\lambda}X_\alpha$.

The $L$-analogue I'm interested in is the class $X:=\bigcup_{\alpha\in\mathsf{Ord}}X_\alpha$. Since $\mathsf{Stv}$ satisfies the full downward Lowenheim-Skolem property, the $X$-hierarchy satisfies a version of condensation (basically, we have to look at the $X_\alpha$s equipped with the appropriate fragments of the $\models_{\mathsf{Stv}}$-relation) and so in particular $X\models\mathsf{GCH}$. At the same time, at least descriptive set theoretically $X$ is quite large (it has all the projective reals).

The obvious way to show that $X\models$ "There are no measurable cardinals" would be to show that, if $j:V\rightarrow M$ is the usual ultrapower embedding gotten from a measurable cardinal, then $j$ in fact respects $\mathsf{Stv}$ so that the restriction $j\upharpoonright X: X\rightarrow X$ would also be (first-order-)elementary. However, this isn't obvious to me given that measurables *can* live in $HOD$, the relevance being that Scott/Myhill showed that we get $HOD$ if we do anything like the above with full $\mathsf{SOL}$ (see the introduction of Kennedy/Magidor/Vaanaanen's [*Inner models for extended logics 1*](http://www.math.helsinki.fi/logic/people/jouko.vaananen/kmv12.pdf), and note that unless I'm missing something this paper and its follow-up don't solve the question here).

More generally, I'm interested in variations of the $L$-hierarchy built using any strong fragment of $\mathsf{SOL}$ with the downward Lowenheim-Skolem property (for example, Farmer S. proved that the [absolute fragment can have dLS](https://mathoverflow.net/a/410213/8133), and that fragment might actually be more natural here).