Has Ribet's theorem been proved using only finite powers of primes?

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.

This is a partial answer regarding the use of the use of the absolute Galois group of the rationals. In our paper Reverse Mathematics and Algebraic Field Extensions, Jeff Hirst, Paul Shafer and I analyze what is needed to have Galois theory of infinite extensions work as expected in the context of subsystems of second-order arithmetic. At no point do we need more than ACA0 to make things work as expected. (And when the ground field is $\mathbb{Q}$ we can often get by with a lot less.) Since ACA0 is conservative over PA, the use of the absolute Galois group of $\mathbb{Q}$ can always be eliminated in a proof of a purely first-order statement, so long as nothing is used that doesn't go through in ACA0. Since we haven't looked at the entire body of results in infinite Galois theory, we can't guarantee that the use of Galois theory that Ribet does can be eliminated. However, we would be very happy to look at any snag that you bump into while verifying this.
• Yes, I like that paper. Ribet's use of the absolute Galois group is particularly simple and I expect it can be eliminated almost by inspection. His use of $p$-adics is not so simple. I do not even see how to address it without really getting into the specifics of the proof. I'm hoping someone knows a faster way. Aug 23 '13 at 20:03