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

47 Views Asked by At

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

1

There are 1 best solutions below

11
On BEST ANSWER

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