Is there a deductive system for second-order logic that is complete with respect to Henkin semantics?

It is very easy to name such a deductive system, although it depends on exactly what you call "Henkin semantics". Recall that a prototypical completeness theorem states that a formula is derivable in a deduction system $\mathcal{D}$ if and only if the formula is true in each of a class of structures $\mathcal{S}$.

Basically, to obtain a complete deductive system for second-order logic (SOL), you treat SOL as multi-sorted first order logic, take a deductive system for the latter (which is already complete), and translate it to use the language of the former. That will give you a complete deductive system when $\mathcal{S}$ is the class of all Henkin structures. You can do this with any complete deduction system for first order logic.

However, it is common in SOL to think of set existence axioms as part of the logic itself, rather than part of a particular theory. In this case, one also adds to the deductive system the so-called comprehension scheme, which consists of each formula of the form $$ (\exists X)(\forall n)[n \in X \leftrightarrow \phi(n)] $$ where $X$ is not in $\phi$. The effect of that change is to ensure that every set which is definable (with parameters) over a model must exist in that model. To make this extended deductive system complete, we have to restrict the class of Henkin models to only those in which each definable set exists. This change to the deductive system and semantics is nearly universal in the study of SOL.

The axiom of choice is a trickier subject, for two reasons. First, not as many authors agree about whether the axiom of choice is part of second order logic (although, as I said, most do think that full comprehension is part of the logic [1]). So some authors include choice as part of the deductive system, and some do not. Those who do must further limit the collection of Henkin structures to those that satisfy the choice scheme they add to the deductive system.

The other tricky thing about choice is that it is not as robust a principle in SOL as it is in ZFC. In the context of ZFC, the axiom of choice for formulas of second-order arithmetic and the axiom of dependent choice for formulas of second-order arithmetic are equivalent relative to ZF, and many small variations of the axiom of choice are also equivalent to it. These equivalences happen because ZFC is so weakly typed. In the context of SOL, because of the strong typing of first- and second-order objects, choice principles will have different strengths depending on exactly what sort of objects they deal with. For example, in the context of second-order arithmetic, the scheme for the axiom of choice of numbers, $$ (\forall n)(\exists m) \phi(n,m) \to (\exists f)(\forall n)\phi(n,f(n)) $$ is weaker than the scheme for the axiom of choice of sets, $$ (\forall n)(\exists X) \phi(n,X) \to (\exists Y)(\forall n)\phi(n,(Y)_n) $$ which is again weaker than a scheme for dependent choice of sets, even in the presence of full comprehension. The relationships between choice schemes are laid out in chapter VII.6 of Simpson's book Subsystems of Second-order Arithmetic.

I also recommend Shapiro's book Foundations without Foundationalism, mentioned by Peter Smith, for a general introduction to second-order logic.

1: The notable exception to this is in reverse mathematics, where only parts of the comprehension scheme are used. The difference is because reverse mathematics is focused tightly on second-order arithmetic, not on second-order logic in general. For general second-order logic, it is harder to justify leaving out the comprehension scheme, because of the intended interpretation of the set quantifiers.