# 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. Commented Dec 4, 2016 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. Commented Dec 5, 2016 at 6:13

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.