Are there "typical" formal systems that have mutual consistency proofs? How long a chain of these can we build? Sufficiently powerful theories (Peano arithmetic, ZFC, and so on — this question came from thinking about Coq) can't prove their own consistency. However, are there cases of two theories, $A$ and $B$, where $A$ proves $B$ is consistent and $B$ proves $A$ is consistent? (To make up a potential example, "Peano arithmetic proves ZFC is consistent, and ZFC proves Peano arithmetic is consistent".) If so, are there long chains of these sorts of proofs we can build, so that, if any of $k$ theories were inconsistent, all of them would be?
(The context here is idle curiosity about whether we can get in-practice reassurances about our theories by noting that many separate systems would need to have "bugs" at once.)
 A: No, this cannot happen, although it's a little bit trickier than one might expect to prove this!

First, a miniature result:

Suppose $T,S$ are computably axiomatizable theories in the language of arithmetic, each containing the theory $\mathsf{I\Sigma_1}$, with $T\vdash Con(S)$ and $S\vdash Con(T)$. Then $T$ and $S$ are inconsistent.

If you haven't seen $\mathsf{I\Sigma_1}$ before, the only points you need to know are that it is finitely axiomatizable, strong enough for Godel's theorems to be applicable, and self-provably $\Sigma_1$-complete. Note that neither of the better-known arithmetics $\mathsf{Q}$ or $\mathsf{PA}$ will suffice: $\mathsf{Q}$ doesn't prove its own $\Sigma_1$-completeness since it lacks induction, and $\mathsf{PA}$ isn't finitely axiomatizable.
PROOF. It will be enough (by symmetry) to show that $T$ is inconsistent.
Since $\mathsf{I\Sigma_1}$ is finitely axiomatizable and proves its own $\Sigma_1$-completeness, we have that $T$ proves "$S$ is $\Sigma_1$-complete:" just verify in $T$ an $S$-proof of any single sentence axiomatizing $\mathsf{I\Sigma_1}$. Consequently, $T$ proves the sentence $\neg Con(T)\rightarrow [S\vdash (\neg Con(T))]$.
On the other hand, since $S\vdash Con(T)$ and $T$ is $\Sigma_1$-complete we have that $T$ proves $S\vdash Con(T)$. Putting this together with the above paragraph, we get a $T$-proof of "If $T$ is inconsistent, then $S$ proves $Con(T)\wedge\neg Con(T)$" - that is, a $T$-proof of $\neg Con(T)\rightarrow\neg Con(S)$.
But since $T\vdash Con(S)$, this gives a $T$-proof of $Con(T)$ - so $T$ is inconsistent.

The above can be improved, however.
First there's the issue of generalizing beyond $n=2$. This isn't very interesting though, since it's clear how to proceed: simply iterate the above idea by applying "provable $\Sigma_1$-completeness" over and over again.
More interestingly there's the language issue: $\mathsf{ZFC}$ for example is not a theory in the language of arithmetic, so the above result doesn't immediately apply to it. This can be handled via the notion of an interpretation. Basically, a theory $A$ interprets a theory $B$ if there is some tuple of formulas $\Phi_A$ in the language of $A$ such that for each sentence $\varphi\in B$, the theory $A$ proves that the structure defined by $\Phi_A$ satisfies $\varphi$. (Think about how $\mathsf{ZFC}$ implements arithmetic via the finite ordinals, for example.)
Via interpretations, we can generalize the argument above to arbitrary languages. Combined with the generalization past $n=2$ above, this gives the stronger result:

Suppose $T_1,...,T_n$ are computably axiomatizable theories, each of which interprets $I\Sigma_1$, such that $T_1\vdash Con(T_2)$, $T_2\vdash Con(T_3)$, ..., $T_n\vdash Con(T_1)$. Then each $T_i$ is inconsistent.

The most difficult part here is being precise about what "$Con(-)$" should mean in each of the relevant languages (basically, we just "work along interpretations").
The final improvement to be made is with respect to the base theory. We can replace $\mathsf{I\Sigma_1}$ with substantially weaker theories without changing the argument, but this doesn't get us all the way to $\mathsf{Q}$. So - dropping back to a more manageable level of generality along the other axes - we're left with a natural question:

Can there be two computably axiomatizable consistent theories $T,S$ in the language of arithmetic containing $\mathsf{Q}$ such that $T\vdash Con(S)$ and $S\vdash Con(T)$?

As Emil Jerabek comments below, the answer is still negative. However, at this point I'm not familiar with the relevant methods, so I can't say anything meaningful.
A: No, it is not possible for two sufficiently strong, consistent theories to prove each other's consistency. Here's a sketch of the proof: Suppose A and B are sufficiently strong and prove each other's consistency. Then A proves every true $\Sigma^0_1$ sentence. (This needs only that $A$ extends Robinson's Q.) Furthermore, Peano arithmetic PA proves this fact, and therefore so does B (being sufficiently strong). Apply that to the negation of an arbitrary $\Pi^0_1$ sentence $\pi$, and you find that B proves that "if $\pi$ is consistent with A then $\pi$ is true."
Consider the particular $\Pi^0_1$ sentence $\pi$ expressing "B is consistent" and remember our assumption that A proves this $\pi$.  The fact that A proves $\pi$ is a $\Sigma^0_1$ statement, so it's provable in B. That lets us simplify the conclusion of the previous paragraph to: B proves "if A is consistent then B is consistent." But by assumption, B proves "A is consistent" and therefore B also proves "B is consistent." But now Gödel's theorem tells us that B is inconsistent.
Of course, a symmetrical argument gives that A is also inconsistent. Alternatively, we can argue that the inconsistency of B, being a $\Sigma^0_1$ truth, is provable in A. But so is "B is consistent" by assumption, and thus we have an inconsistency in A.
A: Would you be happy with equiconsistency? That is, $A$ being consistent would imply $B$ consistent, and vice versa? There are lots of cases like this! I guess to make things rigorous, one would have to say how one is supposed to count the different theories, but presumably mutually contradictory theories should count as different, or theories that are proper extensions (as in, they prove strictly more theorems). Under this notion, you can say that ZF, ZFC, ZFC+CH, ZFC+(not CH) are all equiconsistent, for example. There are many more examples that can be added to this list, via models constructed by forcing. Set theorists measure the different classes of such theories via the large cardinal hierarchy.
