Uniform solutions to Post's problem for axiomatizable theories

Question

The Second Incompleteness Theorem says that if $T$ is a consistent (computably) axiomatizable theory which extends IΣ₁, then $\mathrm{Con}(T)$ is not provable from $T$. By analogy with computability theory, the stronger theory $T + \mathrm{Con}(T)$ can be thought of as the "jump" of $T$. To abuse this analogy, I will use $T'$ to denote the theory $T + \mathrm{Con}(T)$. I will write $T \leq S$ when $S$ proves every axiom of $T$; I will also write $S \equiv T$ (resp. $T < S$) when $T \leq S$ and $S \leq T$ (resp. $S \nleq T$).

It is well-known that if $T$ is consistent there are plenty of axiomatizable theories $S$ such that $T < S < T'$. In the following questions $H$ will denote an operator (like $\mathrm{Con}$) that uses the computable axiomatization of $T$ to produce a sentence $H(T)$. I will write $T^H$ for the theory $T + H(T)$.

1. Is there a computable operator $H(T)$ such that $T < T^H < T'$ for every consistent axiomatizable theory $T$ extending IΣ₁? Is there such an operator which moreover satisfies that $T \equiv S$ implies $T^H \equiv S^H$?

2. Is there a computable operator $H(T)$ such that $(T^H)^H \equiv T'$ for every consistent axiomatizable $T$ extending IΣ₁? Is there such an operator which moreover satisfies that $T \equiv S$ implies $T^H \equiv S^H$?

Question 1 asks for a uniform solution to the analogue of Post's Problem for axiomatizable theories. Question 2 asks for a uniform "half-jump" operator.

Answer 1

(Note: this has been rewritten to reflect the comments below).

The answer to #1 is basically yes, because the proof that the Lindenbaum algebra above T is atomless is completely constructive.

Start with a (consistent) theory T to which the second incompleteness theorem applies, which means that T + ~Con(T) is also consistent. Then there is a sentence S such that T + ~Con(T) neither proves nor disproves S (using the first incompleteness theorem via Rosser's trick). So T + ~Con(T)$\land$~S is stronger than T + ~Con(T), but is still consistent. This means that T + ~(Con(T)$\lor$S) is consistent, so T + Con(T)$\lor$S is stonger than T.

If T $\vdash$ (Con(T)$\lor$S) $\to$ Con(T) then T $\vdash$ S $\to$ Con(T). But this means T $\vdash$ ~Con(T) $\to$ ~S which is impossible. This shows that T + (Con(T)$\lor$S) < T+ Con(T) .

So we can let T^H be T + (Con(T)$\lor$S).

Answer 2

The premise in your question that the Con operator itself has the desired property and serves as a jump operator is not universally true among the theories you consider. Specifically, you seem to assume that because $\text{Con}(T)$ is not provable in $T$, that $T+\text{Con(T)}$ is consistent. But this is not correct, because perhaps $T$ actually proves $\neg\text{Con}(T)$. One easy instance of this is the theory $T=PA+\neg\text{Con}(PA)$, which is consistent by the 2nd Incompleteness Theorem, but clearly proves $\neg\text{Con}(PA)$ and hence also $\neg\text{Con}(T)$. Thus, as weird as it sounds, $T$ is a consistent theory that proves its own inconsistency. In this case your theory $T'$ is inconsistent and the jump failed. Carl's theory $T^H$ in this case is consistent, but upon inspection you will find that it is equivalent to $T$. So for this theory $T$, your theory $T'$ jumped into inconsistency, and his theory didn't jump at all.

One can similarly replace $PA$ here with any representable theory $T_0$ and arrive at similar counterexamples, densely above any theory.

You can fix the question by considering only the case where $T'$ is consistent, which is surely what you had in mind. In this event, you would only apply the jump when it happens to arrive at a consistent theory. Since this question is not decidable from a presentation of the theory, however, even from a finite axiomatization, it may affect your motivation for considering computable versions of the half-jump, since even the full jump is not computable.

For this reason, and also because there is something a little arbitrary about having the jump only partially defined, it may be that a more robust jump arises from the Rosser sentence---there is no proof of me without a shorter proof of my negation---instead of $\text{Con}(T)$? This would put you back into the universal domain of all representable consistent theories.