*Previously asked and bountied without response at MSE.*

This question is a companion to this one, about a tame(?) fragment of second-order logic with the standard semantics, $\mathsf{SOL}$, motivated by the Tarski-Vaught test. The question is:

Working in $\mathsf{ZFC}$ + "There is an extendible cardinal," can the strong compactness number$^1$ of $\mathsf{SOL}_{TV}$ be strictly less than the smallest extendible cardinal?

To keep things self-contained, here is the relevant definition. First, given structures $\mathfrak{A},\mathfrak{B}$ in the same signature $\Sigma$, say $\mathfrak{A}\trianglelefteq\mathfrak{B}$ iff $\mathfrak{A}\subseteq\mathfrak{B}$ and $\varphi^\mathfrak{B}\not=\emptyset \implies\varphi^\mathfrak{B}\cap \mathfrak{A}^{arity(\varphi)}\not=\emptyset$ for every second-order $\Sigma$-formula $\varphi$ with parameters from $\mathfrak{A}$. We then let $\mathsf{SOL}_{TV}$ be the set of $\mathsf{SOL}$-formulas which are absolute with respect to $\trianglelefteq$, that is the set of $\varphi\in\mathsf{SOL}$ such that whenever $\mathfrak{A}\trianglelefteq\mathfrak{B}$ are structures in the signature of $\varphi$ we have $\varphi^\mathfrak{A}=\varphi^\mathfrak{B}\cap\mathfrak{A}^{arity(\varphi)}.$

Note that despite having the downward Lowenheim-Skolem property, $\mathsf{SOL}_{TV}$ is much stronger than first-order logic. For example, well-foundedness is $\mathsf{SOL}_{TV}$-characterizable$^2$; 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 question above seems like it might be approachable.

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

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