Timeline for Is it possible for a theorem to be constructive only in a non-constructive metatheory?
Current License: CC BY-SA 3.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Jul 3, 2017 at 15:09 | history | suggested | Matthieu FG |
added cat log tag
|
|
| Jul 3, 2017 at 14:51 | review | Suggested edits | |||
| S Jul 3, 2017 at 15:09 | |||||
| May 3, 2014 at 9:07 | comment | added | godelian | @Ingo: Thanks a lot for this material! I'll study it, and if there are questions to discuss I'll contact you privately | |
| May 2, 2014 at 22:16 | comment | added | Ingo Blechschmidt | @godelian: For the Friedman translation with respect to a fixed formula $\alpha$, use the topology given by $\varphi \mapsto \varphi \vee \alpha$ (read this as a term in the internal language). Often, one needs to first apply the double negation translation and then the Friedman translation; this can be realized by the topology $\varphi \mapsto ((\varphi \Rightarrow \alpha) \Rightarrow \alpha)$. Fun fact: Let $X$ be a topological space and $x \in X$ be a point. Then, for suitable $\alpha$, this topology gives the subtopos Sh$(\{x\})$ of Sh$(X)$. This has useful consequences (see the notes). | |
| May 2, 2014 at 22:12 | comment | added | Ingo Blechschmidt | @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! | |
| Apr 30, 2014 at 12:47 | comment | added | godelian | @Ingo: That is very interesting, thanks! I would be certainly interested in reading the details, as well as the topology that you need to use for Friedman's translation | |
| Apr 30, 2014 at 6:51 | comment | added | Ingo Blechschmidt | @godelian: Such a development is indeed possible, using Lawvere-Tierney topologies. For instance, let $\varphi^{\neg\neg}$ denote the Gödel-Gentzen negative translation of a formula $\varphi$. Then $\mathcal{E} \models \varphi^{\neg\neg}$ is equivalent to $\mathrm{Sh}_{\neg\neg}(\mathcal{E}) \models \varphi$, where $\mathrm{Sh}_{\neg\neg}(\mathcal{E})$ denotes the subtopos of sheaves in $\mathcal{E}$ with respect to the double negation topology. The case for the Friedman translation is similar. I can make details available, if you are interested. | |
| Apr 29, 2014 at 23:09 | comment | added | Zhen Lin | Good point. I wasn't thinking carefully enough. Of course, it's still weaker than the full classical completeness theorem for coherent logic, which (if I recall correctly) is already equivalent to the boolean prime ideal theorem (at least when the metatheory has LEM). | |
| Apr 29, 2014 at 22:40 | comment | added | godelian | @Zhen: I believe the methods of Erik's proof could be adapted as soon as one develops a sort of geometric version of Gödel-Gentzen negative translation (and Friedman's translation as well). Note, however, that this would only eliminate the uses of excluded middle in the proof, and does not answer whether eventual uses of stronger principles, like, e.g., the axiom of choice, could also be eliminated. | |
| Apr 29, 2014 at 16:23 | comment | added | Zhen Lin | @godelian The cited results seem to provide a definitive answer for coherent theories, at least regarding the title question. Thanks! Are you familiar enough with the proofs to say whether the methods extend to (infinitary) geometric logic? | |
| Apr 29, 2014 at 14:04 | comment | added | godelian | Eduardo, I think you're confusing two issues here. One is the conservativity result of Barr's theorem, which has a classical topos-theoretic proof, and another whether that result can be established in a constructive metatheory. Also I don't understand your last sentence, "...since we accept the conclusion as true without requiring any other proof" | |
| Apr 29, 2014 at 13:55 | comment | added | Eduardo J. Dubuc | So, for example, if we want to prove that the validity of some equation follows from the validity of other equations in the real interval [0, 1] (equations in any geometric language interpretable in [0, 1]), then we can proceed by cases, for example, (x = 1) or (not x = 1). Even though that [0, 1] is not decidable. So this proof using classical logic which is not valid intuitionistically will in practice be accepted as a proof in the internal language of any topos, since we accept the conclusion as true without requiring any other proof. – | |
| Apr 29, 2014 at 13:49 | comment | added | godelian | 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) | |
| Apr 29, 2014 at 13:31 | comment | added | Zhen Lin | 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. | |
| Apr 29, 2014 at 13:20 | comment | added | godelian | 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. | |
| Apr 29, 2014 at 12:23 | answer | added | user44143 | timeline score: 7 | |
| Apr 29, 2014 at 8:31 | history | asked | Zhen Lin | CC BY-SA 3.0 |