# Can a theory play the role of conservatively extending a strictly weaker or incomparable theory?

Suppose we have effective first order theories $$T, T^+$$ and have some injective function $$t$$ that sends (translate) every formula of the language of $$T$$ to a formula of the language of $$T^+$$; such that $$T^+$$ proves all $$t$$-translations of theorems of $$T$$, but $$T^+$$ doesn't prove $$t$$-translations of sentences of the language of $$T$$ that are not theorems nor axioms of $$T$$.

I'd label that situation as: Theory $$T^+$$ plays the role of conservatively extending theory $$T$$ over translation $$t$$.

Questions:

1. Can theory $$T^+$$ be of incomparable consistency strength with theory $$T$$?

2. Can theory $$T^+$$ be of strictly stronger consistency strength than theory $$T$$?

The answer to both questions is yes, for unsatisfying reasons.

To avoid immediate triviality we need to require that $$t$$ (as well as $$T$$ and $$T^+$$) be "simple" - say, computable. This is because the sets of $$T$$-theorems, $$T$$-non-theorems, $$T^+$$-theorems, and $$T^+$$-non-theorems are all countably infinite$$^1$$ so without a complexity restriction such a $$t$$ always exists (just pair up a bijection between the $$T$$-theorems and the $$T^+$$-theorems with a bijection between the $$T$$-non-theorems and the $$T^+$$-non-theorems).

But that still doesn't save us. For example, let's look at $$T=PA$$ and $$T^+=ZFC$$. The translation "$$\varphi\mapsto\varphi^{HF}$$" does not work of course, but there is one which does: send $$\varphi$$ to (the ZFC-implementation of) the sentence "$$PA\vdash \varphi$$." This is clearly computable and injective, and assuming ZFC is arithmetically sound we have $$PA\vdash\varphi\quad\iff\quad ZFC\vdash (PA\vdash\varphi).$$ Indeed, this idea works for any pair $$T,T^+$$ of theories which are appropriately sound and $$\Sigma_1$$-complete, and that gives very silly positive answers to both your questions.

At the moment I don't see a way to modify the question to avoid this problem.

$$^1$$Saying that a theory is effective presupposes that its language is countable (indeed, effective).

• I think there is a typo, I think you meant: send $\varphi$ to $PA \vdash \varphi$. – Zuhair Dec 3 at 0:46
• @Zuhair Whoops, quite right - fixed! – Noah Schweber Dec 3 at 2:27
• there must be a way to characterize $t$ as to avoid this unsatisfactory condition. I'll think about it. By the way do the above argument work when the theories are incomparable? – Zuhair Dec 3 at 5:37
• @Zuhair Yes - the only assumption used was that they are both strong enough to talk about provability and that they're both $\Sigma_1$-sound (and complete, but that's basically trivial) in the appropriate ways (e.g. for ZFC, this is meant in the sense of $HF$). For example, it applies to any pair of theories extending (or interpreting, even) the weak arithmetic $I\Sigma_1$. – Noah Schweber Dec 3 at 5:44
• @Zuhair I don't know what that means. Any formula $\varphi$ is equivalent to "$T=T$ and $\varphi$" (appropriately phrased). So that restriction seems to rule out everything. – Noah Schweber Dec 3 at 17:44