Membership Provability in co-RE Sets

Question

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

Answer 1

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

Answer 2

Noah has given an excellent answer. Here is another way to look at such an answer.

Theorem. For EVERY computably enumerable set $R$ and for every computably axiomatizable consistent theory $T$, there is a Turing machine that enumerates $R$, such that $T$ does not prove any assertion of the form $n\in R'$, using that enumeration of $R$.

Proof. Fix any enumeration of $R$, and then modify it to produce a Turing machine that also enumerates everything into $R$, if a proof of a contradiction from $T$ is found. Since $T$ does not prove that $T$ has no such proof, $T$ cannot prove that any assertion of the form $n\in R'$. But meanwhile, since $T$ really is consistent, then this program will enumerate $R$ correctly. QED

Thus, the property you are asking about is not a property of the predicate or the c.e. set you have in mind, but rather it is a property of your way of describing how that set is enumerated. In other words, what you have is an intensional property of the set rather than an extensional one.