Theorems which say "such and such method cannot possibly prove FLT" After a previous question that I asked https://mathoverflow.net/questions/31565/request-for-comments-about-a-claimed-simple-proof-of-flt-closed was closed, someone suggested in the comments that I ask another question that is more suited for MO. That question is as follows:
Are there any nontrivial theorems of the form "Method X cannot possibly prove FLT."? 
The reason I am asking is because I'd like to know (by deductive reasoning and not relying on 350 years experience) if it is impossible to prove FLT using elementary methods.
 A: There is also the relative approach, which is to show that making Method X work is at least as difficult as solving some set of known hard problems, due to relatively simple reductions between the problems.  This is what has been done for the P=NP problem --- thousands of NP problems are computationally equivalent to each other --- as well as the Riemann Hypothesis which has a large number of known equivalents.  If you had the bright idea of replacing the non-elementary Riemann zeta function and statements about its zeroes by statements about the distribution of primes, or sums of the Moebius function, then the translation between those contexts is known and much easier than the theory of the zeta function itself, so there would have to be some elementary idea that people had missed in each and every one of those equivalent environments. 
For example, if Method X = "prove an effective form of the ABC conjecture" (the non-effective form implies FLT for large exponents using a few lines of algebra), then solutions of dozens of hard unsolved problems, and easier proofs of very hard theorems, would be assured as soon as one could carry out Method X.  Because the reductions of these problems to the ABC conjecture are often quite simple, any elementary idea used to carry forward Method X would immediately translate into elementary methods for the dozens of other problems, and it is less likely that nobody would have ever noticed this in any of the other actively studied problems. 
A: You may find it of interest to peruse the very readable introduction in the following paper. It explains briefly what's known about obstructions to a local-global principle for the generalized Fermat equation.
H. Darmon, A. Granville,
On the equations $z^m = F(x, y)$ and $A x^p + B y^q = C z^r$.
Bull. London Math. Soc. 27 (1995), 513–543.
http://blms.oxfordjournals.org/cgi/content/short/27/6/513
A: For a while at the end of undergrad and beginning of graduate school I made some money correcting an enthusiastic amateur mathematician's incorrect proofs of FLT.  (It was a good experience, he was an academic in another field so was professional and was willing to pay what my time was worth.)  When I first read his argument I tried to convince him why the method was doomed to failure.  He wasn't interested in trying to understand that, but maybe it'll still be informative here.
His method of proof was to consider the "even-ness" (that is the highest power of 2 which is a factor) each side of the equation.  He would then do ever more esoteric changes of variables until he inevitably misapplied the tricky part of the non-archimedian triangle inequality (i.e. if 4 divides x and 4 divides y then you have no idea what the "even-ness" is of x+y).  At that point he got a contradiction.
Now why is this doomed to failure?  Well any reasonable argument along those lines would apply to the 2-adic integers.  However, if p is an odd prime, then the power series for the pth root converges 2-adically.  So every 2-adic integer is a pth power, so certainly the Fermat equation has loads of nontrivial 2-adic integer solutions.
A: According to the review of the paper 
MR2006194 
Avigad, Jeremy
Number theory and elementary arithmetic.
Philos. Math. (3) 11 (2003), no. 3, 257--284
Harvey Friedman (who is the expert on these sorts of questions) has conjectured that FLT is provable in elementary function arithmetic, a very weak form of arithmetic that contains addition, multiplication, exponentiation, and some rather weak form of induction. A proof in this theory would elementary in almost any reasonable sense of the word "elementary", but presumably rather long. 
A: The motivation "because I'd like to know [...] if it is impossible to prove FLT using elementary methods" seems to require comment. It is much more likely (in my view) that it is true that FLT can be proved by technically elementary methods, but that the proof is the sort that should never be printed out (to save trees) and is entirely unreadable and useless to humans. 
This kind of discussion has been going on, in a smouldering way, in proof theory, for half a century and more. There is some sort of "compilation" that is possible, and it has been called "proof unwinding", to replace the use of high-order concepts by more elementary ones, showing that the higher-order ones are substantively "only" abbreviations. Well, it is anyway a more healthy view for a mathematician, I believe, to welcome the abbreviating power of concepts.
So I'm not commenting on whether this has been done or is likely or possible to do. I'm really trying to make a point such as: FLT is not like circle-squaring where one can confidently say that a circle-squarer is a crank. An "elementary proof of FLT" is probably not an impossible object. It perhaps is a too-ghastly-to-contemplate object. But we are unlikely to be sure (ever) that some slick simplification doesn't exist. I think this sort of discussion is required to put into context the other answers; and it is much more treacherous ground than the remarks that congruences don't suffice.
A: Ruling out Method X is generally much harder than Method X itself, so one shouldn't necessarily expect that for any method that won't work a "certificate" can be found establishing its insufficiency.  With that said:
There are plenty of environments (rings) where the algebraic equation in FLT makes sense, but has solutions.  If the ingredients of Method X apply in one such environment, they aren't using specific enough properties of the integers to prove FLT.  It is well known that if Method X = congruences (reduction modulo $t$ for different values of $t$), then this argument works in rings of $p$-adic numbers where FLT has solutions.   Similarly, if Method X = inequalities, then it would have to rule out the positive real solutions of $x^n + y^n = z^n$.  
Another possibility, requiring much more knowledge, would be to use the close relations between FLT and elliptic curves (Frey, Wiles, etc) to project method X onto the canvas of Wiles' proof and see how much of it can be understood and delimited in those terms.  It could be that X is in effect trying to construct nontrivial objects of a certain kind (esp. cohomology classes) and one can see in light of Wiles methods that the relevant classes are zero, necessary field extensions or coverings are trivial, important obstructions are not killed, etc.  This approach stays within environments where FLT is true, but tries to subsume Method X within existing lines of attack, and show that it only includes a part of what is needed.
Another idea is "reverse mathematics", to represent Method X as formal derivations in some weak system Y of arithmetic, and show that FLT is of higher proof theoretic strength (because it implies all the theorems of an even stronger system Z).  This is unlikely because FLT is too specialized a statement and the proof-theoretic calibrations of strength only work for reasonably generic theorems with a lot of parameters that can be varied.
EDIT:  I should add that each of these approaches has been pursued for showing that the P=NP problem doesn't have elementary solutions.   The Baker-Gill-Solovay theorem demonstrated that environments (oracles) exist where P=NP has a different answer but simple methods of proof would continue to work.  The Razborov-Rudich "natural proofs" paper showed that any proof sharing certain features of all the arguments then known (for proving lower bounds on circuit complexity) couldn't produce bounds growing faster than any polynomial.  And there are weak formal systems whose most general class of definable languages or constructible functions is exactly P or NP; Stephen Cook himself has many papers on the logic/formal-systems approach to P=NP.
