Timeline for Proof of Tennenbaum's Theorem by McCarty
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 10, 2021 at 19:48 | history | edited | Léreau | CC BY-SA 4.0 |
small edit suggested by comment
|
| Apr 10, 2021 at 19:47 | comment | added | Léreau | @FrançoisG.Dorais You are indeed correct, CT should definitely not be left out. | |
| Apr 10, 2021 at 19:25 | comment | added | François G. Dorais | "HA categorial" in the last paragraph should be "HA + CT categorical". This result is indeed well worth mentioning but this is really just a different reading of Tennenbaum's Theorem. | |
| Apr 10, 2021 at 6:30 | history | edited | Léreau | CC BY-SA 4.0 |
small clarification due to a comment
|
| Apr 10, 2021 at 6:25 | comment | added | Léreau | @MattF. The equivalence is indeed a theorem. The bullet points derived $\neg \exists a \in M \neg \mathsf{std}(a)$. I edited to text to clarify this. | |
| Apr 8, 2021 at 15:04 | comment | added | Léreau | @AndrejBauer I am refering to the embeding $i : \mathbb{N} \rightarrow X$ used in (Proof of Th.0.1 of) the paper Arithmetic is Categorical linked by Ingo Blechschmidt. | |
| Apr 8, 2021 at 14:13 | comment | added | Andrej Bauer | @Lereau: what is $i$ in your second comment above? | |
| Apr 8, 2021 at 11:52 | history | edited | gmvh |
Added top-level tag
|
|
| Apr 8, 2021 at 11:05 | history | edited | Léreau | CC BY-SA 4.0 |
A few text and TeX edits
|
| Apr 3, 2021 at 16:43 | comment | added | Léreau | @IngoBlechschmidt I guess what I am asking with my post (and maybe I should make this explicit) is: Why is this result not more widely known? It was published before the article of e.g. Smith and was not mentioned there. But the head news "HA is categorial" seems so notable, even if this is only the case in constructive logic which might still be a bit niche. I'm kind of looking for reassurance on the result. | |
| Apr 3, 2021 at 16:42 | comment | added | Léreau | @IngoBlechschmidt You are welcome! I actually stumbled on that one when looking through the papers that cited McCarty and it is indeed interesting, especially the corollary! Unfortunately I don't know enough about the effective topos to grasp the result and the parallels completely. For example my gut is telling me that the part of the proof showing that $i$ embeds $N$ as a $\neg \neg$ subobject corresponds to showing $\forall a : \neg \neg \operatorname{std}(e)$, but I am not sure about that. | |
| Apr 3, 2021 at 15:51 | comment | added | Ingo Blechschmidt | Welcome to MO, Lereau! Thank you for the apt summary of the proof, and for bringing paper (2) to my attention. A further very nice related paper is Arithmetic is Categorical by Benno van den Berg and Jaap van Oosten. But can you clarify what exactly you are asking? :-) | |
| Apr 3, 2021 at 13:00 | history | edited | Léreau | CC BY-SA 4.0 |
corrected mistake
|
| Apr 2, 2021 at 15:12 | review | First posts | |||
| Apr 2, 2021 at 15:22 | |||||
| Apr 2, 2021 at 15:07 | history | asked | Léreau | CC BY-SA 4.0 |