Timeline for Categories of recursive functions
Current License: CC BY-SA 3.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 23, 2020 at 20:41 | answer | added | Todd Trimble | timeline score: 8 | |
| Apr 10, 2013 at 18:57 | answer | added | Paul Taylor | timeline score: 6 | |
| Apr 9, 2013 at 16:08 | vote | accept | Wouter Stekelenburg | ||
| Apr 7, 2013 at 15:28 | answer | added | Paul Taylor | timeline score: 33 | |
| Apr 5, 2013 at 7:04 | comment | added | Wouter Stekelenburg | @Francois: I assume regular categories have finite limits. The definition of NNO is in the question, but 'parametrized' sounds like a good description. | |
| Apr 4, 2013 at 16:48 | comment | added | François G. Dorais | So for 2, you're just looking at a regular category with finite limits (or just products?) and a parametrized nno? (Disjoint coproducts too?) | |
| Apr 4, 2013 at 16:46 | comment | added | François G. Dorais | No, a nonstandard Gödel code doesn't give a proof in any reasonable sense. | |
| Apr 4, 2013 at 16:45 | comment | added | Noah Schweber | @Wouter: If I understand what you're asking, the answer is no: assuming $PA$ is consistent, there are models of $PA$ (hence, satisfying $0\not=1$) which contain internal "proofs" that 0=1. | |
| Apr 4, 2013 at 16:43 | history | edited | Wouter Stekelenburg | CC BY-SA 3.0 |
spelling
|
| Apr 4, 2013 at 16:42 | comment | added | Wouter Stekelenburg | @Francois: in a regular category, a partial function $X\rightharpoonup Y$ is an isomorphism class of spans $(m:Z\to X, f:Z\to Y)$ where $m$ is monic. If a non standard model forces that $0=1$ is provable, doesn't it automatically force $0=1$? | |
| Apr 4, 2013 at 15:18 | comment | added | François G. Dorais | Unless you insist on well-pointed categories, there are usually no major issues using intensional equality instead of extensional equality. | |
| Apr 4, 2013 at 15:04 | comment | added | François G. Dorais | I think 1 is also sensitive to formalization, but not as much. The problem is not that functions can be omitted but that they can be accidentally identified. For example, there is a p.r. function $c$ such that $c(x) = 0$ unless $x$ is a Gödel code of a PA-proof of $0=1$, in which case $c(x)=1$. In the standard model, $c$ is the identically $0$ function. If these are actually the same in your category, then it is not initial since there are models where $c$ is not identically $0$. However, this is can be fixed using intensional equality instead of extensional equality. | |
| Apr 4, 2013 at 14:55 | comment | added | François G. Dorais | I'm curious how you formalize partial functions in 2. | |
| Apr 4, 2013 at 13:37 | history | asked | Wouter Stekelenburg | CC BY-SA 3.0 |