There are several theorems in category-theoretic logic which say something like, "any proposition in X logic that is provable in topos logic assuming (the law of excluded middle and) the axiom of choice is provable in X logic itself (i.e. without the law of excluded middle and the axiom of choice)". However, some of these theorems are themselves non-constructive, so one is left wondering whether one really can "obtain" a constructive proof in this fashion.

More concretely, consider a geometric theory $\mathbb{T}$, i.e. a theory in a certain fragment of infinitary intuitionistic first-order logic. Topos theory tells us:

1. There is a topos $\mathbf{Set}[\mathbb{T}]$ containing a "conservative" model of $\mathbb{T}$, i.e. one where everything that is true is also provable.
2. By Barr's theorem, there is a surjective geometric morphism $\mathcal{B} \to \mathbf{Set}[\mathbb{T}]$ where $\mathcal{B}$ is a boolean topos with the (internal) axiom of choice. Note that $\mathcal{B}$ also contains a conservative model of $\mathbb{T}$.

I think (1) is constructive, but (2) is not. Thus, using classical mathematics, we deduce that every sequent in (the language of) $\mathbb{T}$ that we can verify (by any means!) in the conservative model in $\mathcal{B}$ admits a proof in $\mathbb{T}$; but non-constructiveness in (2) prevents us from actually extracting that proof.

Now, maybe the problem is that $\mathbb{T}$ potentially contains axioms of infinite length. So let's restrict to the finitary fragment of geometric logic, also known as coherent logic. There we have an even stronger completeness theorem:

• If $\mathbb{T}$ is a coherent theory, then a sequent is provable in $\mathbb{T}$ if and only if it is true in every model of $\mathbb{T}$ in $\mathbf{Set}$.

Question. Let $\mathbb{T}$ be a coherent theory that can be defined in reasonable metatheories – so perhaps the metatheory is an extension of higher order Heyting arithmetic and $\mathbb{T}$ is a recursive theory in a language with countably many sorts. Let $\phi \vdash \psi$ be a sequent in (the language of) $\mathbb{T}$. Can the provability of $\phi \vdash \psi$ depend on the metatheory?

Of course one could cheat and define $\mathbb{T}$ so that, say, $\mathbb{T}$ is inconsistent when some condition is satisfied in the metatheory. I'm more interested in those theories $\mathbb{T}$ where every reasonable metatheory agrees on the axioms of $\mathbb{T}$ – perhaps such that every reasonable metatheory agrees on whether a given standard natural number codes an axiom of $\mathbb{T}$, if that makes sense.