Timeline for Defining computable functions categorically
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 17, 2018 at 17:00 | comment | added | Mike Shulman | Ah, that's what I was asking. So what you had originally wasn't wrong, but the emphasis was (to me) misleading: it's not the Peano-ness of the axioms that's wrong but their first-order nature. The NNO in a topos is characterized by the second-order Peano axioms, but not by the first-order ones. And maybe you can't even express the second-order Peano axioms in assemblies (as opposed to the whole realizability topos) because you don't have a truth-value object to quantify over? | |
| May 17, 2018 at 6:31 | comment | added | Andrej Bauer | Yes, I am still wondering what Mike had in mind. @MikeShulman, how precisely would show that all models of PA are isomorphic? (Note that you can only apply induction of formulas expressible in the language of PA, and these cannot refer to objects in the topos.) | |
| May 17, 2018 at 5:06 | comment | added | David Roberts♦ | The second-order Peano axioms, at least. | |
| May 17, 2018 at 4:59 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 127 characters in body
|
| May 17, 2018 at 4:56 | comment | added | Andrej Bauer | Ah good, I wasn’t sure of the top of my head. I edited the answer. | |
| May 16, 2018 at 17:19 | comment | added | Mike Shulman | I'm pretty sure the NNO in a topos is also characterized by the Peano axioms. Are you saying that the Peano axioms are wrong because assemblies aren't a topos, or maybe because the relevant Peano axioms are second-order or something? | |
| May 16, 2018 at 16:43 | history | answered | Andrej Bauer | CC BY-SA 4.0 |