Completeness theorem for second-order logic in the language $\{\}$

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?

• Trying to understand. What is an example of a sentence in the language $\{\}$? You do have the predicate ‘=’ anyway? So I guess you have a sentence $(\forall x) (\exists y) x=y$. So is it true that all this language can do is express properties of equality? – GEdgar May 26 '16 at 13:59
• Yes, $=$ is allowed. For example, $\exists a\exists b(a\not = b)$ would be a sentence in the language $\{\}$ – thisismyname May 26 '16 at 14:02

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.