*Previously [asked and bountied](https://math.stackexchange.com/questions/4318032/does-the-absolute-fragment-of-second-order-logic-satisfy-a-strong-lowenheim-skol) 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.



Can the forcing-absolute fragment of SOL have a strong Lowenheim-Skolem property?
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.


