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?

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$. 


Adnreas, how do we know that if $¬\varphi$ is $\Sigma_1^0$, then $PA+¬\varphi$ proves $Pr_{PA}(¬\varphi)$ ? 

