There are two semantics used for second-order logic, Henkin semantics and standard semantics. It’s easy to make a recursive deductive system $D$ that is sound and complete with respect to Henkin semantics. Furthermore, $D$ is also sound with respect to standard semantics, but it is not complete. This is because no recursive deductive system can be both sound and complete with respect to standard semantics, as the set of second-order logical validities with respect to standard semantics is not recursively axiomatizable or even arithmetical.
My question is, what examples are there of recursive extensions of $D$, in the language of pure second-order logic, which are sound with respect to standard semantics? Are there any natural examples?
I know the set of second-order logical validities is definable in the language of $ZFC$ and even in the language of $\lambda+1^{st}$-order arithmetic where $\lambda$ is the Lowenheim number of second-order logic (which is bigger than many large cardinals if they exist). So there are some recursively enumerable sets of sentences which those two theories prove are second-order logical validities. But first of all those theories are not written in the language of pure second-order logic, and second of all I imagine they prove far, far more second-order logical validities than $D$ does. So I’m interested in systems of intermediate strength between $D$ on the one hand, and $\lambda+1^{st}$-order arithmetic and $ZFC$ on the other.
Really an overly-long comment:
Any subtheory of $\mathsf{ZFC}$ gives rise to such a system, just as $\mathsf{ZFC}$ does. Specifically, corresponding to each $T\subseteq\mathsf{ZFC}$ have the deduction relation $\vdash_T$ given by $$\psi\vdash_T\varphi\quad\iff\quad T\vdash(\psi\models_2 \varphi)$$ where "$\models_2$" is the standard-semantics entailment relation for second-order logic and I'm restricting attention to the single-sentence-hypothesis case of entailment to make the "$T$-ification" in the right hand side completely unproblematic.
At a glance, $\vdash_{\mathsf{KP}}$ falls short of the deduction relation for Henkin semantics only as far as choice principles are concerned. So a natural place to look for a moderately-stronger system is, for example, $\vdash_{\mathsf{2KPC}}$, where $\mathsf{2KPC}$ is $\mathsf{KP}$ + $\Sigma_2$-$\mathsf{Rep}$ + $\mathsf{AC}$.
(Meanwhile, the following seems quite hard: which deduction relations arise as $\models_T$s for $T$ a consistent c.e. extension of $\mathsf{KP}$?)