Timeline for Radix notation and toposes
Current License: CC BY-SA 2.5
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 15, 2016 at 6:31 | comment | added | Mike Shulman | LLPO, however, does appear to hold in Johnstone's topological topos. | |
| Jul 27, 2015 at 5:06 | comment | added | Mike Shulman | ...moreover, $\mathbb{N}+1$ includes into $\mathbb{N}_\infty$ as the sequences that are 1 at at some known place or constantly 0, and the localization at this inclusion is equivalent to Set. So "once you force LPO to hold, you get all of classical logic." | |
| Jul 27, 2015 at 5:06 | comment | added | Mike Shulman | @DavidFeldman, I would say there's some sense in which Johnstone's topological topos (ncatlab.org/nlab/show/Johnstone%27s+topological+topos) is a "canonical" one where LPO fails. It's generated by the one-point compactification $\mathbb{N}_\infty$ of $\mathbb{N}$, which can be defined internally to it as "the set of nondecreasing binary sequences", and maps out of that object detect all the "topology" of other objects. [cont.] | |
| Dec 20, 2010 at 4:58 | comment | added | Daniel Mehkeri | On reflection I was reading "isomorphism between numeral systems of various radix" WITHOUT taking a quotient as mentioned by Peter in the comments to Andrej's answer. If you take this quotient (and this seems more reasonable) then I think (I'm less sure) it's still true that any non-trivial isomorphism implies all of them, but the principle is LLPO (ncatlab.org/nlab/show/principle+of+omniscience) rather than LPO and countable choice may be involved. The effective topos still violates LLPO and satifies countable choice. | |
| Dec 19, 2010 at 21:40 | comment | added | Daniel Mehkeri | The extrapolation is mine but the basic stuff on decimal expansions goes back to Brouwer, and is repeated in many introductory texts on constructive mathematics, such as Bishop's Foundations of Constructive Analysis, which is also I think where the name LPO is introduced. The effective topos violates LPO, but I don't know if it's the best/canonical example of that. | |
| Dec 19, 2010 at 21:15 | comment | added | David Feldman | Since my last comment, I have found this (useful): zianet.com/k5am/math/mandelkern-bwp.pdf | |
| Dec 19, 2010 at 20:30 | comment | added | David Feldman | @Daniel. Terrific - is this your own thinking or do you have a reference? (I often teach future teachers, so I collect material on elementary mathematics from an advanced viewpoint). Can you offer a canonical example of a topos where where LPO fails? | |
| Dec 19, 2010 at 20:26 | vote | accept | David Feldman | ||
| Dec 19, 2010 at 19:49 | history | answered | Daniel Mehkeri | CC BY-SA 2.5 |