Is consistency an axiom of mathematics?
Yes. That is exactly what it means. Consistency assumptions are axioms.
This gives rise to a natural hierarchy of axioms, specifically part of set theory, called large cardinal axioms which are stronger and stronger in consistency strength, and generally each one implies the weaker are consistent (and much more).
For example, the standard set theory, ZFC (Zermelo–Fraenkel with Choice) does not prove its own consistency strength, but we can add an axiom stating that it is in fact consistent. To that you can add an axiom that it is not only that ZFC is consistent, but "ZFC+ZFC is consistent" is also consistent. This can go on for a while.
But you can also just say that there are inaccessible cardinals, whatever they might be. This implies that ZFC is consistent, and much more. You can move to stating that there exists a weakly compact cardinal, which then implies that not only it is consistent that there is an inaccessible cardinals, but that it is consistent that every set is smaller in size from some inaccessible cardinal.
And the list continues.
Interestingly, though, while the large cardinal axioms are stating that some particular sets exists (or don't exist), consistency statements can be seen as axioms added to the theory of the natural numbers. So you can also investigate them from arithmetic theories such as PA or PRA, both of which are vastly weaker than ZFC.
Well, we must be careful about what 'mathematics' means here. We generally mean some kind of formal system (the things Godel's theorem talks about) capable of formalizing and proving theorems of interest. Certain kinds of mathematics require stronger systems than others, and thus are at a higher risk of being inconsistent.
Godel's theorem itself is about formal systems, which consist of strings of symbols that we manipulate syntactically to form and verify proofs. This is very simple reasoning at its core: a computer program can verify if something is a valid formal proof or not. As such, Godel's theorem can be talked about in very simple formal systems. In fact the system PRA (which is commonly associated with purely finitary reasoning) is sufficient to prove Godel's theorem$^*$.
In order for us to believe in the meaningfulness of Godel's theorem, we need to believe that PRA is a sound and consistent system. Fortunately, it's such a weak system, that almost everyone, even extreme skeptics, believe it is consistent. However, PRA is powerful enough arithmetically for Godel's theorem to apply to it, and thus we cannot prove the consistency of PRA in a weaker system than it. Ultimately, it must be assumed.
Remember, if you believe a system is correct (i.e. it talks about 'real' mathematical objects, whatever that means, and only proves true things about them) then you believe it is consistent. So if we believe in natural numbers - not the completed infinite set of natural numbers, just natural numbers - and that certain statements about natural numbers have meaning (namely, the quantifier free statements about primative recursive functions that PRA can talk about), and that PRA is a valid way about reasoning about them, then we believe PRA is consistent. As I said, this is something most people believe even at their most skeptical. (Though not universally.)
But not all math is a simple matter of string manipulation and finitary reasoning. Much of modern math requires thinking about infinite collections of objects. Traditionally, math has been considered to be founded on set theory, with the ZFC axioms and first order logic as our formal system of reasoning. This is a much stronger system then PRA. For instance, it easily proves that PRA is correct and consistent. There is nothing contradictory about this since it's stronger. And of course it's a strong enough arithmetically that Godel's theorem applies to it, so it cannot prove itself consistent.
So if we're taking 'mathematics' to be ZFC, then 'mathematics' (actually a very weak fragment of 'mathematics') proves Godel's incompleteness theorem, and thus 'mathematics' proves that it cannot prove itself to be consistent. Thus we will have to assume the consistency of ZFC if we want to take its proofs seriously (or, more exactly, whatever fragment of ZFC we use in the proofs).
So, basically, that's a big yes. We need to make assumptions about consistency, in order to do any math at all, and the more math we want to do the stronger assumptions we're going to need to make. (And see Asaf's excellent answer about just how far this goes and how precise this is.)
A few more comments.
- First, there's kind of a weird fixation on theories proving themselves consistent. Recall that it's a basic tenet of classical logic that if a system can prove an inconsistency, it can prove anything. So if you doubted the consistency of a system, why would you believe its proof that it's consistent? If it were inconsistent, it could prove that too. Really, the dream scenario would be something like PRA that's very weak with little philosophical commitment proving something very strong like ZFC to be consistent. Of course Godel dashes our hope here too: anything provable in the weaker system would be provable in the stronger system too. However, it wasn't an unreasonable request at the outset. Consistency is just a statement about syntactic manipulation of symbols, so it doesn't require a very sophisticated system to talk about. The consistency of ZFC is expressible in PRA, even if it's not provable there.
- Second, actually, ZFC can prove every finite fragment of ZFC is consistent. Thus with any ZFC proof (which must use only a finite number of axioms) we have a proof in ZFC that the axioms we used were consistent. This is not super comforting for the reasons stated in my previous comment. And what of the axioms we used in our proof that the finite fragment was consistent... were they consistent?
- Third, while Godel says we can't prove the consistency of a system from a weaker one, there's a famous loophole there. Peano arithmetic is a much-studied system of arithmetic that seems to delineate 'purely arithmetical' (as opposed to analytical, or set theoretical, etc) reasoning. It can be proven consistent in ZFC, but as I've emphasized, it's of little interest that set theory proves consistency if you're wondering if maybe something's fishy about arithmetic. However, Gentzen came up with a famous proof that uses mostly very weak finitary reasoning about formulas (just PRA, in fact, which is weaker than PA). However, it assumes that transfinite induction through the ordinal $\epsilon_0$ is valid. This is much less scary and infinitary than it probably sounds, but it's still something that can't be proven in PA, in accordance with Godel. So PA can be proven consistent in a system that's a lot weaker than PA in some ways, while being a little stronger in another.
- It is a logical possibility that ZFC is consistent, but it proves itself inconsistent. The key to understanding this is that a system can be consistent, but also be wrong. 'ZFC is inconsistent,' as represented in ZFC, is an arithmetical statement about the existence of a number that encodes the proof of a contradiction. So more precisely, ZFC would be arithmetically unsound... it would prove a number with a certain property exists that doesn't actually exist. What's more strange, whether a number is a proof of an inconsistency is a very simple computable property - so simple that ZFC is bound to get it right - so for any number you name, it would prove that it doesn't have that property (even though it proves there exists a number with that property!). This seeming, but not literal, inconsistency is called $\omega$-inconsistency. This would mean that ZFC (more precisely, all models of ZFC) does not actually have the natural numbers we know and love, but rather has a set of nonstandard integers. This is a structure that can't be distinguished from the natural numbers by first order logic, but consists of both the standard naturals and 'infinite' elements larger than all the naturals. The proof of ZFC's inconsistency would be one of these infinite numbers.
$^*$I'm not one hundred percent positive that PRA suffices for the incompleteness theorem as stated here. It's just what I've heard. In any event, it works in a very weak system, certainly much weaker than Peano Arithmetic.
Firstly, we cannot prove anything in a vacuum. Any theorem, such as Godel's incompleteness theorem, is proven in some formal system (often called the meta-system). As spaceisdarkgreen wrote in his answer, this particular theorem can be proven in very weak meta-systems. Take any formal system $S$ that has a proof verifier program and interprets PA. Then the incompleteness theorems just affirm that if $S$ is consistent then it is incomplete (first incompleteness theorem) and cannot even prove Con$(S)$, which is some arithmetical sentence that represents the consistency of $S$ (second incompleteness theorem). Godel had originally proved the first theorem where the "is consistent" condition is replaced by "is ω-consistent", but his proof essentially works for the stronger version where it is replaced by "is $Σ_1$-sound". Later Rosser strengthened it all the way to "is consistent", so it is called the Godel-Rosser incompleteness theorem. And some time later Kleene gave a computability-based proof (see here for the key ideas).
I wish to emphasize that the weak meta-system need not assume/stipulate that $S$ is consistent, since it only proves a conditional assertion. From outside the meta-system, we can observe that if we believe that $S$ is consistent (and we believe that the meta-system is correct) then we must also believe that $S$ is not complete and cannot prove its own consistency.
So the answers to your questions are:
It seems the key to accepting the truth of Gödel's Theorem is to demand that mathematics is consistent. [...]
No, as above. And hence the rest of your questions in that paragraph are based on an incorrect premise.
I've read elsewhere on here that another way to state Gödel's theorem is to say that no formal mathematics system can prove it's own consistency.
That is an incomplete gloss of the second incompleteness theorem. A more accurate gloss would be: No computable formal system that can prove whatever PA proves about the natural numbers can also prove its own consistency unless it is inconsistent.
Does that mean we just have to assume our system of mathematics is consistent?
When we do actual mathematics, we have to work in some foundational system FOM that can be formalized (namely has a proof verifier program). Now PA is considered by almost all mathematicians as indispensable, and so FOM will interpret PA (be able to prove whatever PA proves about $\mathbb{N}$). By the second incompleteness theorem, FOM cannot prove its own consistency. But if you work in FOM, you ought to believe that FOM is at least consistent. In other words, for you to believe that your mathematical work is meaningful you must believe that the arithmetical sentence Con(FOM) is a truth that FOM itself cannot prove.
Parenthetical remarks:
The incompleteness theorem applies to all possible formal systems that humans will ever conceive of, because formalization effectively means the existence of a proof verifier program. This includes formal systems that are not based on classical logic. You might then wonder what "$S$ is consistent" means. Replace it by "$S$ is arithmetically consistent", meaning "$S$ does not prove ( $0=1$ )".
It is true that very weak meta-systems can prove the incompleteness theorems. For example PA proves ( Con$(S)$ ⇒ ¬ Prov$_S($Con$(S))$ ), where "Prov$_S(Q)$" is some arithmetical sentence that encodes provability of $Q$ over $S$. The issue is that this arithmetical sentence can only be ascribed meaning in a meta-system MS that actually 'understands' provability. Concretely, MS needs to assume/stipulate the existence of a model of PA, which we call $\mathbb{N}$. Without that model, there is a disconnect between Con$(S)$ and the actual consistency of $S$. Specifically, we need to show (within MS) that $S$ proves $Q$ iff $\mathbb{N}$ satisfies Prov$_S(Q)$, and that $S$ is consistent iff $\mathbb{N}$ satisfies Con$(S)$, so that we can actually say that ( Con$(S)$ ⇒ ¬ Prov$_S$ Con$(S)$ ) means what it is supposed to mean.