Completness in higher order logic and Interpretations

Question

It´s known that for first order theories, it holds $\mathbf{ZFC} \vdash T \vdash \varphi \leftrightarrow T \models \varphi$. Why does this not hold in the higher order case (any simple example?)?

Furthermore if I change models by interpretations, does it hold that $T \vdash \varphi$ iff for all interpretations (in the sense defined by Tarski) $M$ of the language $L (T)$ (the underlying language of the theory $T$) in a theory $T'$, $T' \vdash\varphi^M$ for the higher order case (I´m interested mainly in the second order case)?

Thanks in advance.

EDIT

For first order languages:

An interpretation $I$ of a language $L$ in a language $L'$ is a correspondence that associates for each predicate symbol $P$ of $L$ a predicate symbol $P_I$ of $L'$. And for each function symbol $f$ in $L$ a function symbol $f_I$ of $L'$.

Furthermore, given a (first order) theory $T'$ in $L'$, then I is said to be a interpretation of $L$ in $T'$ if

$1)$ There is a fixed predicate symbol in $\mathfrak{U}_I$, called the domain.

$2)$For each function symbol $f$ in $L$, $T'\vdash\mathfrak{U}_I x_1 \rightarrow … \rightarrow \mathfrak{U}_Ix_n \rightarrow \mathfrak{U}_If_I x_1…x_n$

Moreover, given a theory $T$ in $L$, $I$ is said to be an interpretation of $T$ in $T'$ if for each formula $\varphi$ it holds that $T'\vdash\mathfrak{U}_I x_1 \rightarrow … \rightarrow \mathfrak{U}_Ix_n \rightarrow \varphi^I $ where $\varphi^I$ is defined inductively as:

$\exists x (\mathfrak{U}_I x \wedge \psi^I)$ if $\varphi$ is $\exists x\psi$

and the other cases (negation, conjunction, predicate symbol, function symbol etc) in the obvious way.

The main difference between models and interpretations are that in a model the predicate $\mathfrak{U}_I$ defines a set and that $T' \vdash \forall y (y \ \text{axiom of T}) \rightarrow I \models y$. While, in an interpretation, it just holds that for every axiom $\varphi$ of $T$, $T' \vdash \varphi^I$.

Answer 1

Answering the first paragraph of the question only: it does hold in the higher-order case, using Henkin semantics. If $T$ is a theory in higher-order logic, we have that $T \vdash \phi$ if and only if every Henkin model of $T$ satisfies $\phi$.

The sense in which the completeness theorem fails is that, if we do not look at all Henkin models, but only at some subclass of them, it may be that all models of $T$ in this subclass satisfy $\phi$, but $T \not\vdash \phi$, because there are other models of $T$ that don't satisfy $\phi$. The most common such subclass that people consider is the class of "full" models, in which the second-order part is the powerset of the first-order part. This is sometimes called "standard semantics". Note that exactly the same phenomenon occurs in first-order logic if we only look at some arbitrary subclass of the possible models of a sentence rather than the full class of possible models: it could be that a sentence holds in all models of the subclass, but still is not provable.

This is all standard information about second-order logic that can be found in any standard reference, e.g. Shapiro's book or the Stanford Encyclopedia article on second-order logic.

A specific example where the restriction to full models makes a difference is with second-order Peano arithmetic, $Z_2$. This has only one full model, $M$, which is the standard model of arithmetic. So for each $\phi$ in the language we have $M\vDash \phi$ if and only if $\phi$ is true. But $Z_2$ is still an effectively axiomatized theory to which Gödel's incompleteness theorem applies, so there will be many sentences $\phi$ in the language that are true but not provable in $Z_2$.