Let $X\subset\Pi_1^0$ be the set of statements which are provable in PA$+$Con(PA) but independent of PA. Is $X$ recursively enumerable?

$\begingroup$ Suggestion. Take also PA + not Con(PA). Then enumerate the theorems of both PA + Con(PA) and PA + non Con(PA). In the final enumeration, take the theorems that give opposite results in the two systems. Could that work? $\endgroup$ – Lucas K. May 2 '11 at 10:16

$\begingroup$ What means "opposit results"? $\endgroup$ – Alex Gavrilov May 2 '11 at 10:45

$\begingroup$ If you can prove p in PA + Con(PA) and not p in PA + not Con(PA), then p must be independent of PA (or PA is inconsistent). At that moment you can enumerate p in your solution. $\endgroup$ – Lucas K. May 2 '11 at 11:17

$\begingroup$ Lucas, If I got you right, you suggest to enumerable the statements which are equivalent to Con. I suspect that there are statements which are strictly weaker then Con but still undecidable. $\endgroup$ – Alex Gavrilov May 2 '11 at 11:19

$\begingroup$ Do you answer your own question now? $\endgroup$ – Lucas K. May 2 '11 at 12:32
The answer is no, and in particular, $X$ is $\Pi^0_1$hard. Let $\sigma(x)=\exists v\,\theta(x,v)$ be a complete $\Sigma^0_1$formula, where $\theta\in\Delta^0_0$, and find a formula $\pi(x)$ such that PA proves
$$\pi(x)\leftrightarrow\forall w\,(\mathrm{Proof_{PA}}(w,\ulcorner\pi(\dot x)\urcorner)\to\exists v\le w\,\theta(x,v))$$
by selfreference. Let $n\in\omega$. Since $\neg\pi(\bar n)$ is equivalent to a $\Sigma^0_1$ sentence, PA proves $\neg\pi(\bar n)\to\mathrm{Pr_{PA}}(\ulcorner\neg\pi(\bar n)\urcorner)$. By definition, $\neg\pi(\bar n)\to\mathrm{Pr_{PA}}(\ulcorner\pi(\bar n)\urcorner)$, hence PA proves $\mathrm{Con_{PA}}\to\pi(\bar n)$. I claim that
$$\tag{$*$}\mathbb N\models\sigma(n)\Leftrightarrow\mathrm{PA}\vdash\pi(\bar n),$$
which means that $n\mapsto\ulcorner\pi(\bar n)\urcorner$ is a reduction of the $\Pi^0_1$complete set $\{n:\mathbb N\models\neg\sigma(n)\}$ to $X$.
To show $(*)$, assume first that $M\models\mathrm{PA}+\neg\pi(\bar n)$. Then there is no standard PAproof of $\pi(\bar n)$, hence the witness $w\in M$ to the leading existential quantifier of $\neg\pi(\bar n)$ must be nonstandard. Then $\neg\theta(n,v)$ holds for all $v\le w$, and in particular, for all standard $v$, hence $\mathbb N\models\neg\sigma(\bar n)$.
On the other hand, assume that PA proves $\pi(\bar n)$, and let $k$ be the code of its proof. Since PA is sound, $\mathbb N\models\pi(\bar n)$, hence there exists $v\le k$ witnessing $\theta(\bar n,v)$, i.e., $\mathbb N\models\sigma(\bar n)$.
Here's a proof that doesn't directly diagonalize but instead relies on wellknown results, which in turn were proved by diagonalization. So ultimately, it isn't really easier than Emil's, but it may be easier to find and remember.
I claim first that, if a $\Pi^0_1$ sentence $\phi$ is provable in PA plus $\neg\text{Con}(PA)$, then it is already provable in PA. This is probably well known, but here's a proof anyway. The assumption is equivalent to saying that $\text{Con}(PA)$ is provable from PA plus $\neg\phi$. But since $\neg\phi$ is a $\Sigma^0_1$ sentence, one can also prove from PA plus $\neg\phi$ that PA proves $\neg\phi$. Combining the preceding two sentences, we get a proof from PA plus $\neg\phi$ that PA plus $\neg\phi$ is consistent. By Gödel's second incompleteness theorem, it follows that PA plus $\neg\phi$ is inconsistent. This means that PA proves $\phi$, as claimed.
Now consider the transformation $T$ on $\Pi^0_1$ sentences defined by letting $T(\phi)$ be $\text{Con}(PA)\lor\phi$. I claim that $T(\phi)$ is in the set $X$ of the question if and only if PA does not prove $\phi$. To see this, note first that $T(\phi)$ is trivially provable from PA plus $\text{Con}(PA)$. So $T(\phi)\in X$ if and only if PA doesn't prove $\text{Con}(PA)\lor\phi$. That's if and only if PA plus $\neg\text{Con}(PA)$ doesn't prove $\phi$. And, by the claim proved above, that's if and only if PA doesn't prove $\phi$.
So T is a (trivially computable) manyone (in fact oneone) reduction to $X$ of the set of $\Pi^0_1$ sentences not provable in PA. The latter set is known not to be recursively enumerable; therefore neither is $X$.

$\begingroup$ Thank you, Andreas. This is nice! Why didn't I see it before? $\endgroup$ – Alex Gavrilov May 3 '11 at 6:50

$\begingroup$ Adnreas, how do we know that if $¬\varphi$ is $\Sigma_1^0$, then $PA+¬\varphi$ proves $Pr_{PA}(¬\varphi)$ ? $\endgroup$ – mtg May 24 '13 at 13:19

$\begingroup$ PA proves $\sigma\to\Pr_{PA}(\ulcorner\sigma\urcorner)$ for every $\Sigma^0_1$sentence $\sigma$ by formalizing the proof of $\Sigma^0_1$completeness of Q. $\endgroup$ – Emil Jeřábek May 24 '13 at 15:16

$\begingroup$ It might be useful to add that this "provable $\Sigma^0_1$completeness" result can be found in textbooks as an ingredient in the proof of the second incompleteness theorem. $\endgroup$ – Andreas Blass May 24 '13 at 16:33

$\begingroup$ I didn't know how to make a comment, sorry, but you're right. In the meantime I figured out that $\Sigma^0_1$completeness of $PA$ is provable in $PA$, but thanks  yeah, that's pretty obvious. $\endgroup$ – mtg May 24 '13 at 21:55