Ribet proved the Serre epsilon conjecture using $p$-adic Galois representations (http://math.berkeley.edu/~ribet/Articles/invent_100.pdf). Can someone show how to replace all use of $p$-adics in this (or some other) proof of the theorem by arithmetic modulo some finite number of specified powers?
A word on the motivation: To actually find a proof of Fermat's Last Theorem in Peano Arithmetic would require eliminating $p$-adics from the proof, along with absolute Galois groups, and cohomological tools (all of which are un-interpretable in Peano Arithmetic), I expect that will be done someday. In fact I expect the absolute Galois groups can be easily removed in favor of Galois groups of specified number fields, given the particular way they serve in the existing proofs. This question looks toward removing $p$-adics from the proof of Ribet's theorem, which may not be easy at all.
Merely to show there is a PA proof of FLT, though, does not require eliminating any of these. The promising strategy for that today is to use $\mathsf{ACA}_0$ as in François's comment. In effect, you use numbers and sets of numbers but all sets of numbers must be defined by referring only to numbers and not also to sets of them. Large parts of Ribet's proof are already like that. It remains to check the whole in detail. While there is a good routine for turning $\mathsf{ACA}_)$ proofs of arithmetic statements into PA proofs, it seems unlikely to me that this route could lead to a humanly comprehensible PA proof.
Currently it seems that getting the Modularity Thesis into PA will be a substantially larger project.