# Is it possible that two theories be equiconsistent, with Peano Arithmetic not able to prove this?

Do there exist first-order theories that are are equiconsistent, but which cannot be proven to be equiconsistent using Peano Arithmetic? (I hope not.)

-

There is no absolute notion of "$T$ is equiconsistent with $S$". The definition depends on the background theory (in which the proof of equivalence between ${\rm Con}(T)$ and ${\rm Con}(S)$ is carried out).

Typically for set theoretic propositions, for example, Peano Arithmetic is assumed; PRA suffices, and even less can be made to work. The relevant theories are mentioned in the answers to this MO question, that you may find interesting independently of this. The point here is that, to say that two theories are equiconsistent is understood to mean that PA proves their equiconsistency, so the answer to your question is no, by definition. But let me emphasize again that the definition requires that we specify whether the background theory is PA, or PRA, or whatever, and that this matters.

For fragments of arithmetic, you want your background theory to be very weak; in general, you do not want your background theory to already prove both ${\rm Con}(T)$ and ${\rm Con}(S)$ (Naturally, this complicates matters sometimes, and not just in the context of showing equiconsistency of theories.) For a silly example, ZFC proves that PA and Z (Zermelo) are equiconsistent, since it proves that both theories have models, but this is silly; arguing over, say, PA, we get the much more reasonable conclusion that Z proves the consistency of PA and is therefore strictly stronger.

If $T$ and $S$ are very strong, it is conceivable one would be willing to settle for a "weak equiconsistency" result, where their equiconsistency is relative to a significantly strong background theory, and it is conceivable that such equiconsistency could be independent of PA. However, I do not know of any natural examples where there is need for doing this.

-
So would it be accurate to say that the stronger the background theory, the more systems which are equiconsistent relative to that background? And an inconsistent background proves that every two theories are equiconsistent. –  user18921 Feb 6 '13 at 7:17
Yes, exactly.${}$ –  Andres Caicedo Feb 6 '13 at 7:20
Is there a related idea that is background independent? For instance, we might try defining that theories $T$ and $S$ are equiconsistent* if and only if $T \vdash \mathrm{Con}(T) \rightarrow \mathrm{Con}(S)$ and $S \vdash \mathrm{Con}(S) \rightarrow \mathrm{Con}(T)$. I don't know if this can be made rigorous, but maybe something like it? –  user18921 Feb 6 '13 at 7:33
These kind of attempts tend to run into issues. For example, $T=$ZF$+\lnot$Con(ZF) and $S=$PA$+\lnot$Con(PA) are obviously not equiconsistent, but they are according to your suggested notion. Of course, we could limit ourselves to sound theories... I do not know if in that context your proposal has been studied. –  Andres Caicedo Feb 6 '13 at 15:40
How incredibly weird. –  user18921 Feb 7 '13 at 0:29
show 1 more comment

There is a phenomenon that happens when we look at questions like these, which often makes the answers uninteresting.

Let $S = \{\phi_n\}$ be the usual effective enumeration of the axioms of PA. Define a theory $T = \{\psi_1, \psi_2, \ldots\}$ where $\psi_i = \phi_i$ unless $i$ is a coded proof of $0=1$ from the axioms of ZFC, in which case $\psi_i$ is $0=1$. Note that $T$ is an effective theory for which we can write down a single, fixed program to enumerate the axioms in the manner just described. Thus, when we formalize $T$ inide PA or ZFC, we do so by using this particular program to enumerate axioms of $T$ to make the Con predicate for $T$.

Now ZFC is consistent, so in fact $T$ is the same theory as $S$, and hence they are equiconsistent. But ZFC cannot prove $S$ is the same theory as $T$, because ZFC cannot prove that ZFC is consistent, and the definition of $T$ leverages this. Thus ZFC can prove $\operatorname{Con}(S)$ but not $\operatorname{Con}(T)$, so ZFC cannot prove that $S$ and $T$ are equiconsistent.

By tweaking the original theories $S$ and $T$, we can produce examples where ZFC proves the equiconsistency, but PA does not, or where PA proves the equiconsistency, but a weaker effective theory of arithmetic $W$ does not (where the consistency of $W$ is provable in PA).

This phenomenon arises in many places when we begin to study formalized theories within ZFC or PA. Any time we quantify over all effective theories, this includes theories such as $T$ which are well behaved in the standard model but do strange things when formalized and then viewed in a nonstandard model. For this reason, it is usually more interesting to look at equiconsistency for natural theories with their canonical axiomatizations rather than with arbitrary axiomatizations.

-