Timeline for $f_{\epsilon_0}$ and provably total functions in $PA$
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 25, 2017 at 13:56 | vote | accept | Eric | ||
| Feb 25, 2017 at 13:52 | comment | added | Henry Towsner | @Eric: if you have another question, it's better to ask it separately. The standard representation of the functions f_alpha are provably total in PA. A trace of the computations in the standard description of f_alpha gives a descending sequence below alpha*omega. One then shows that PA proves this ordinal is well-founder. By choosing a very weird fundamental sequence (say, omega[n]=f_epsilon_0(n)), one changes the function and can get one not probably total in PA. | |
| Feb 25, 2017 at 13:44 | comment | added | Eric | Thank you for the clear answer. Please have a look at my edit of the original question. | |
| Feb 25, 2017 at 12:17 | history | answered | Henry Towsner | CC BY-SA 3.0 |