Can the forcing-absolute fragment of SOL have a strong Lowenheim-Skolem property?

Question

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.

Answer 1

Yes, and a proper class of Woodin cardinals suffices. For $n<\omega$ and $X$ a set of ordinals, $M_n(X)$ denotes the minimal iterable proper class model $M$ of ZFC with $n$ Woodin cardinals above $\mathrm{rank}(X)$ and $X\in M$. Because we have a proper class of Woodin cardinals, $M_n(X)$ exists for every set $X$ of ordinals. If $x$ is a real, then for $n$ even, $M_n(x)$ is boldface-$\Sigma^1_{n+2}$-correct, and for $n$ odd, is boldface-$\Sigma^1_{n+1}$-correct. All forcing below is set forcing.

Claim 1: Given a structure $\mathfrak{B}$ and a set $B$ of ordinals coding $\mathfrak{B}$, and given an element $x\in\mathfrak{B}$ and a second order formula $\varphi$, if "$\mathfrak{B}\models\varphi(x)$" is forcing absolute then for all sufficiently large $n<\omega$, $M_n(B)\models$"It is forced by $\mathrm{Coll}(\omega,\mathrm{rank}(\mathfrak{B}))$ that $\mathfrak{B}\models\varphi(x)$".

(Here '"$\mathfrak{B}\models\varphi(x)$" is forcing absolute' just means that the truth value of "$\mathfrak{B}\models\varphi(x)$" is independent of which generic extension of $V$ we are working in, but here $\mathfrak{B}$ and $x$ are fixed.) (Note I'm not saying that the converse of the claim holds.)

Proof: Let $G$ be $\mathrm{Coll}(\omega,\mathrm{rank}(\mathfrak{B}))$-generic over $V$, hence also over $M_n(B)$. Then $V[G]\models$"$\mathfrak{B}\models\varphi(x)$". Since $\mathfrak{B}$ is countable in $V[G]$, this is just a projective statement there, about some reals in $M_n(B)[G]$. But one can show that (with our large cardinal assumption) $M_n(y)$ is not changed by forcing, so $(M_n(B))^V=(M_n(B))^{V[G]}$, and $V[G]\models$"$M_n(B)[G]=M_n(B,G)$", so $M_n(B)[G]$ is at least boldface-$\Sigma^1_{n+1}$-correct in $V[G]$. So for sufficiently large $n$, $M_n(B)[G]\models$"$\mathfrak{B}\models\varphi(x)$", as desired.

Now working in $V$, let $\pi:H\to V_\gamma$ be elementary, with $\gamma$ a sufficiently large ordinal, and $H$ transitive and countable, and $\mathrm{rg}(\pi)$ containing $B,\mathfrak{B}$. The proper class mice $M_n(B)$ are determined by set-sized mice $M_n^\#(B)$, and these are definable from $B$ over $V_\gamma$, so are also in $\mathrm{rg}(\pi)$. Let $\pi(\bar{B},\bar{M}_n^\#(\bar{B}))=(B,M_n^\#(B))$. Then because $\pi$ is elementary, in fact $\bar{M}_n^\#(\bar{B})=M_n^\#(\bar{B})$, i.e. the collapse of $M_n^\#(B)$ is the true $M_n^\#(\bar{B})$.

Claim 2: $\pi\upharpoonright\bar{\mathfrak{B}}:\bar{\mathfrak{B}}\to\mathfrak{B}$ is elementary with respect to forcing absolute second order formulas.

Proof: Suppose $\bar{\mathfrak{B}}\models\varphi(\bar{x})$ where $\varphi$ is forcing absolute, but $\mathfrak{B}\models\neg\varphi(x)$ where $x=\pi(\bar{x})$. Clearly $\neg\varphi$ is also forcing absolute, so in particular, "$\mathfrak{B}\models\neg\varphi(x)$" is forcing absolute, so by Claim 1, for sufficiently large $n$, $M_n(B)$ models 'it is forced by $\mathrm{Coll}(\omega,\mathrm{rank}(\mathfrak{B}))$ that $\mathfrak{B}\models\neg\varphi(x)$'. So $M_n(\bar{B})$ models the same about $\bar{\mathfrak{B}}$ and $\bar{x}$ (as the theory gets encoded into the $\#$ versions). We have an $(M_n(\bar{B}),\mathrm{Coll}(\omega,\mathrm{rank}(\bar{B})))$-generic $g\in V$ (as $M_n^\#(\bar{B})$ is countable). So for large $n<\omega$, $M_n(\bar{B})[g]$ models "$\bar{\mathfrak{B}}\models\neg\varphi(\bar{x})$". But $M_n(\bar{B})[g]=M_n(\bar{B},g)$, so this model is boldface-$\Sigma^1_{n+1}$ correct, so with $n$ large enough, this gives that $\bar{\mathfrak{B}}\models\neg\varphi(\bar{x})$, a contradiction.