Second-order undecidability

Question

Hi,

The idea of undecidability in computability theory seems to be along the lines of: There can't be an effective procedure, that decides all instances of input, but a single instance can still be decided. I view this as requiring a lot of "ad hoc" techniques specific to the class of inputs: Like "If input is of this form(one computable function)->Do this procedure(another computable function)". No matter how hard you try to generalize your techniques, you won't be able to reduce it to finite number of such statements that covers all class of inputs. This is the reason why a single instance can still be solved with some ad hoc technique. (Feel free to correct this view, if you think it isn't a right view)

Along these lines, can there be "problems" in which even all specific instance is also not decidable? (Something like nowhere differentiable function. Let us call it "nowhere decidable function/set/problem) My attempt to create such a problem doesn't seem to get me anywhere. I thought of starting with {set of all undecidable first-order theories} and asking for membership in that set, given a theory T as an input. But, once we can prove that the theory can have Natural Numbers as Model, we know that there are statements that are independent of the system by Godel's incompleteness theorem and therefore undecidable, so we have an instance of the input on which we can decide membership. Is this sufficient condition, which means it's all-input-decidable? But i am not sure how easy it is to do Model-check on a given Theory for Natural Numbers.

Or is there a way to see that such a problem can never exist? Like some ill-definedness comes in: What des it even mean to pose a problem, when all its input are undecidable? We can say a problem is defined, if only we can give at least one example to it, in which case we have already one instance i.e.the example itself, for which we know the answer, so no problem can be all instance undecidable? More generally, is it even possible to define a set S without being able to list even a single member in it? Does that even make sense?

Answer 1

Perhaps the question is illuminated by making a distinction between two notions of what it means to "decide" a question. On the one hand, a set $A\subset\mathbb{N}$ is decidable if there is a computable procedure that on input $n$ tells you yes-or-no whether $n\in A$. On the other hand, a single assertion $\psi$ is undecided by or independent of a theory $T$, if $T$ neither proves nor refutes $\psi$.

Of course, any given single statement is decidable in the computability sense, since either the "say yes" algorithm or the "say no" algorithm decides it. Similarly, it can happen that we have a pure existence proof of decidability, without being able to exhibit a particular algorithm, as in my answer to the question Can a problem be simultaneously polynomial time and undecidable?

Although these notions of undecidability seem to exist in different realms, they overlap in the following way.

Theorem. If $A\subset\mathbb{N}$ is computably enumerable, but not decidable, then for any given true c.e. theory $T$, there are infinitely many values $n$ such that the assertion $n\in A$ is undecidable in $T$.

Proof. If not, then for numbers $n$ above some $n_0$, we would have $n\notin A$ if and only if $T\vdash n\notin A$. This would make $A$ decidable, since on input $n$ above $n_0$ we could wait for $n$ to appear in $A$ and simultaneously search for a proof from $T$ that $n\notin A$, and exactly one of these searches will terminate. This contradicts our assumption on $A$. QED

Thus, every c.e. computably undecidable set is saturated with logical undecidability, even with respect to very strong theories, such as ZFC + large cardinals.

Perhaps your question is answered by the following theorem.

Theorem. There is a c.e. set $A$, such that for every natural number $n$, the particular assertion $n\in A$' is independent of PA (or any other fixed true c.e. theory $T$).

Proof. Let $A$ be the set of all $n$ that are less than the size of the smallest proof of a contradiction in $T$. That is, $n\in A$ if and only if there is a proof of a contradiction in $T$, and $n$ is smaller the size of the smallest such proof. In particular, $A$ is empty if $T$ is consistent and otherwise is $\{0,1,\ldots,k-1\}$, where $k$ is the size of the smallest proof of a contradiction in $T$, if $T$ is inconsistent. Since our assumption ensure that $T$ does not settle the question of its own inconsistency, it follows that for any specific $n$, the assertion $n\in A$ is independent of $T$. Meanwhile, $A$ is c.e., by the following algorithm: first search for a proof of a contradiction in $T$, and then enumerate all smaller numbers than the size of the smallest such proof. So this is a c.e. set all of whose particular membership assertions are independent of $T$. QED

I believe that one can make a better example, by finding an $A$ such that not only is every assertion $n\in A$ undecidable in $T$, but also these assertions are mutually undecidable, so that knowledge of some members of $A$ tells you nothing about other membership inquires.

Answer 2

For what I think you are asking, it would suffice to produce a single yes/no question whose answer cannot be "decided". Then we could ask this question on all inputs and have a "problem" for which no specific instance is decidable.

And I also think that by "decided" you really mean "proved". Well, if we're talking about provability within a given formal system that contains first order arithmetic and is known to be consistent, then by Godel we know that there do exist statements whose truth value cannot be decided within the system, for instance (a standard arithmetization of) the statement that the system itself is consistent. But this is not such a good example because we just stipulated that we know the system is consistent, so evidently we do in fact know the truth value of this statement even if we can't prove it within the system in question.

The issue becomes more subtle if we're talking about the general semantic notion of provability rather than provability within some particular formal system. I can't see how there could be any meaningful sense in which we could definitively establish that the truth value of some statement could never be known. Maybe the best candidates are statements of the form "ZFC plus large cardinal axiom X is consistent" which, if they are true, cannot be proven to be true in ZFC. I guess we cannot exclude the possibility that there is some totally new principle whose truth is intuitively evident and which does decide questions like this, the best we can say is that it doesn't seem very likely.