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


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

  • $\begingroup$ I think there is a typo, I think you meant: send $\varphi$ to $PA \vdash \varphi$. $\endgroup$ – Zuhair Dec 3 at 0:46
  • $\begingroup$ @Zuhair Whoops, quite right - fixed! $\endgroup$ – Noah Schweber Dec 3 at 2:27
  • $\begingroup$ 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? $\endgroup$ – Zuhair Dec 3 at 5:37
  • $\begingroup$ @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$. $\endgroup$ – Noah Schweber Dec 3 at 5:44
  • $\begingroup$ @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. $\endgroup$ – Noah Schweber Dec 3 at 17:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.