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

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.