We're interested in recursive predicates $P(n)$ with RE range $R$ and non-RE complement $R^\prime$. For various $n \in R^\prime$ we may be able to prove that $n \in R^\prime$. For instance, if $P$ is the halting problem, then we can build a non-halting algorithm, figure out its index $n$, and we then know that $n \in R^\prime$. Another example is provability: if $P(n)$ is "the statement [with Gödel number] $n$ is provable", then we can prove that if $n$ is [the Gödel number of] the Gödel Sentence, then $n \in R^\prime$.


What I'm asking is whether there is any such recursive predicate $P(n)$ for which no member of $R^\prime$ is provably in $R^\prime$?



Membership Provability in co-RE Sets
This clearly depends on what you mean by "provably."


Under one reasonable interpretation, the answer is very much "yes." The set $S\_T$ of theorems of a (consistent, recursively axiomatizable, extending $PA$) theory $T$ is r.e., but $T$ cannot prove that the complement of $S\_T$ is nonempty (Goedel's Theorem), much less that any specific element is in the complement of $S\_T$. $\Box$


I think this probably addresses the question you ask. However, this might be unsatisfying, since a theory slightly stronger than $T$ - namely $T+Con(T)$ - can prove that certain sentences are not theorems of $T$. Maybe we don't care about "provability from $T$," but rather "provability from $T$ plus reasonable consistency assumptions." So now, we might ask something along the lines of:



> 
> Fix a theory $T$ which is a consistent, recursively axiomatizable extension of $PA$ (and, for simplicity, a subtheory of true arithmetic). Let $T^\alpha$, for $\alpha$ an ordinal, be defined by: $T^0=T$, $T^{\alpha+1}=T^\alpha+Con(T^\alpha)$, and $T^\lambda=\bigcup\_{\alpha<\lambda} T^\alpha$ for $\lambda$ a limit. Is there some co-r.e. set $X$ which has no element provably in $X$ in any of the $T^\alpha$?
> 
> 
> 


A stronger question:



> 
> Does some "ordinal iteration" of $T$ prove every true $\Pi^0\_1$ sentence?
> 
> 
> 


If the answer to this question were "yes," then this would be a sense in which the answer to your original question is - morally, at least - "no."


There's a huge problem here, however: for $\alpha\ge\omega$, $T^\alpha$ is not uniquely defined by what we've written. To make this idea precise, we need to use *ordinal notations* - that is, ways of representing ordinals by natural numbers - and now things get very messy. Alan Turing wrote a paper about this in 1939, in which he proved:



> 
> Fix a true $\Pi^0\_1$ sentence $\varphi$. Then there is some notation for $\omega+1$ according to which $T^{\omega+1}$ proves $\varphi$. More precisely, we define $T^a$ for $a$ a *notation for an ordinal*; there is then a map $\vert\cdot\vert$ from notations to ordinals - the interpretation map - and Turing's result is that there is some $a$ with $\vert a\vert=\omega+1$ such that $T^a$ proves $\varphi$.
> 
> 
> 


This isn't the end of the story; we can look at "nice" systems of notations, and try to avoid Turing's result. But things stay pretty complicated, still. I don't know much about this, but Feferman and Spector's paper "Incompleteness along paths in progressions of theories" and Franzen's book "Inexhaustibility" both go into more detail.


EDIT: Another resource you should look at is Lindstrom's book "Aspects of Incompleteness" (see Andres' comment below). (Totally unrelated, but I can't resist plugging it: Lindstrom proved one of my favorite theorems in logic - that first-order logic is the "strongest logic" with the compactness and Lowenheim-Skolem properties.)


