Is it possible for a theorem to be constructive only in a non-constructive metatheory?

Question

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.

Answer 1

You can ask the same question about arithmetical theories, and the answer may be illuminating.

For most arithmetical examples, when we can establish provability non-constructively, we can also establish it constructively within a few years.

See Jeremy Avigad's 1998 talk on Semantic Methods in Proof Theory. That has examples like:

Theorem. $B\Sigma_{k+1}$ is $\Pi_{k+2}$-conservative over $I\Sigma_k$. Original proofs by Paris and Friedman (independently) were semantic. Sieg offered the first proof-theoretic proof.

He surveys semantic methods for establishing provability, and in every case he mentions a syntactic method to the same end.

The one contrary example I see in his talk is the Paris-Harrington statement, whose unprovability in PA is established only semantically.

So for arithmetical theories, it is rare and usually temporary for theorems to be shown provable only in a non-constructive metatheory. I don't have good data on whether the same pattern holds for geometric theories with topos-theoretic metatheories; perhaps others do, or perhaps it remains to be seen.