Timeline for Goodstein's theorem without transfinite induction
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 25, 2023 at 23:43 | comment | added | Piotr Hajlasz | Perhaps this post is relevant: mathoverflow.net/q/354551/121665. | |
| S Oct 25, 2023 at 23:01 | history | suggested | The Amplitwist | CC BY-SA 4.0 |
fixed broken link to Wikipedia; replaced broken link to www.math.niu.edu with WebArchive snapshot
|
| Oct 25, 2023 at 21:29 | review | Suggested edits | |||
| S Oct 25, 2023 at 23:01 | |||||
| Jun 28, 2013 at 12:08 | comment | added | François G. Dorais | I'm out of the office so I can't check but Google books tells me there are four matches for "Goodstein" in the book (one of which is in the index). So I think it's worth a trip to the library. | |
| Jun 25, 2013 at 18:39 | comment | added | Lucas K. | I have been thinking how exactly the second order proof goes. One should prove that if the exponents follow a well ordered relation, then the newly created relation is also well ordered. Which such proof, you can then do induction on the height of the exponent tower. Because, we are quantifying over all well ordered relations, this is a second order proof. In case of meta-logic (using Constructive omega rule), the quantification is on syntactical level. | |
| Jun 24, 2013 at 18:26 | comment | added | François G. Dorais | Interesting! Have you checked Franzen's Inexhaustibility book? Sounds like this is a concrete way to see that $ACA_0$ with $\Sigma^1_1$-induction is not conservative over $PA$. | |
| Jun 24, 2013 at 18:09 | comment | added | Lucas K. | Note, that Goodstein can be proven in second order logic. So, if the sets are defined by predicates and you allow quantification over it, you have effectively a second order system. The proof in such system might however become close to the transfinite proof. | |
| Jun 24, 2013 at 17:45 | answer | added | Lucas K. | timeline score: 5 | |
| Jun 24, 2013 at 7:03 | history | asked | user10891 | CC BY-SA 3.0 |