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$.
Lemma 1: If $A\models T$ and $A\res L_T=B\res L_T$, then $B\models 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
Lemma 2: $T\res L_T$ is equivalent to $T$.
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.
Lemma 3: If $T$ depends on $\kappa\ge\omega$ symbols, there exist models $\{A_\alpha:\alpha<\kappa\}$ and sentences $\{\phi_\alpha:\alpha<\kappa\}$ valid in $T$ such that
$$A_\alpha\models\phi_\beta\iff\alpha\ne\beta\tag1$$
for all $\alpha,\beta<\kappa$, and
$$T\models\phi\implies\{\alpha<\kappa:A_\alpha\nmodels\phi\}\text{ is finite}\tag2$$
for all sentences $\phi$.
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
Theorem: Every theory $T$ has an independent axiomatization.
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
