Timeline for Ackermann function in the Primitive recursive arithmetic
Current License: CC BY-SA 2.5
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 31, 2010 at 10:37 | vote | accept | Dan | ||
| Aug 11, 2010 at 23:34 | comment | added | Carl Mummert | Good point - in general you have to take a "natural" index for the computable function you want to prove is total. Of course you also have to take a "natural" primitive recursive index for the $T$ predicate, or it might be that your theory can't prove any computable function is total. It's an endemic problem with formalization. | |
| Aug 11, 2010 at 20:01 | comment | added | Andreas Blass |
Different indices $e$ for the same function might lead to different formulations $(\forall n)(\exists t)T(e,n,t)$ of totality. Carl's answer is fine because, for the Ackermann function, no choice of $e$ will make totality provable in PRA. But for other functions, you could have two indices of the same function such that totality for one is provable in PRA while totality for the other is not provable even in ZFC. (In fact, the constant zero function has two such indices.)
|
|
| Aug 11, 2010 at 12:56 | history | answered | Carl Mummert | CC BY-SA 2.5 |