@GabeGoldberg Thanks. I forgot bounded quantifiers can be pushed after the unbounded quantifiers.

@NickS I'm skeptical of that claim. Certainly there are a few notable pure math problems that stimulated the development of "new results and tools [...] with applications to many other problems", but I'm not convinced that the phenomenon occurs "very often". Do you know of any empirical data that sheds light on how often that happens? In any case, the development of new results and tools is not the primary reason we study problems like this. We study them because they're interesting, and we would be happy to see solutions to these problems even if they didn't lead to new results and tools.

In the paper "The ubiquitous Prouhet-Thue-Morse sequence", Allouche and Shallit claim that there are uncountably many overlap-free binary words, which implies that the threshold is 2. I believe this follows from Fife's theorem.

Do you mind explaining how we get that $\Pi^1_2$ is special (given that $\Pi^1_1$ is special)?

I originally meant what you're calling a simple notion of deduction, so I think I was wrong. But deduction with the $\omega$-rule is not simple in your sense, so that question is still non-trivial, right?

I could be misinterpreting what they proved. My understanding is that they proved that every true $\Pi^1_1$ sentence is provable using the $\omega$-rule. I assumed this is equivalent to saying that every true $\Pi^1_1$ sentence follows from true arithmetic sentences, but now I see that I could be wrong in assuming that (although I'm not sure why that would be wrong). If I am wrong (in which case the answer to my question is $m=0$ and any $n$), I'd still be interested in the modified question where we allow the use of the $\omega$-rule in the definition of "follows from" in step 2.