# Decidability of language containing strings of length equal to that of some substring of 1s in $\pi$?

I read that the following language is decidable.

$\{w | w \in \{0, 1\}^* \text{ and } 1^{|w|} \text{ is a substring in binary expansion of } \pi \}$

The proof has been given by considering the two possible cases

• Suppose it is true that there exists a minimal integer $N$ such that the binary expansion of $\pi$ only contains substrings of 1 having length at most $N$. That is, it contains substring $1^N$ but not $1^{N + 1}$. Define a corresponding turing machine $M_N$ such that it accepts the input string if it is of length $N$, otherwise rejects it. This machine decides the given language.

• Suppose the binary expansion of $\pi$ contains substrings of $1$s of all lengths. Then the Turing machine that accepts all strings decides the given language.

We are not able to construct a single Turing machine that decides the language given, but one of these machines thus constructed will decide it but we do not know which. I don't quite understand how this language is decidable?

• A very similar question was asked before. This is just a non-constructive proof. If you don't like that, you can read up on intuitionistic mathematics. – Yuval Filmus Dec 4 '16 at 23:37
• I see. What I do not understand is how this question is well-posed, since the maximum length of substrings of 1s in the expansion of pi is not known. – slnsoumik Dec 5 '16 at 6:13

You are confusing knowledge and truth. Something may be true without us knowing precisely why. An object may exist without us being able to construct it.

If you belive in classical logic, then it is true that the maximum length of consequtive 1's in the expansion of $\pi$ is either finite or infinite. In each case, there exists a decision procedure for your language. Therefore a decision procedure exists.

But we do not know which of the cases happens, and so we not not know a particular decision procedure, even though one exists. If you don't like this line of reasoning, then you should ask for a constructive proof of decidability of your language.