*Previously asked and bountied at MSE:*

Let $\mathsf{SOL_{abs}}$ be the "forcing-absolute" fragment of second-order logic - that is, the set of second-order formulas $\varphi$ such that for every (set) forcing $\mathbb{P}$ and every (set-sized) structure $\mathfrak{A}$ (in the ground model $V$) we have $$\mathfrak{A}\models\varphi\quad\iff\quad\Vdash_\mathbb{P}(\mathfrak{A}\models\varphi).$$ Note that this is in fact definable since the second-order theory of a structure in $V_\kappa$ is calculated, uniformly, in $V_{\kappa+1}$; by contrast, the set of forcing-absolute second-order properties of *the universe* is not so nice (to put it mildly).

Under a "mild" large cardinal assumption, $\mathsf{SOL_{abs}}$ has a **weak downward Lowenheim-Skolem property for countable languages**, namely every satisfiable countable $\mathsf{SOL_{abs}}$-theory $T$ has a countable model. This is just a consequence of the appropriate amount of large-cardinal-given absoluteness applied to the $\Sigma^1_{\omega+1}$ sentence "$T$ has a countable model," with $L(\mathbb{R})$-absoluteness being more than enough.

However, I don't see how to get the full downward Lowenheim-Skolem property for countable languages:

Does $\mathsf{ZFC}$ + [large cardinals] prove that every structure in a countable language has a countable $\mathsf{SOL_{abs}}$-elementary substructure?

(To clarify since there is a stronger notion of second-order elementary equivalence in use as well, I mean the "weak" version of elementarity here: $\mathfrak{A}\preccurlyeq_{\mathsf{SOL_{abs}}}\mathfrak{B}$ iff for every $\mathsf{SOL_{abs}}$-formula $\varphi(x_1,...,x_n)$ with only **object** variables we have $\varphi^\mathfrak{A}=\varphi^\mathfrak{B}\cap\mathfrak{A}^n$.)

The problem is that for a given structure $\mathfrak{A}$, the property "is a countable substructure of $\mathfrak{A}$" might be too wild for our large cardinal assumption to get useful purchase.