11
$\begingroup$

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.

$\endgroup$
12
  • 1
    $\begingroup$ 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. $\endgroup$ May 30, 2010 at 3:01
  • $\begingroup$ Thanks Carl! I just replaced Q by ISigma_1 as you suggested. $\endgroup$ May 30, 2010 at 3:20
  • $\begingroup$ Very nice question, in particular #2. $\endgroup$ May 30, 2010 at 4:48
  • $\begingroup$ 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? $\endgroup$ May 30, 2010 at 20:53
  • $\begingroup$ 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. $\endgroup$ May 30, 2010 at 21:02

2 Answers 2

8
$\begingroup$

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

$\endgroup$
5
  • $\begingroup$ That was blazing fast Carl! Any thoughts on #2? $\endgroup$ May 30, 2010 at 3:40
  • $\begingroup$ Thanks; I see my blind spot now. I rewrote the answer above. $\endgroup$ May 31, 2010 at 3:29
  • 1
    $\begingroup$ 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. $\endgroup$ Jun 1, 2010 at 4:41
  • 1
    $\begingroup$ Great ! $\endgroup$ Jun 1, 2010 at 5:06
  • $\begingroup$ 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. $\endgroup$ Jun 2, 2010 at 19:58
5
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$ May 30, 2010 at 20:51
  • $\begingroup$ I don't know if Rosser's sentence gives a theory which is independent of the enumeration of T. Do you happen to know? $\endgroup$ May 30, 2010 at 21:30
  • $\begingroup$ 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. $\endgroup$ May 30, 2010 at 21:45
  • $\begingroup$ Why is it necessary to prove the equivalence internally? $\endgroup$ May 30, 2010 at 21:58
  • 1
    $\begingroup$ 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.) $\endgroup$ Nov 8, 2012 at 11:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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