Constructive Proof that Intuitionistic Higher-Order Logic is Conservative over Constructive First-Order Logic In the classical setting, we know that higher-order logic is conservative over first-order logic.
More precisely, consider a classical first-order many-sorted theory $T$, and consider some sentence $\phi$. If we can prove in higher-order logic that $T \vdash \phi$, then we can also prove this in first-order logic. For if $T \nvdash \phi$ in first-order logic, then $T \cup \{\neg \phi\}$ would be consistent, and we would have a model $M$ of $T \cup \{\neg \phi\}$ by the completeness theorem. From $M$, we can construct a higher-order logic model in the obvious way, which will of course also be a model of $T \cup \{\neg \phi\}$, which is not possible.
It is also known that given any theory $T$ in intuitionist higher-order many-sorted logic, we can construct a topos $\epsilon$ and select, for each sort $S$, an object $\epsilon_S$ of $\epsilon$ such that for all sentences $\phi$, $\epsilon \Vdash \phi$ if and only if $T \vdash \phi$.
In particular, then, for any many-sorted classical first-order theory $T$, there exists a Boolean topos $B$ which models only the sentences which follow from $T$ in first-order logic.
I would like to generalise this situation to constructive first-order logic. In other words, I would like to show that for any constructive theory $T$ in first-order logic, there is a topos $\epsilon$ such that for all sentences $\phi$, $T \vdash \phi$ if and only if $\epsilon \Vdash \phi$. Equivalently, I would like to show that intuitionist higher-order logic is conservative over constructive first-order logic. Finally, I require that this proof be intuitionistically valid.
Another way of expressing this claim is that for every Heyting category $H$, there is a topos $Q$ and a Heyting functor $F : H \to Q$; furthermore, for every object $X \in H$, the induced Heyting algebra homomorphism $sub(X) \to sub(FX)$ is injective. It actually suffices to show that for all $X \in Q$, $FX$ is terminal if and only if $X$ is terminal.
A classical proof of this theorem can be derived from the completeness of Kripke semantics. Kripke semantics is just the usual forcing semantics for presheaves on a poset. Kripke completeness therefore means that we can actually pick $Q$ to be a presheaf topos on a poset for the above, which is a nice strengthening of our result. However, proving the completeness of Kripke semantics itself requires some amount of classical logic and is therefore constructively inadmissible.
 A: Yes. One topos we can choose is the Grothendieck topos $Q = Sh(H)$, the topos of sheaves on $H$ (using the coherent topology), and we can take $F : H \to Q$ to be the Yoneda embedding.
