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 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, 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, and that fragment might actually be more natural here).