Timeline for Does any lower bound on proofs of FLT improve Shepherdson 1965?
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 22, 2013 at 11:25 | comment | added | Emil Jeřábek | Yes. This is provable by open (and therefore $\Sigma^b_0$) induction: if $x$ is neither $0$ nor a successor, we can prove $y\ne x$ for every $y$ by induction on $y$, and taking $y=x$ gives a contradiction. | |
| Apr 16, 2013 at 21:11 | comment | added | Colin McLarty | $T^0_2$ does include Robinson's $Q$, right? Specifically, it includes $x=0\vee \exists y(x=Sy)$? | |
| Apr 16, 2013 at 17:53 | vote | accept | Colin McLarty | ||
| Apr 16, 2013 at 16:00 | comment | added | Emil Jeřábek | In light of the other answer, I should probably stress that $T^0_2$ is not a weak theory when it comes to Tennenbaum phenomena: it has no recursive nonstandard models, and in fact, every nonstandard countable model of $T^0_2$ has a nonstandard cut that is a model of PA. While the theory shows signs of pathological weakness (by Leszek’s results, it can’t prove that a power of $2$ is not divisible by $3$), the slightly stronger theory $T^0_2(\lfloor x/2^y\rfloor)$ is quite well-behaved, it can define all polynomial-time functions and prove induction for them (it is equivalent to $PV_1$). | |
| Apr 16, 2013 at 13:46 | history | answered | Emil Jeřábek | CC BY-SA 3.0 |