Return to Answer

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

If you haven't seen $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.

Since $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 $I\Sigma_1$. Consequently, $T$ proves the sentence $\neg Con(T)\rightarrow [S\vdash (\neg Con(T))]$.

The final improvement to be made is with respect to the base theory. $I\Sigma_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:

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.)

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.

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))]$.

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:

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.

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.

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.

No, this cannot happen, although it's a little bit trickier than one might expect to prove this! (This subtlety is why I'm answering as opposed to voting to close as more appropriate for MSE; I think that this is MO-appropriate, if only barely.)

No, this cannot happen, although it's a little bit trickier than one might expect to prove this!