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

• (Just adding it here as a comment, since it is buried a long way down the page and a bit implicit in a comment I left) If you are interested in "in-practice reassurances" as in your last sentence states, then you can vary the requirements of your question to only ask for "$Con(A)$ if and only if $Con(B)$", where $Con$ denotes consistency. The implication $Con(A) \Rightarrow Con(B)$ is weaker than "$A$ proves $Con(B)$". – David Roberts Jan 16 at 9:07
• Also, in light of the other answers, the best you can say about your potential example is that ZFC proves $Con(PA)$. One way to see this is that ZFC proves that the set of finite ordinals is a model of $PA$, and hence the latter is consistent. – David Roberts Jan 16 at 9:12

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.

• @DavidRoberts It looks like I overreacted; I was expecting a quick negative reaction to this question, and I wanted to preempt it. If this hasn't become a downvote magnet by tomorrow, I'll remove that line. – Noah Schweber Jan 16 at 4:41
• OK, thanks. It probably would have been better as a comment first (minus the "barely") before you wrote your answer. By now, with three answers, I don't think people are going to start downvoting now in any case, so why wait until tomorrow? – David Roberts Jan 16 at 4:44
• @LSpice I did consider this. But I think leaving it here to show how it was removed amicably is an important lesson in how MO can be made a better place. – David Roberts Jan 16 at 5:30
• With all questions about provability of consistency statements, the answer is always the same: yes, it works already for $Q$. Use the same tricks as always. (Pass to a cut satisfying $S^1_2$, use provable $\exists\Sigma^b_1$-completeness in $S^1_2$. The provability predicates are $\exists\Sigma^b_1$ as the theories can be assumed finitely axiomatized.) – Emil Jeřábek Jan 16 at 7:32
• BTW, alternatatively, one can formalize the following argument with a little effort: if $T\vdash Q+\mathrm{Con}_S$ and $S\vdash Q+\mathrm{Con}_T$, then $U=T\cap S$ satisfies $U\vdash Q+\mathrm{Con}_U$, hence $U$ is inconsistent, hence so are $T$ and $S$. – Emil Jeřábek Jan 16 at 8:56

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.

• I think this argument can be done more elegantly, but not by me until after I sleep. – Andreas Blass Jan 16 at 4:04
• Are theories sufficiently strong for this purpose if they extend PA? – Matt F. Jan 18 at 13:42
• @MattF. Yes, any extension of PA is strong enough. In fact, as indicated in Noah Schweber's answer, considerably weaker theories are already strong enough. – Andreas Blass Jan 18 at 16:23

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.

• I don't think this is what the OP is looking for; note that the $n=1$ case of equiconsistency is tautologous, as opposed to immediately ruled out by the incompleteness theorem. – Noah Schweber Jan 16 at 4:46
• @Noah, yeah, I was aware that it wasn't quite the same, but since I know now that what the OP is after is ruled out (which I didn't know, so I'm glad experts jumped in), this might be a suitable alternative. – David Roberts Jan 16 at 5:31
• @Noah especially given the motivation, 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, which doesn't strictly require the OP's formulation via $A \vdash Con(B)$ and $B \vdash Con(A)$. – David Roberts Jan 16 at 5:32
• There are some alternative axiomatizations of set theory that look rather different from ZFC. For some of these, consistency implications in one, the other, or both directions with ZFC are known - there's links to discussions of many examples here en.wikipedia.org/wiki/Alternative_set_theory. These would provide additional support in the direction of "many separate systems would need to have 'bugs' at once". – Will Sawin Jan 16 at 14:52
• @WillSawin I was thinking similarly: ETCS and BZC, for instance, or variants with Replacement (or its analogue). – David Roberts Jan 16 at 15:40