Timeline for Barr's theorem and constructivity?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 26, 2013 at 17:58 | comment | added | Andreas Blass | Consider a nondegenerate but non-Boolean Grothendieck topos $E$. Diaconescu's proof that AC implies excluded middle can be used to show that an internal version of choice fails in $E$. (More precisely, one can give an object $A$ such that the internal sentence "for every equivalence relation on $A$, the map from $A$ to the quotient has a section" is false.) So in $E$, from any set (even the empty set) of geometric hypotheses plus AC one can deduce anything, even the geometric conclusion "false", because AC fails. That inference won't work constructively. | |
| Sep 26, 2013 at 16:28 | comment | added | Zhen Lin | @SimonHenry That is a very different question than your original question! But the "logical form of Barr's theorem" is not obviously true in the internal logic of even a Grothendieck topos – for one thing, a topos that is "internally localic" may not actually be localic. | |
| Sep 26, 2013 at 14:45 | comment | added | Simon Henry | Yes that's what I mean. What I call the logical form of Barr's theorem is "If from a family of geometric hypothesis I can deduce a geometric conclusion using the axiom of choice then I can deduce it also constructively". This theorem hold internally in any Grothendeick topos. But one generally said that it is non-constructive, I want a proof of this non-constructivity by a counterexample in a topos (which has to be elementary.) | |
| Sep 26, 2013 at 14:08 | comment | added | Andreas Blass | Does the edit mean that you want to allow $H$ and $C$ to be in a language internal to an elementary topos $E$, and that the infinitary disjunctions of geometric logic can be indexed by objects of $E$, and that the "set" $H$ itself might not be a "real" set but an object of $E$, and that deducibility is to be interpreted internally in $E$? Or only some of these? "Deducible using the axiom of choice" looks suspicous in $E$ if $E$ doesn't satisfy the (internal) AC. Did you perhaps want the deducibility to work also in all topoi defined over $E$? | |
| Sep 26, 2013 at 13:57 | comment | added | Zhen Lin | You've misunderstood: the completeness theorem I'm referring to is the one that says that any coherent sequent in a coherent theory that is true in all Grothendieck toposes can also be proved using the rules of inference of coherent logic. In particular it is valid in elementary toposes. | |
| Sep 26, 2013 at 12:56 | history | edited | Simon Henry | CC BY-SA 3.0 |
added 701 characters in body
|
| Sep 15, 2013 at 16:18 | answer | added | Zhen Lin | timeline score: 6 | |
| Sep 15, 2013 at 14:18 | history | asked | Simon Henry | CC BY-SA 3.0 |