Problem: Is it true that for every $\Pi^0_1$ relation $P(e, t) \subseteq \omega\times\omega$ there is a partial recursive function $g \colon \omega \to \omega$ satisfying $(\exists t)P(e, t) \Rightarrow \left(g(e)\!\downarrow\ \&\ P(e, g(e))\right)?$
My attempt: Take $P(e, t)$ to be $|W_e| < t$. It is $\Pi^0_1$ because its negation is r.e. (just enumerate in a dovetailing fashion all $W_e$ and add a pair $(e, t)$ whenever you see that $|W_{e, s}| \geqslant t$). Then the expression $(\exists t)P(e, t)$ just says that $W_e$ is finite. So $g(e)$ gives an upper bound on the cardinality of $W_e$ whenever it is finite. But such a function can't be recursive. To see this, using recursion theorem define $$W_e = \begin{cases} \{0, 1, \dots, g(e)\},& \text{if } g(e)\!\downarrow,\\ \varnothing,& \text{otherwise.} \end{cases}$$ $W_e$ is always finite, so it must be the case that $g(e)\!\downarrow$ and hence $W_e = \{0, 1, \dots, g(e)\}$, but $|W_e| > g(e)$, a contradiction.
It took me a while to come up with such an example. Initially, I was looking through some "halting problem-like" relations and was trying to show that the existence of such a function $g(e)$ leads to the decidability of the halting problem or something similar, but no one of them worked. Nevertheless, I'm pretty sure that there must be such examples, because the problem is basically "Does uniformization (or $\Sigma^0_1$-selection) principle hold for $\Pi^0_1$ relations?". So it just seems that I was lucky enough and randomly stumbled upon such a counterexample, but don't really have a general understanding of what exact "property" must the relation have to serve as a counterexample.
Question: Is there a more natural (or easier) example of such a relation $P(e, t)$ directly related to the halting problem? Also I'm interested in what specific ideas or knowledge from computability theory have led you to such a counterexample?
Thank you in advance!
There is indeed (in my opinion) an easier way to do this. But I don't think trying to embed the Halting Problem is necessarily the way to go, since often you can't actually do that (e.g. you can build an infinite binary tree with no computable path, but every infinite binary tree will have a low path so you can't code the halting problem in).
Instead, I like to think of these types of problems dynamically: you are playing a game against various opponents (the partial computable functions) and building a set in a certain way (in this case, throwing things out of the set - the set is what's left over). If your strategy is computable, then everything works!
In this case, I'll break into pieces. I'll have a different computable strategy for each column $C_m=\{n: P(m, n)\}$ (these strategies will be uniform though, so no problem), which ensures that $C_m$ defeats $\varphi_m$ (because why not?).
I need to make $C_m$ nonempty (otherwise there's no requirement on what $\varphi_m(m)$ should do), so let's begin by not throwing anything out of $C_m$. Now we wait for $\varphi_m(m)$ to halt. If it never does, we never throw anything out of $C_m$, so $C_m=\omega$; and in particular $\exists n((m, n)\in P)$, so $\varphi_m$ is defeated. If $\varphi_m(m)\downarrow=k$, then my action is clear: throw $k$ out of $C_m$, and leave everything else in $C_m$!
This is clear as a strategy in a game. Now I turn it into a description of a computable set:
$$P=\{(m, n): \neg(\varphi_m(m)\downarrow=n)\}.$$ It's not hard to check that this is $\Pi^0_1$, and we're done!