Conservative extension in higher order logic?

Question

Specifically I am interested in the prerequisites of a valid extension by definition, like in FOL before introducing an n-ary function symbol (e.g. $f$) for the extension to be conservative we have to prove $\forall \vec x:\exists !y:\phi(y,\vec x)$. What theorems one has to prove in HOL for an extension to be conservative?

I would somehow expect it to be a general requirement, as in FOL a new relation symbol needs no proof to be safely introducible, but in HOL relations and operations are on more equal footing.

Answer 1

The proof systems for higher-order logic are not different in any important way from the proof systems for first-order logic. So, as long as your notion of "conservative extension" is phrased (as usual) in terms of provability, there is no difference in how to make a conservative extension.

Start with the syntactic definition of a conservative extension by a function symbol:

Definition. A theory $S$ is a conservative extension of a theory $T$ if $T$ is a subset of $S$ and every sentence in the language of $T$ that is provable in $S$ is already provable in $T$.

Then we have:

Theorem. Let $T$ be a higher-order theory with full semantics. If $T \vdash (\forall x)(\exists y) \psi(x,y)$, and $S$ is $T$ plus an extra function symbol $f$ and an extra axiom $(\forall x)\psi(x, f(x))$ then $S$ is a conservative extension of $T$.

Proof. Let $T_1$ and $S_1$ be the same syntactic theories as $S$ and $T$, but with first-order semantics (that is, Henkin semantics). Then we have $T \vdash \phi$ if and only if $T_1 \vdash \phi$ for all $\phi$ in the language of $T$, and a similar equivalence for sentences in the language of $S$. This is because the proof system does not depend on and does not care about the semantics that we choose.

Now, standard results about first-order theories show that if $\phi$ is a sentence in the language of $T_1$ and $S_1 \vdash \phi$ then $T_1 \vdash \phi$. But, because of the the facts in the previous paragraph, and because the language of $T$ is the same as the language of $T_1$, it follows immediately that $S$ is a conservative extension of $T$. $\quad \blacksquare$

We could also look at a different kind of "conservative extension":

Definition. A theory $S$ is a semantically conservative extension of a theory $T$ if $T$ is a subset if $S$ and every model of $T$ can be expanded to a model of $S$.

Then we have the same kind of theorem:

Theorem. Let $T$ be a higher-order theory with full semantics. If $T \vdash (\forall x)(\exists y) \psi(x,y)$, and $S$ is $T$ plus an extra function symbol $f$ and an extra axiom $(\forall x)\psi(x, f(x))$ then $S$ is a semantically conservative extension of $T$.

Proof. Let $M$ be a model of $T$. By the axiom of choice, there is a function $F$ such that $$(\forall x \in |M|)(\exists y \in |M|) \phi(x, F(x)).$$ Because $M$ is a model under full semantics, $F$ is already an element of one of the sorts of $M$. Therefore, if we simply interpret the new symbol $F$ as $f$, this gives an expansion $M'$ of $M$ that satisfies $S$. It is immediate that $M'$ still satisfies $T$, because we have not changed any of the sorts nor the interpretation of any symbol in the language of $T$. The fact that $M$ satisfies $(\forall x)\psi(x,f(x))$ follows directly from the choice of $F$. $\quad \blacksquare$

Notice that in the second (semantic) situation, if we are looking at $(n+1)$-st order logic, the proof needs $f$ to be of type $n+1$ or lower. In the first (syntactic) situation, $f$ could also be of type $n+2$.