This question is about a tame(?) fragment of second-order logic with the standard semantics $\mathsf{SOL}$, motivated by the Tarski-Vaught test. The general setup is as follows. Given structures $\mathfrak{A},\mathfrak{B}$ and a logic $\mathcal{L}$, write $\mathfrak{A}\trianglelefteq_{\mathcal{L}}\mathfrak{B}$ iff $\mathfrak{A}$ is a substructure of $\mathfrak{B}$ and for every $\mathcal{L}$-formula $\varphi$ with parameters from $\mathfrak{A}$ we have $$\varphi^\mathfrak{B}\not=\emptyset\implies \varphi^\mathfrak{B}\cap\mathfrak{A}\not=\emptyset.$$
Tarski-Vaught says that $\trianglelefteq_\mathsf{FOL}$ coincides with $\preccurlyeq_{\mathsf{FOL}}$, but in general this breaks down: note that whenever $\trianglelefteq_\mathcal{L}$ and $\preccurlyeq_\mathcal{L}$ coincide we get a downward Lowenheim-Skolem theorem for $\mathcal{L}$ by counting formulas. However, we can ask how much elementarity $\trianglelefteq_\mathcal{L}$ guarantees. Specifically, say that the TV-fragment of $\mathcal{L}$ is the set $\mathcal{L}_{TV}$ of $\mathcal{L}$-formulas $\varphi$ for which we have $$\mathfrak{A}\trianglelefteq_\mathcal{L}\mathfrak{B}\implies\varphi^\mathfrak{A}=\varphi^\mathfrak{B}\cap\mathfrak{A}.$$
I'm interested in the expressive power of $\mathsf{SOL}_{TV}$ as a logic in its own right. Despite having the downward Lowenheim-Skolem property, it is much stronger than first-order logic. For example, well-foundedness is $\mathsf{SOL}_{TV}$-characterizable$^1$; this means that there is an $\mathsf{SOL}_{TV}$-sentence pinning down $\mathbb{N}$ up to isomorphism, which in turn implies that the $\mathsf{SOL}_{TV}$-definable relations on $\mathbb{N}$ are exactly the $\mathsf{SOL}$-definable ones. Beyond this, not much is clear to me. The following seems like a good next point to tackle:
Working in $\mathsf{ZFC}$ + "There is an extendible cardinal," can the strong compactness number$^2$ of $\mathsf{SOL}_{TV}$ be strictly less than the smallest extendible cardinal?
At present I don't see anything preventing the strong compactness number of $\mathsf{SOL}_{TV}$ from being extremely small - although of course since $\mathsf{SOL}_{TV}$ has the downward Lowenheim-Skolem property it must be uncountable by Lindstrom's Theorem.
$^1$Since well-foundedness is preserved downwards, it's enough to show (working in a language with a distinguished binary relation symbol $<$) that if $\mathfrak{A}\trianglelefteq_{\mathsf{SOL}}\mathfrak{B}$ and $<^\mathfrak{B}$ is illfounded then $<^\mathfrak{A}=<^\mathfrak{B}\cap\mathfrak{A}$ is illfounded. Consider first the formula $\psi(x)\equiv$ "The initial segment of $<$ below $x$ is ill-founded." We have $\psi^\mathfrak{B}\not=\emptyset$, so there must be some $a\in\mathfrak{A}$ which is in the ill-founded part of $<^\mathfrak{B}$. But now for each $u\in\mathfrak{A}$ in the ill-founded part of $<^\mathfrak{B}$, consider the formula $\theta_u(y)\equiv$ "$y<u$ and $y$ is in the ill-founded part of $<$." Applying $\triangleleft_{\mathsf{SOL}}$-ness, we get that the set of elements of $\mathfrak{A}$ which are in the ill-founded part of $\mathfrak{B}$ has no $<^\mathfrak{B}$-minimal element, which (together with its above-established nonemptiness) implies that $<^\mathfrak{A}$ is ill-founded as desired.
$^2$The strong compactness number of a logic $\mathcal{L}$, if it exists at all, is the least cardinal $\kappa$ such that every unsatisfiable $\mathcal{L}$-theory has an unsatisfiable subtheory of cardinality $<\kappa$. Large cardinals imply the existence of strong compactness numbers; in particular, second-order logic has a strong compactness number iff there is an extendible cardinal, in which case its strong compactness number is the least extendible. As an amusing aside, Vopenka's Principle turns out to be equivalent to the existence of strong compactness numbers for all logics in a precise sense.
