The answer to the question is yes.
Let $\alpha_0<\alpha_1$ be the least ordinals (in the reverse lex order, say) such that $V_{\alpha_0}$ and $V_{\alpha_1}$ have the same second order theory $T$. Assume towards a contradiction that $V_{\alpha_0}$ and $V_{\alpha_1}$ are elementarily embeddable into a common structure $M$, which we may assume is transitive. Note that the embeddings fix $T$. Since $V_{\alpha_1}$ satisfies that there is an ordinal $\beta$ such that $V_\beta$ satisfies $T$, so does $M$, and hence so does $V_{\alpha_0}$. But this means that some $\beta < \alpha_0$ has the same theory as $V_{\alpha_0}$, contrary to the minimality of the pair $\alpha_0 < \alpha_1$.
(Edit: I now see this is very close to what Trevor was doing.)
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.
Best Answer
Here is a proof of Reznikoff’s theorem I found among my notes, not quite following Reznikoff’s proof. I stared at it for a while, and it seems to apply to second-order logic just the same; in fact, the only property of first-order logic it uses is that any sentence contains only finitely many non-logical symbols, and there are only countably many sentences in any given finite language. Let me know if I missed something.
We say that a theory $T$ in a language $L$ depends on a predicate or function symbol $s\in L$ if there are models $A\models T$, $B\let\nmodels\nvDash\nmodels T$ such that $A\let\res\restriction\res(L\let\bez\smallsetminus\bez\{s\})=B\res(L\bez\{s\})$. Let $L_T$ denote the set of symbols $s\in L$ on which $T$ depends. If $L'\subseteq L$, let $T\res L'$ be the set of $L'$-sentences valid in $T$.
Proof: Fix $\phi\in T$, we will show $B\models\phi$. Let $\{s_i:i<n\}$ enumerate the symbols of $L\bez L_T$ occurring in $\phi$, and for $i\le n$, let $A_i$ denote $A$ with the interpretation of $s_j$ changed to $s_j^B$ for each $j<i$. Applying $n$ times the definition of $L_T$, we see that $A_i\models T$ for each $i\le n$, thus $A_n\models\phi$. But $A_n$ and $B$ agree on all symbols that occur in $\phi$, hence $B\models\phi$. QED
Proof: For every $L$-sentence $\phi$, we define an $L_T$-sentence $\phi'$ by replacing all predicates $P\in L\bez L_T$ with $\bot$, and all functions $F\in L\bez L_T$ by a fixed fresh variable $x$, and putting a universal quantifier $\forall x$ in front of the whole formula. Similarly, if $A$ is an $L_T$-model and $c\in A$, we define an $L$-model $A_c$ expanding $A$ by $P^{A_c}=\varnothing$ and $F^{A_c}(\vec a)=c$. Clearly, $$A\models\phi'\iff\forall c\in A\:A_c\models\phi.$$ If $T\models\phi$ and $A\models T$, then $(A\res L_T)_c\models T$ for each $c\in A$ by Lemma 1, hence $(A\res L_T)_c\models\phi$, and $A\models\phi'$. That is, if $T\models\phi$, then $\phi'\in T\res L_T$.
Consequently, if $A\res L_T\models T\res L_T$, then $A\res L_T\models\{\phi':T\models\phi\}$, i.e., $(A\res L_T)_c\models T$ for any $c\in A$, and therefore $A\models T$ by Lemma 1. Thus, every model of $T\res L_T$ is a model of $T$. QED
NB: Alternatively, Lemma 2 can be proved using the Craig interpolation lemma.
Proof: Assume that $T$ depends on all symbols in $\{s_\alpha:\alpha<\kappa\}$, and pick models $A_\alpha\nmodels T$, $A'_\alpha\models T$ such that $A_\alpha$ and $A'_\alpha$ differ only in the interpretation of $s_\alpha$. For each $\alpha<\kappa$, fix a sentence $\xi_\alpha$ such that $T\models\xi_\alpha$ and $A_\alpha\nmodels\xi_\alpha$.
Since $A'_\alpha\models T$, we see that $A_\alpha\nmodels\phi$ for $T\models\phi$ can only happen when $s_\alpha$ appears in $\phi$. Since only finitely many symbols appear in $\phi$, this implies (2). Moreover, considering $\phi=\xi_\alpha$, it implies that for each $\alpha<\kappa$, only finitely many $A_\beta$ can satisfy the same sentences as $A_\alpha$, thus there are $\kappa$ inequivalent models on the list; w.l.o.g., we may assume that $A_\alpha\not\equiv A_\beta$ whenever $\beta\ne\alpha$.
Fix $\alpha<\kappa$. We already know that $\{\beta\ne\alpha:A_\beta\nmodels\xi_\alpha\}$ is finite; let us enumerate it as $\{\beta_{\alpha,i}:i<n_\alpha\}$. For each $i<n_\alpha$, we fix a sentence $\zeta_{\alpha,i}$ such that $A_{\beta_{\alpha,i}}\models\zeta_{\alpha,i}$ and $A_\alpha\nmodels\zeta_{\alpha,i}$. Then we put
$$\phi_\alpha=\xi_\alpha\lor\bigvee_{i<n_\alpha}\zeta_{\alpha,i},$$
and observe that it makes (1) hold. QED
Proof: Put $\kappa=|L_T|$, and assume first that $\kappa$ is infinite. Let $\{A_\alpha:\alpha<\kappa\}$ and $\{\phi_\alpha:\alpha<\kappa\}$ be as in Lemma 3. Enumerate $T\res L_T$ as $\{\chi_\alpha:\alpha<\kappa\}$, and define
$$\begin{align*} \psi_\alpha&=\Bigl(\let\ET\bigwedge\ET_{\beta\colon A_\beta\nmodels\chi_\alpha}\phi_\beta\Bigr)\to\chi_\alpha,\\ S&=\{\phi_\alpha\land\psi_\alpha:\alpha<\kappa\}. \end{align*}$$ Since $T\equiv T\res L_T$ by Lemma 2, it is clear that $S\equiv T$. Moreover, $A_\alpha\models\phi_\beta\land\psi_\beta$ for $\beta\ne\alpha$, but $A_\alpha\nmodels\phi_\alpha$, hence $S$ is independent.
If $\kappa$ is finite, $T$ has a countable axiomatization $\{\phi_n:n<\omega\}$ by Lemma 2. Put
$$\begin{align*} \psi_n&=\Bigl(\ET_{i<n}\phi_i\Bigr)\to\phi_n,\\ S&=\{\psi_n:n\in\omega,\text{ $\psi_n$ is not logically valid}\}. \end{align*}$$
Since $\ET_{i\le n}\psi_i$ is equivalent to $\ET_{i\le n}\phi_n$, $S\equiv T$. Moreover, since $\psi_n\in S$ is not valid, there is $A_n\models\neg\psi_n$. This means $A_n\models\phi_i$ for $i<n$ and $A_n\models\neg\phi_n$, which implies $A_n\models\{\psi_i:i\ne n\}$. Thus, $S$ is independent. QED