# Is there a decidable problem which has a proof that it cannot be proved to have a particular deciding Turing machine?

I came across the question Is there an algorithm that provably exists although we don't know what it is? I was able to follow the example "Given an integer $n\ge0$ is there a run of $n$ or more consecutive 7s in the decimal expansion of $\pi?$" given in one of the answers. The answer shows that the problem in example is decidable although we don't know which is the correct algorithm. Let $P$ be a problem which is decidable, we know that for some for some finite integer $k > 1$ one of the Turing machines $M_1,M_2,..,M_k$ decides the problem, but we don't know which of them exactly is the decider. Is it possible that $P$ has a finite proof which tells us that it is not possible to prove exactly which of the machines is the decider ? Or is it always, that the proof exists proving that exactly one of the machines is the decider but we don't know it ?
I am not even sure if my question makes sense. I could make changes or remove the question if it does not not. Sorry for the vague definition of a proof.

Let us examine the following language:

$x\in L \iff ZFC \hspace{1mm} \text{is consistent}$.

Clearly, $L$ is decidable, and is decided by either the constant 1 or 0 machines.

Proofs from ZFC for the statements "$M_0$ decides $L$", "$M_1$ decides $L$" cannot exist (if ZFC is consistent), since any of those would imply a proof from ZFC about its own consistency (see Godels's second incompleteness).

Note that i can however, provide a proof that the following machine $M$ decides $L$:

Given input $x$, check if there exists a proof for the consistency of ZFC, of length$\le |x|$. If such proof is found, return 0, otherwise return 1.

If ZFC is consistent, the above machine outputs 1 for all $x$. If it isn't, we also have a proof that the above machine decides $L$ (An inconsistent system can prove any statement). The problem is that i cant prove whether or not $M$ computes the constant 1 function.

• Can't you, or is it provably unprovable? – Raphael Nov 11 '15 at 9:03
• I have proved no such proofs exists from ZFC (as a direct consequence of Godel's second incompleteness) – Ariel Nov 11 '15 at 9:21
• You have not defined a language. You state a property of languages which might be met by at most two languages (the empty set and the universal language), and as you explain it cannot be proven that either language meets this property. That's not a definition: a definition characterizes a unique object. Instead of “$L$ is decidable”, which is not well-formed because you have not defined $L$, what you can state is “any language $L such that$x\in L \iff \text{ZFC is consistent}$is decidable”, but this is not an interesting statement. – Gilles 'SO- stop being evil' Nov 11 '15 at 14:02 • I disagree,$L$is well defined, the membership of a string$x$to$L$does not have to depend on$x$. I have provided a formula which defines L. You could also refer the same arguments to the language in question, what is$L$? does it contain all strings? I dont know since i cant yet prove that$\pi$contains arbitrarily large sequences of 7. The only difference is that here you can omit the word "yet". – Ariel Nov 11 '15 at 14:12 • As a reminder I like to make these kinds of threads, the decidability of$L\$ is contingent on the excluded middle, and it is nonsensical for a constructivist to admit such statements like "ZFC is either consistent or inconsistent" as tautologies. This might be why examples such as these are somewhat counter-intuitive. – cody Jan 11 '16 at 15:57