Uniform solutions to Post's problem for axiomatizable theories - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-18T07:07:43Z http://mathoverflow.net/feeds/question/26411 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/26411/uniform-solutions-to-posts-problem-for-axiomatizable-theories Uniform solutions to Post's problem for axiomatizable theories François G. Dorais 2010-05-30T02:44:59Z 2010-06-01T04:26:50Z <p>The Second Incompleteness Theorem says that if $T$ is a consistent (computably) axiomatizable theory which extends I&Sigma;<sub>1</sub>, 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 &lt; S$) when $T \leq S$ and $S \leq T$ (resp. $S \nleq T$). </p> <p>It is well-known that if $T$ is consistent there are plenty of axiomatizable theories $S$ such that $T &lt; S &lt; 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)$.</p> <ol> <li><p>Is there a computable operator $H(T)$ such that $T &lt; T^H &lt; T'$ for every consistent axiomatizable theory $T$ extending I&Sigma;<sub>1</sub>? Is there such an operator which moreover satisfies that $T \equiv S$ implies $T^H \equiv S^H$?</p></li> <li><p>Is there a computable operator $H(T)$ such that $(T^H)^H \equiv T'$ for every consistent axiomatizable $T$ extending I&Sigma;<sub>1</sub>? Is there such an operator which moreover satisfies that $T \equiv S$ implies $T^H \equiv S^H$?</p></li> </ol> <p>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.</p> http://mathoverflow.net/questions/26411/uniform-solutions-to-posts-problem-for-axiomatizable-theories/26413#26413 Answer by Carl Mummert for Uniform solutions to Post's problem for axiomatizable theories Carl Mummert 2010-05-30T03:10:17Z 2010-06-01T04:26:50Z <p>(Note: this has been rewritten to reflect the comments below). </p> <p>The answer to #1 is basically yes, because the proof that the Lindenbaum algebra above T is atomless is completely constructive. </p> <p>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. </p> <p>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) &lt; T+ Con(T) .</p> <p>So we can let T<sup>H</sup> be T + (Con(T)$\lor$S). </p> http://mathoverflow.net/questions/26411/uniform-solutions-to-posts-problem-for-axiomatizable-theories/26500#26500 Answer by Joel David Hamkins for Uniform solutions to Post's problem for axiomatizable theories Joel David Hamkins 2010-05-30T20:33:58Z 2010-05-30T20:47:47Z <p>The premise in your question that the <em>Con</em> 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.</p> <p>One can similarly replace $PA$ here with any representable theory $T_0$ and arrive at similar counterexamples, densely above any theory.</p> <p>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. </p> <p>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---<em>there is no proof of me without a shorter proof of my negation</em>---instead of $\text{Con}(T)$? This would put you back into the universal domain of all representable consistent theories.</p>