It is well-known that the completeness theorem fails for second-order logic. In particular, there is no calculus $C$ that proves exactly those second-order sentences $\phi$ in the language $\{0, s, +, \cdot\}$ which are valid (valid means true in every interpretation/model). This is because of Gödels Incompleteness theorem: If there was such a calculus $C$, this would contradict the assertion of Gödels Incompleteness theorem, since the sentence $\mathrm {PA}\rightarrow \varphi$ is valid if and only if $\varphi$ is true in the standard model $\mathbb N$ of the peano axioms. ($\mathrm{PA}$ denotes the conjunction of the second-order peano axioms.)
My question is: Is there a complete calculus for second-order logic in the empty language $\{\}$ with no constant symbols, no function symbols and no relation symbols? That is to say: Is there a calculus $C$ that proves exactly those second-order sentences $\phi$ in the language $\{\}$ which are valid?
No, second-order logic over the empty language is basically as powerful as second-order logic over an arbitrary language. To see this, suppose $\varphi$ is a second-order sentence with some non-logical symbols; let $\psi$ be the sentence gotten by "universally quantifying out" the non-logical symbols in $\varphi$. For example, if $\varphi$ is the sentence $$\forall x\exists y(xRy),$$ then $\psi$ would be $$\forall R\forall x\exists y(xRy).$$ It's not hard to see that $\psi$ is valid iff $\varphi$ is valid, but $\psi$ uses no non-logical symbols.