Completness in higher order logic and Interpretations

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)?

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$.

• There is a proper formalization of 'logical axioms' in higher-order logic? Set of valid sentences of second-order logic (under standard semantics) is not r.e. (In fact, it is not even arithmetically definable!) – Hanul Jeon Sep 27 '14 at 2:06
• I do not understand what the second paragraph is asking. Could you rephrase it? – Carl Mummert Sep 27 '14 at 12:46
• @CarlMummert Well, the completeness is for models, in the sense, that if a formula holds for every model, then it holds globally, i.e., it's provable. I was trying to see how it would work for interpretations instead of models (since interpretations are more general than models). – user40276 Sep 28 '14 at 18:50
• @user40276: I would love to answer that, but the problem is that, in my mind, interpretations are models. I am intrigued that you have a different definition for "interpretation" than for "model". Could you state a definition of what an "interpretation" is, and how it's different than a model? By model I mean a structure in the sense of model theory, which gives a domain of discourse and also gives meanings to all the symbols of the language. – Carl Mummert Sep 29 '14 at 0:31
• @CarlMummert Sure. I've tried to edit properly. As you can see, by a model I mean an internal thing of $ZF$ while an interpretation is a metamathematical thing. Maybe interpretations are generalizations of models under some assumptions and not in the more general case (as I was thinking)... – user40276 Sep 30 '14 at 22:23

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.
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$.