Is consistency an axiom of mathematics?

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.

1. 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.
2. 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?
3. 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.
4. 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.

I would not say that "the key to accepting the truth of Gödel's Theorem is to demand that mathematics is consistent." The theorem says that, if a formal system is consistent, then it can be used to express true statements that don't have proofs within the system. So, even if mathematics were inconsistent, the theorem would still be true.

It's complicated,

In ZFC, the formal theory that is the foundation for most of what people call "mathematics" today, there is no axiom saying that "ZFC is consistent". So in this sense, "ZFC is consistent" is not an axiom of mathematics. People may believe in the consistency of mathematics, but it's a subjective point of view of the interpreter of the theory, not a formal axiom.

What we get from applying Gödel's Second Incompleteness Theorem to ZFC is: "If it so happens that ZFC is consistent, then no theorem proven by ZFC will ever be 'ZFC is consistent'".

Let's see what happens when we try to add a "ZFC is consistent" axiom to create a new theory from ZFC. There are three cases:

1. Should ZFC be inconsistent, then you just created a new, inconsistent theory, because it still contains the axioms of ZFC that make it inconsistent.
2. Should ZFC be consistent, but prove its own inconsistency, the new theory is inconsistent, since you're adding the negation of a theorem as an axiom.
3. Should ZFC be consistent and not prove its own inconsistency, then the new theory is consistent too, but then Gödel's Second Incompleteness Theorem applies to this new theory, so it cannot prove its own consistency.

So in the only case where the theory turns out consistent, it still cannot prove its own consistency.

All of this just means that you can't build a consistent theory that can prove itself consistent by adding axioms to it. Your notion of mathematics will always be incomplete in that sense. Furthermore this happens with any powerful enough theory to have Peano Arithmetic, so you can't create a consistent, powerful enough theory that proves itself consistent at all.

However, notice that this "new theory" proves ZFC consistent. So if you have faith in it, then yeah, ZFC is proven consistent -- from outside ZFC itself. It just so happens that you don't gain much from it, most people would judge it's the same as just believing in ZFC in the first place.

This isn't a full answer but a supplement to what others have said.

In fact in formal logic (AFAIK) one never really sees an explicit consistency axiom. Rather, when you set up a formal deductive system using reasonable-looking principles what happens is it ends up allowing all deductions of the form $p\land\lnot p\vdash q$, where $q$ is absolutely any statement the formal system can make.

Thus, any theory that can prove $p$ and also $\lnot p$ is just the (unique) theory in which every statement you can make is a theorem. Such a theory is not generally considered interesting or worthy of study, although it's surely a mathematical theory, for whatever that's worth.

It's perfectly possible to set up your deductive system so that $p\land\lnot p$ does not entail every statement. There are different ways to do it, all falling under the heading of "paraconsistent logic". Formally, paraconsistent logics are dual to intuitionistic logics but they have received nowhere near as much attention.

On the philosophical side of things, Graham Priest's books might be of interest -- Part I of In Contradiction is pretty good (I'm not a fan of where it goes later, but YMMV). The mathematics is as far as I know still emerging. If you grok category theory 'The Evil Twin: The Basics of Complement Toposes' by Estrada-Gonzalez might be helpful.

On a philosophical note, it's still the case that the vast, vast majority of new mathematical theorems are proved informally by human beings, not formally by machines. And it is a sociological fact that most human mathematicians assume an informal version of the Principle of Non-Contradiction as part of their working practices. If you devise a new theory and prove a contradiction within it, it's unlikely to gain acceptance in the mathematical community -- de facto the PNC is in force. But formal logic is only a part of that story.