What makes higher/second-order logic incompatible with completeness theorem? Completeness theorem and compactness theorem do not hold in full second and higher-order logic. What makes them incompatible with the theorems? Is it somehow related to Russell's paradox or diagonalization issues?
Thanks.
 A: For the Compactness Theorem:
Take second-order Peano arithmetic, that is, the original Peano arithmetic, with full second-order version of induction. The language of Peano arithmetic in particular has a constant symbol $0$, and a unary function symbol $S$ for the successor function. It is not hard to show that second-order Peano arithmetic is categorical: any two models are isomorphic. 
Add to the language a new constant symbol $B$. Add to second-order Peano arithmetic the infinitely many special axioms $\lnot(B=0)$, $\lnot(B=S(0))$, $\lnot(B=S(S(0)))$, $\lnot(B=S(S(S(0))))$, and so on forever.
Any finite subset $T_{\text{fin}}$ of this theory has a model. Just interpret $B$ as a natural number larger than any of the natural numbers "mentioned" in the finitely many special axioms that occur in $T_{\text{fin}}$. But the full theory does not have a model, since such a model cannot be isomorphic to the natural numbers. Thus the Compactness Theorem is violated. 
A: The reason is that (the set of valid formulas) of these systems are not c.e. and therefore do not have effective proof systems, i.e. there is no c.e. set of axioms that would formalize them.
Here I am using the word proof system in the usual sense, i.e. a decidable set of axioms and rules and a proof is finite structure built from them. In addition given a string and a formula we can decide if the string is a proof of the formula. If we modify the requirements we can have a proof system and a completeness theorem. For example, we can add the $\omega$-rule and then anything in second order arithmetic is derivable. We can combine these ideas with computability and consider only those proof objects which have finite representations, e.g. a Turing machine gives their bits. There is considerable amount of literature in proof theory on these topics.
