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.


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

  • $\begingroup$ 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!) $\endgroup$
    – Hanul Jeon
    Commented Sep 27, 2014 at 2:06
  • $\begingroup$ I do not understand what the second paragraph is asking. Could you rephrase it? $\endgroup$ Commented Sep 27, 2014 at 12:46
  • $\begingroup$ @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). $\endgroup$
    – user40276
    Commented Sep 28, 2014 at 18:50
  • $\begingroup$ @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. $\endgroup$ Commented Sep 29, 2014 at 0:31
  • $\begingroup$ @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)... $\endgroup$
    – user40276
    Commented Sep 30, 2014 at 22:23

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


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .