Uniform solutions to Post's problem for axiomatizable theories

The Second Incompleteness Theorem says that if $T$ is a consistent (computably) axiomatizable theory which extends IΣ1, 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Σ1? 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Σ1? 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.

-
A little-known fact: Q is not strong enough for the second incompleteness theorem as it is usually proved, because Q doesn't prove the Hilbert-Bernays conditions on the Bew predicate. In fact, I read recently that Q does not verify that Bew is closed under modus ponens. I have not read the proof, though. Sigma^0_1 induction is apparently enough for the theory to verify the Hilbert-Bernays conditions, but not Sigma^0_0 induction. I only learned this when I had to actually document the hypotheses required for the incompleteness theorems this winter to help out an undergrad. – Carl Mummert May 30 '10 at 3:01
Thanks Carl! I just replaced Q by ISigma_1 as you suggested. – François G. Dorais May 30 '10 at 3:20
Very nice question, in particular #2. – Halfdan Faber May 30 '10 at 4:48
François, could you clarify what sense of computability you want here? Shall we assume that T is given by finitely many axioms over the base theory? Or do you want us to work with a program enumerating T? – Joel David Hamkins May 30 '10 at 20:53
Joel, I don't think it matters much what type of machine enumeration you use, but if you find it more comfortable you can assume that all enumerations are primitive recursive. Any computable enumeration is equivalent to a primitive recursive one via padding tricks. – François G. Dorais May 30 '10 at 21:02

2 Answers

(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 TH be T + (Con(T)$\lor$S).

-
That was blazing fast Carl! Any thoughts on #2? – François G. Dorais May 30 '10 at 3:40
Thanks; I see my blind spot now. I rewrote the answer above. – Carl Mummert May 31 '10 at 3:29
I was afraid I had extra negation symbols; the code started to blur together in my browser, but I thought I had double-checked them. They should be fixed now. – Carl Mummert Jun 1 '10 at 4:41
Great ! – Joel David Hamkins Jun 1 '10 at 5:06
I have deleted my earlier comments, which pointed out a flaw in the original answer, because the issue has been completely addressed in the revised answer. – Joel David Hamkins Jun 2 '10 at 19:58

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.

-
I wasn't assuming that $T'$ is consistent; the inconsistent theory is the top of the lattice. However, you are right that using Rosser's sentence instead is perfectly justifiable. – François G. Dorais May 30 '10 at 20:51
I don't know if Rosser's sentence gives a theory which is independent of the enumeration of T. Do you happen to know? – François G. Dorais May 30 '10 at 21:30
I doubt it. At the very least, it would seem required for the theory to prove that the enumerations gave the same theory, not merely that this was true. – Joel David Hamkins May 30 '10 at 21:45
Why is it necessary to prove the equivalence internally? – François G. Dorais May 30 '10 at 21:58
Not only can Rosser’s sentence depend on the enumeration, but in fact, it can also depend on the method of diagonalization. That is, there exist proof predicates for which Rosser’s fixed point equation has more than one solution up to provable equivalence. This is an old result of (IIRC) Guaspari and Solovay. (In contrast, Gödel’s sentence, and more generally any fixed point equation using just the provability predicate and Boolean connectives, is unique up to provable equivalence, for a fixed proof predicate.) – Emil Jeřábek Nov 8 '12 at 11:24