First, we prove a slightly more general version of the theorem. Let $C$ be a coherent category, and let $T$ be the corresponding coherent topos $Sh(C)$. Note that the coherent topology is subcanonical, so the Yoneda functor $F : C \to T$ is well-defined. I claim that $y$ is a coherent functor.
Indeed, the Yoneda functor $y = UF : C \to Set^{C^{op}}$ always preserves all limits. And the forgetful functor $U : Sh(C) \to Set^{C^{op}}$ creates limits. Therefore, $F$ preserves limits.
Now suppose $f : A \to B$ is a regular epi in $C$. I claim that $Ff$ is a regular epi in $Sh(C)$. It suffices to show that $Ff$ is epi. Suppose we have $g, h : FB \to \mathcal{D}$ such that $g \circ Ff = h \circ Ff$. Then doing some clever Yoneda stuff, we have $\mathcal{D}(f)(\mathcal{D}(g_B(1_B))) = \mathcal{D}(f)(\mathcal{D}(h_B(1_B))$.
Now $\mathcal{D}$ is a sheaf. Note that $\{f : A \to B\}$ is a covering family. It follows that $\mathcal{D}(g_B(1_B)) = \mathcal{D}(h_B(1_B))$, and thus $g = h$. So $Ff$ is an epi, as required.
Now suppose we have subobjects $\{s_i : S_i \to A \mid 0 \leq i < n\}$ such that $s_0 \lor \cdots \lor s_{n - 1} = \top$ as subobjects of $A$. Let $I = \{i \in \mathbb{N} \mid 0 \leq i < n\}$. We wish to show that $F s_0 \lor \cdots \lor F s_{n - 1} = \top$ as subobjects of $FA$. We identify each subobject $F s_i : F S_i \to FA$ with the corresponding subsheaf $F(s_i)(C) = \{g : C \to A \mid g$ factors through $s_i\}$, and we also identify the join with the corresponding subsheaf.
Indeed, consider an arbitrary $f \in F(A)(B)$: that is, an arbitrary $f : B \to A$: we wish to show $f \in \bigvee\limits_{i \in I} F s_i$. Note that $\{s_i : S_i \to A\}_{i \in I}$ is a covering family. Therefore, so is $\{f^*(s_i) : f^*(S_i) \to B\}_{i \in I}$. Thus, it suffices to show that for all $i \in I$, $FA(f^*(s_i))(f) \in (\bigvee\limits_{i \in I} F s_i)(S_i)$. Note that $FA(f^*(s_i))(f) = f \circ f^*(s_i)$. By the definition of pullback, $f \circ f^*(s_i)$ factors through $s_i : S_i \to A$ and is therefore in $F(s_i)(S_i) \subseteq (\bigvee\limits_{i \in I} F s_i)(S_i)$. This completes the proof. $\square$
Now we need only show that in the original case, $F$ also preserves dual images. Then, we'll be done. Consider $f : A \to B$ and monic $m : S \to A$. The subsheaf (equivalent to) $F (\forall_f m) : F (\forall_f S) \to FA$ is given by $C \mapsto \{g : C \to A \mid g$ factors through $\forall_f m\}$, while the subsheaf $\forall_{(Ff)} (Fm) : \forall_{(Ff)} (FS) \to FA$ is given by $C \mapsto \{g : C \to A \mid \forall D \forall h : D \to C \forall i : D \to B (f \circ i = g \circ h \to i \to i \in FS(D))\}$. The fact that $F(\forall_f m) \subseteq\forall_{(Ff)}(Fm)$ follows from the fact that $F$ preserves pullbacks. For the other direction, suppose $g \in \forall_{(Ff)}(Fm)(C)$. That is, $g : C \to A$ and for all $D$, $h : D \to C$, and $i : D \to B$ such that $f \circ i = g \circ h$, $i$ factors through $m$. Since $\forall_{(Ff)}(Fm)$ is a sheaf, we can factor $g$ into an epi and a mono, and the image of $g$ is in $\forall_{(Ff)}(Fm)$ if and only if $g$ is. So without loss of generality, we suppose $g$ is mono.
Now let $(D, h, i)$ be the pullback of $g$ and $f$. Then $f \circ i = g \circ h$, so $i$ factors through $m$. But $i$ is $f^{-1}(g)$, so $i \leq m$ if and only if $g \leq \forall_f m$. So $g$ factors through $\forall_f m$, and thus $g \in F(\forall_f m)(C)$. Thus, we see that $\forall_{(Ff)}(Fm)$ is indeed a subsheaf of $F(\forall_f m)$, as required.
Thus, we see that $F$ is a Heyting functor.
Note that there is a minor size issue here, since the Grothendieck topos will, in general, be a large category. However, we can just take the full subcategory of $Sh(H)$ generated by the image of $F$, finite limits, and power objects, which will be a small logical subtopos of $Sh(H)$. There is a modest amount of subtlety here. We could be working in an extremely weak metatheory - perhaps that of, say, BZC. BZC cannot prove that there exists a nontrivial topos with natural numbers object, but it can prove that Peano arithmetic is consistent. In any topos $T$ with a model $N$ of the Peano axioms, we can find a natural numbers object $\mathbb{N} = \{i \in N \mid \forall S \subseteq N, 0 \in S \land \forall x \in S (s(x) \in S) \to i \in N\}$. So we cannot prove this theorem in BZC. We need stronger axioms to get the result we want.
