Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
    
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 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 at 13:31
2  
Erik Palmgren, in "An intuitionistic axiomatisation of real closed fields" (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 at 13:49
1  
@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 at 22:12
1  
@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 at 9:07

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

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.