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?



Does any lower bound on proofs of FLT improve Shepherdson 1965?
[Leszek Kołodziejczyk](http://dx.doi.org/10.1016/j.apal.2011.06.003) 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.


