Nice quote-worthy answers and questions from MathOverflow every Tuesday!
If you like, you can view proofs of a statement in some formal system (e.g. ZFC) as a certificate that a counterexample cannot be found without demonstrating the inconsistency of ZFC, which would be a major mathematical event, and probably one of far greater significance than whether one’s given statement was true or false.
In practice, a given proof is not going to be closely tied to a single formal system such as ZFC, but will be robust enough that it can follow from any number of reasonable sets of axioms, including those much weaker than ZFC. Only one of these sets of axioms then needs to be consistent in order to guarantee that no counterexample would ever be found, and this is about as close to an ironclad guarantee as one can ever hope for.
But ultimately, mathematicians are not really after proofs, despite appearances; they are afterunderstanding. This is discussed quite well in Thurston’s article “On proof and progress in mathematics“.
Gödel’s theorems do not say that we can never know our axiom systems are consistent. Not at all. What they say is that we can never prove that certain systems are consistent within those systems themselves. This leaves open the possibility that we can prove their consistency in other axiom systems, or can convince ourselves of their consistency by methods that are not completely formal.
My recommended reference on the incompleteness theorems for a general reader is “Gödel’s Theorem: An Incomplete Guide to its Use and Abuse” by Torkel Franzén. This book has the rare combination of being written to be broadly accessible while still being precise enough to be satisfying.
To address the issue of Fermat’s Last Theorem: the reasoning behind Fermat’s Last Theorem, while elaborate, in the end rests on basic intuition about the integers. (I’m not sure that it is actually proved in first order Peano arithmetic, since the proof as written certainly uses concepts outside of PA, but nevertheless, it is basically a result about numbers, proved using our fundamental notions about numbers.)
If the proof was correct, but the statement wrong (due to an inconsistency), there would be something fundamentally wrong in our conception of numbers. I don’t think this would be like the crisis in set-theory: it would be much more fundamental. For example, if induction turns out to be inconsistent (and this is the kind of thing being speculated about here), this says that our basic intuition for the natural numbers, namely that non-empty subsets have least elements, is wrong. If that is true, then all mathematics goes out the window!
I think that most mathematicians (indeed, most humans who have been taught arithmetic) have a mental model of the natural numbers which says that you can always add 1 to get a new number, and that between any two natural numbers there are only finitely many more (so that any non-empty subset of the naturals has a least element). Given this, they know that PA is in fact consistent, even though PA doesn’t prove this. They are proving it by exhibiting a (mental) model; they don’t need formal arguments. (This falls under the class of “not completely formal” methods alluded to by Carl Mummert.)
I think many mathematicians go with Carl’s “convince ourselves of their consistency by methods that are not completely formal.” Many mathematicians use set theory simply as a language–probably similar sorts of mathematicians as do not concern themselves with categories too much, of which type there are still many. Mathematicians with a physics bent often enjoy “informal” arguments based on physical intuition, a mechanical construction, or the nonrigorous arguments of Archimedes or Appolonius or Cavalieri using a primitive version of infinitesimals to compute volumes, etc. The insight gained from less formal arguments, while less definitive, perhaps, probably outweighs the worries about set-theoretic and proof-theoretic issues for many mathematicians. (A graph theorist, for example, could be perfectly happy proving results for classes of graphs and graph properties for their whole career, knowing that the results are true for graphs the way one usually pictures them, without worrying about the consistency of ZFC).
Since your question is part mathematical logic and part psychology (whether people “worry”), may I suggest some of the literature on pedagogy for higher mathematics? Many people have thought a lot about how to treat the concept of proof and other issues in courses for various sorts of students in order to maximize the understanding and value gained. See, for example, David Henderson’s work on “educational mathematics” at Cornell.
A proof is valuable because it helps convince oneself and others of the validity of that result from the axioms [whether those axioms are consistent or not]. Mathematicians, I believe, are not worried that the axioms are inconsistent, but rather hopeful that they are consistent; or even more precisely, optimistic that if the axioms are inconsistent they can be modified [if necessary] to be consistent and still encompass most things proved. But even if they are inconsistent, we won’t figure that out without lots and lots of proofs in the meantime.
To answer the philosophical question from a personal point of view:
From my point of view, I do mathematics because I love certainty and truth. I also enjoy discovery. Godel’s theorems simply tell me that there are some things I will never be certain of or discover (inside a formal system). This may be disappointing, but at some level we all have to deal with uncertainty. For example, I could be deceiving myself that I’m typing this message. But I (and most others I know) are willing to accept a few things on faith; and if shown we are wrong, modify our beliefs accordingly.
We adopt axioms not because we can prove their consistency, but because we believe that they accurately describe something that we want to study. A proof from these axioms will have value in that it shows how the proposition (which may be surprising or complicated) follows from things that we already believe and are simple. If we someday prove an inconsistency using a given set of axioms, this shows that our possibly naïve intuition for reasonable axioms was incorrect. (e.g. Russel’s paradox showing that unrestricted comprehension is a bad idea)