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 $ISigma_1$, with $Tvdash Con(S)$ and $Svdash Con(T)$. Then $T$ and $S$ are inconsistent.
If you haven’t seen $ISigma_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 $ISigma_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 $ISigma_1$. Consequently, $T$ proves the sentence $neg Con(T)rightarrow (Svdash (neg Con(T)))$.
On the other hand, since $Svdash Con(T)$ and $T$ is $Sigma_1$-complete we have that $T$ proves $Svdash Con(T)$. Putting this together with the above paragraph, we get a $T$-proof of “If $T$ is inconsistent, then $S$ proves $Con(T)wedgeneg Con(T)$” – that is, a $T$-proof of $neg Con(T)rightarrowneg Con(S)$.
But since $Tvdash 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 $varphiin 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 $ISigma_1$, such that $T_1vdash Con(T_2)$, $T_2vdash Con(T_3)$, …, $T_nvdash 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. $ISigma_1$ can certainly be pushed down substantially 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 $Tvdash Con(S)$ and $Svdash Con(T)$?
If memory serves the answer is still “no,” but I don’t immediately see the proof. (Note that at this point we really should be careful about what specific consistency predicate we’re using – there are certainly easy modifications of the standard consistency predicates which make things go through nicely, basically by restricting attention to a “tame cut” of the natural numbers, but I’m not sure if those modifications are necessary.)
