For $S$ a set of (parameter-free) second-order formulas and $\mathfrak{A},\mathfrak{B}$ structures, write $\mathfrak{A}\trianglelefteq^S\mathfrak{B}$ iff $\mathfrak{A}$ is a substructure of $\mathfrak{B}$ and for every formula $\varphi(\overline{x};\overline{y})\in S$ and every $\overline{a}\in\mathfrak{A}^{\vert\overline{y}\vert}$, we have $\varphi(-;\overline{a})^\mathfrak{B}\not=\emptyset\implies \varphi(-;\overline{a})^\mathfrak{A}=\varphi(-;\overline{a})^\mathfrak{B}\cap\mathfrak{A}^{\vert\overline{x}\vert}.$ More familiarly, let $\mathfrak{A}\preccurlyeq^S\mathfrak{B}$ iff $\mathfrak{A}$ is a substructure of $\mathfrak{B}$ and for every formula $\varphi(\overline{x};\overline{y})\in S$ and every $\overline{a}\in\mathfrak{A}^{\vert \overline{y}\vert}$, we have $\varphi(-;\overline{a})^\mathfrak{A}=\varphi(-;\overline{a})^\mathfrak{B}\cap\mathfrak{A}^{\vert\overline{x}\vert}.$
Now say that:
a set of second-order formulas $S$ is self-enforcing iff $\trianglelefteq^{\mathsf{FOL}\cup S}=\preccurlyeq^{\mathsf{FOL}\cup S}$; and
a single second-order formula $\varphi$ is self-enforcing iff $\{\varphi\}$ is self-enforcing in the above sense.
For example, the formula asserting that an element is in the ill-founded part of a binary relation is self-enforcing (see the second footnote in this earlier question of mine). Moreover, the set $S_0$ of self-enforcing formulas is clearly self-enforcing, and there is a largest self-enforcing set of formulas $S_\infty$ (since the union of self-enforcing sets is again self-enforcing).
My question is whether these sets of formulas are different, at least in terms of the logics they generate:
Are (the sublogics of $\mathsf{SOL}$ given by) $S_0$ and $S_\infty$ expressively equivalent?
Recall that two logics are expressively equivalent iff they have the same elementary classes. (In the absence of compactness this is stronger than merely asking for them to have the same elementary equivalence notions.)
