I've removed the green tick until we get an answer with all the right pieces in it.

See also: Could groups be used instead of sets as a foundation of mathematics?

A bounded version of this problem is considered here: lesswrong.com/posts/TNfx89dh5KkcKrvho/…. It's bounded in the sense that M only searches proofs up to some maximum length. They also consider the case with two programs that each search for a proof the other halts. This is eventually used to construct agents which achieve mutual cooperation in the Prisoner's Dilemma, while still defecting against exploitable opponents. arxiv.org/abs/1401.5577

The paper has now been typeset. They didn't have permissions to edit this answer so they asked on reddit and I've inserted their link above.

I've seen this phenomenon in other instances where something grows sublinearly with size, so that it's proportionally shrinking. An example I remember catching me out is thinking about how the speed of a centrifuge depends on its size if you want to maintain a constant $1g$ acceleration. Does it get faster or slower as you make it larger? Answer: It rotates fewer times per second, but the outer edge moves faster.

The inequality could be phrased as $(D^na)_0\geq 0$, where $D$ is the difference operator.

Perfect! Very clear, thanks.

@EmilJeřábek Thanks. It looks like your comment has the community support. If you add it as an answer I'll accept it.

@AlexKruckman Thanks, I've fixed it.