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

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.

-
Regarding the coherent version of (2), there exists a constructive proof of conservativity of classical logic over coherent logic, and thus every coherent sequent provable classically from coherent axioms admits already a coherent proof and this is established constructively. –  godelian Apr 29 '14 at 13:20
Excellent. How is that done? The only proof I am familiar with goes via Deligne's theorem, and I am under the impression that is non-constructive. –  Zhen Lin Apr 29 '14 at 13:31
Erik Palmgren, in "An intuitionistic axiomatisation of real closed ﬁelds" (MLQ, 2002) indicates a proof-theoretic proof by showing that coherent sequents are stable under the Dragalin-Friedman translation. Another proof is given in Sara Negri's "Contraction-free sequent calculi for geometric theories with an application to Barr's theorem" (Arch. Math. Log. 2003) using cut-free systems for the coherent fragment (Warning: In Negri's paper she calls geometric theories/implications what should actually be called coherent theories/sequents) –  godelian Apr 29 '14 at 13:49
@godelian: See very rough notes, still work in progress, on GitHub. Lots of explanations and references are still missing, also some proofs and a proper copyediting. The material you are interested in is in section 6 (Modalities), in particular section 6.6 (The $\Box$-translation). I'd be happy to discuss any questions regarding these notes! –  Ingo Blechschmidt May 2 '14 at 22:12
@Ingo: Thanks a lot for this material! I'll study it, and if there are questions to discuss I'll contact you privately –  godelian May 3 '14 at 9:07

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.

-