You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Fawzi Hreiki (Jan 03 2021 at 14:36):As far as I know, primitive recursive arithmetic can be characterised as the initial category with finite products containing a parametrised NNO. Likewise, Godel's System T is the initial cartesian closed category containing a NNO. We can say these things because the respective doctrines are essentially algebraic.
Is it also true that Heyting (resp. Peano) arithmetic is the initial Heyting (resp. Boolean) category with a parametrised NNO? Also, can anything similar be said about second-order arithmetic?
Fawzi Hreiki (Jan 03 2021 at 14:39):There isn't really anything out there about the categorical semantics of second-order logic. My first guess would be that, like first-order theories are indexed posets with quantifiers to substitution, second-order theories should be indexed first-order hyperdoctrines.
John Baez (Jan 03 2021 at 21:52):Those are fun questions! I can't help you with them, but I hope someone tells us some answers.
Martti Karvonen (Jan 06 2021 at 14:31):Maybe a bit orthogonal to your question (and/or telling you things you already know), but one can ask which functions on naturals are representable given a NNO + some further structure. Afaik, in a monoidal category a NNO gives all primitive recursive functions, and under suitable conditions you get all partial recursive functions (aka computable functions. See these slides by Phil Scott http://www.site.uottawa.ca/%7Ephil/papers/Lambekfest2.pdf and/or this paper by Gordon Plotkin for more https://link.springer.com/chapter/10.1007/978-3-642-38164-5_21