MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
Note that the second example you give isn't quite an example, since you need to pass to a slightly stronger theory to show that the Goedel sentence is not provable. – Noah Schweber Aug 10 '13 at 21:58
up vote 7 down vote accepted

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

share|cite|improve this answer
In Aspects of incompleteness by P. Lindström, it is shown that if we are given an r.e. family of r.e. theories (each being consistent and extending $\mathsf{PA}$), then there are $\Pi^0_1$ formulas simultaneously independent over all of them. (For this, and generalizations, see Chapter 3.) – Andrés E. Caicedo Aug 10 '13 at 23:59
Cool, I didn't know that! I'm adding Lindstrom's book to my answer as an interesting source. – Noah Schweber Aug 11 '13 at 0:44

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.

share|cite|improve this answer
As far as I can see, you haven't needed the assumption of non-computability in the theorem. The proof works even if $R$ is, for example, empty. – Andreas Blass Aug 11 '13 at 4:36
Yes, you are right; I was just using the OP's hypothesis. I have now edited to remove it. – Joel David Hamkins Aug 11 '13 at 13:50

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.