Timeline for Precise relationship between elementary and Grothendieck toposes?
Current License: CC BY-SA 3.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 30, 2017 at 18:19 | comment | added | aws | I don't know a reference for it, but after thinking some more, I think it should be fairly straightforward to prove. In Grothendieck toposes the n.n.o. is just the coproduct of $\mathbb{N}$ copies of $1$ with "standard" zero and successor. So if $\forall n\,\phi(n)$ is a true $\Pi^0_1$, it suffices to show for every $n$, $\phi(\bar{n})$ holds (with $\bar{n}$ the $n$th successor of zero). But this holds in general when $\phi(\bar{n})$ is true and primitive recursive. | |
| May 30, 2017 at 15:06 | comment | added | user71137 | Thanks, especially for the observation about $\Pi^0_1$ sentences. Do you have a source for that claim? I think I agree after playing around with it, but I'm not super confident in my work. | |
| May 29, 2017 at 10:14 | history | answered | aws | CC BY-SA 3.0 |