# Does any lower bound on proofs of FLT improve Shepherdson 1965?

In 1965 Shepherdson proved that FLT is independent of the fragment of PA that uses only open induction and signature $0,S,+\times$. Indeed $2x+1\neq 2y$ is independent of that fragment. Schmerl gives a good general criterion for independence from that fragment in Diophantine equations in a fragment of number theory'' in the book Computation and Proof Theory, Springer Lecture Notes in Mathematics Volume 1104, 1984, pp 389-398.

Is FLT currently known to be independent of any larger fragment of PA?

-
I'll mention Hajek and Pudlak in Metamathematics of First-Order Arithmetic (1998) discuss Shepherdson's result without saying his independence results in 1965 extend to any larger fragment. Rather, they say Shepherdson's technique here is so different from the techniques for stronger fragments that they will not go into it. –  Colin McLarty Apr 14 '13 at 11:22
The L in FLT means Little or Last? –  Emil Jeřábek Apr 16 '13 at 11:59
Last. I had never seen FLT used to mean Fermat's Little Theorem until you put me on the track of it and I found a cryptography oriented website acunix.wheatonma.edu/bbloch/crypto/… using it that way. –  Colin McLarty Apr 16 '13 at 12:44

Leszek Kołodziejczyk has devised a method how to extend some type of Shepherdson-like models of IOpen into models of Buss’s theory $T^0_2$ (a weak subsystem of $I\Delta_0+\Omega_1$). In particular, he has shown that $T^0_2$ does not prove that $x^3+y^3=z^3$ has no nontrivial solution.

-
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$). –  Emil Jeřábek Apr 16 '13 at 16:00
$T^0_2$ does include Robinson's $Q$, right? Specifically, it includes $x=0\vee \exists y(x=Sy)$? –  Colin McLarty Apr 16 '13 at 21:11
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. –  Emil Jeřábek Apr 22 '13 at 11:25