Compactness number for a fragment of second-order logic 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.
 A: I think that if you have a logic $\mathcal{L}$ which has downward Lowenheim-Skolem (for theories of arbitrary cardinality, i.e. if $T$ has cardinality $\lambda$ and $N$ is a model $A$ of size $\theta\geq\lambda$, and $\lambda\leq\gamma\leq\theta$, then we can find a sub-model of size $\gamma$ which is elementary in $A$ (w.r.t. the relevant formulas of the logic)), then its strong compactness number is $\leq$ the least supercompact $\kappa$.
For suppose $T$ is a theory in $\mathcal{L}$ such that all subsets of $T$ of size ${<\kappa}$ have a model. Let $\lambda$ be the cardinality of $T$; we consider $T\subseteq\lambda$. Let $j:V\to M$ with $\mathrm{crit}(j)=\kappa$ and $\mathcal{P}(\lambda)\subseteq M$ and $j\upharpoonright\lambda\in M$. Then $M$ thinks that every sub-theory of $j(T)$ of size $<j(\kappa)$ has a model. But we have $T\in M$ and $T\subseteq\lambda$, and note that $T$ is equivalent to $j``T\in M$,
and this has size $\lambda<j(\kappa)$ in $M$. So $T$ has a model $B$ in $M$. But by Lowenheim-Skolem, then it has a model of size $\lambda$ in $M$. Since $\mathcal{P}(\lambda)\subseteq M$, this is truly a model in $V$.
Edit 4 (previous edits done over): Now regarding lower bounds (and cf. Noah's comments below)...
Say that a (possibly beyond 1st order) logic (I'm not sure of what the formal definition of "logic" is here, but it doesn't really matter; I only use it in a limited sense below which is clear enough) is $\kappa$-compact iff whenever $T$ is a set-sized theory in that logic and all subtheories of size ${<\kappa}$ have a model, then $T$ also has a model.
Now consider the logic $\mathcal{L}$ in the (first order) language of set theory, where we have available a proper class of constant symbols, and an extra predicate symbol (which can be taken to code multiple predicates/functions below),
together with the second-order statement ``I am wellfounded''. (Remark: I mistakenly said  "one" constant symbol in an earlier version; but I used set-many. Actually for the purposes below we can restrict the number of constants available to something like the cardinality of $V_{\kappa+2}$, where $\kappa$ is the cardinal in question.)
Claim: Let $\kappa$ be a cardinal and suppose that $\mathcal{L}$ as above is $\kappa$-compact. Then there is a measurable cardinal $\leq\kappa$.
Proof: First suppose that $\kappa$ is inaccessible.
Consider the $\mathcal{L}$-theory $T$ which includes the full first order theory of $V_{\kappa+1}$ in parameters, the formulas “$\alpha < \dot{\mu} < \kappa$”, for each $\alpha < \kappa$, where $\dot{\mu}$ is a new constant, and the (2nd order) formula “I am wellfounded”. If $M$ is a (wellfounded) model of $T$, note that there is an elementary $j:V_{\kappa+1}\to M$, the critical point $\mathrm{crit}(j)$ of $j$ exists, and is a measurable cardinal $\leq\kappa$. So we just need to see the small subtheories have models, but this follows easily from the inaccessibility of $\kappa$ (consider elementary substructures of $V_{\kappa+1}$).
Now suppose $\kappa$ is singular.
Let $f:\eta\to\kappa$ be cofinal, where $\eta<\kappa$. Consider the theory $T$ consisting of the first order theory in parameters of $V_\kappa$, and using function symbols $\dot{f},\dot{g}$, the statement "$\dot{f}:\eta\to\mathrm{Ord}$ is cofinal", the equations "$\dot{f}(\alpha)=\beta$" for each $\alpha,\beta$ such that $f(\alpha)=\beta$, and the statement "$\dot{g}$ is a surjection from some ordinal onto $\mathrm{Ord}$", and (2nd order) "I am wellfounded". Then for each $\theta<\kappa$, each fragment $\bar{T}$ of size $\theta$ is satisfiable, since we may assume $\eta<\theta$, and we can find an elementary substructure of $(X,f\cap X)\preceq(V_\kappa,f)$ of cardinality $\theta$, with $\theta+1\subseteq X$, and then the transitive collapse $(M,\bar{f},g)$ is a model, where we take $g:\theta\to\mathrm{Ord}^M$ a surjection. So we get a wellfounded model $(M,f',g')$ of the full theory. Let $j:V_\kappa\to M$ be the resulting elementary embedding. Note that $\mathrm{crit}(j)<\kappa$, because otherwise $f'=f$, so by cofinality, $\kappa=\mathrm{Ord}^M$, so $M=V_\kappa$, so $g':\gamma\to\kappa$ is a surjection for some $\gamma<\kappa$, contradiction. But then $\mathrm{crit}(j)<\kappa$ is measurable.
Finally suppose that $\gamma<\kappa\leq 2^\gamma$. Then consider the theory consisting of the first order theory in parameters of $\mathcal{H}_{(2^\gamma)^+}$, "I am wellfounded", and the statement "$\dot{f}:\mathcal{P}(\gamma)\to\mathrm{Ord}$ is surjective". Any sub-theory of size $<\kappa$ is satisfiable (in fact, any sub-theory of size $\leq 2^\gamma$ is satisfiable), so we have a model, and note it gives a measurable $\leq\gamma$.
(This leaves $\omega$, but it's easy to see this is impossible; also cf. Noah's comments in the question and below.)
