3 deleted comment

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.

This could be a very hard pair of questions. However, I suspect that the solutions of the analogous questions in computability theory could be translated to provide an easy answer, but I don't know how that would work...

2 Replaced Q by ISigma_1

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

This could be a very hard pair of questions. However, I suspect that the solutions of the analogous questions in computability theory could be translated to provide an easy answer, but I don't know how that would work...

1

# 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 Robinson's $Q$, 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 $Q$? 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 $Q$? 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.

This could be a very hard pair of questions. However, I suspect that the solutions of the analogous questions in computability theory could be translated to provide an easy answer, but I don't know how that would work...