How to challenge Hutter's algorithm?

Question

For a given sufficiently strong formal axiomatic system $\mathsf{F}$ (like $\mathsf{PA}$ or $\mathsf{ZFC}$) and any given function $p^*(x)$ that can be specified within the formal system $\mathsf{F}$, Hutter's algorithm $M_{\mathsf{F},p^*}$ computes the function $p^*(x)$ nearly as quickly as any (provably quick) algorithm $p$ provably computing $p^*(x)$. More precisely

Let $p$ be any algorithm, computing provably the same function as $p^∗$ with computation time provably bounded by the function $t_p(\xi)$ for all $\xi$. $time_{t_p}(x)$ is the time needed to compute the time bound $t_p(x)$. Then Hutter's algorithm $M_{\mathsf{F},p^∗}$ computes $p^∗(x)$ in time $$time_{M_{\mathsf{F},p^∗}}(x) ≤ 5·t_p(x)+d_p·time_{t_p}(x)+c_p$$ with constants $c_p$ and $d_p$ depending on $p$ but not on $x$.

Here "provably" means that a proof can be found in $\mathsf{F}$. The algorithm could be interpreted as a generalization and improvement of Levin search, but I wonder whether it is always an improvement.

---

Can we use the formal system $F$ to construct a function $p^*$ for which Hutter's algorithm $M_{\mathsf{F},p^*}$ performs badly? How about asking whether a short proof of $\bot$ (i.e. a contradiction) can be found in $\mathsf{F}$? A short proof would be a proof with fewer than $n$ symbols, and we would use $x$ to encode $n$ in binary form. The function $p^*$ would just be a brute force search for the contradiction.

I think this should give a problem in $NEXP$, but the optimal algorithm to compute $p^*$ would have complexity $O(1)$, because the answer is always "no". But $M_{\mathsf{F},p^*}$ will take double exponential time in the length of $x$ to arrive at that conclusion, if I'm not mistaken. Now I wonder whether there are more interesting ways to make $M_{\mathsf{F},p^*}$ look bad, perhaps similar in spirit to Rice's theorem?

Answer 1

But $M_{\mathsf{F},p^*}$ will take double exponential time in the length of $x$ to arrive at that conclusion, if I'm not mistaken.

That $M_{\mathsf{F},p^*}$ will take double exponential time is a conjecture at best. Too see that this conjecture is pretty strong, take any formula $\phi$ that is formally independent of $\mathsf F$, and ask whether a short proof of $\phi$ can be found in $\mathsf F$. Any algorithm that can answer this question quickly (with "no") can also answer the same question for $\phi=\bot$ quickly (with "no"), because any formula can be derived in a single step from $\bot$.

Now I wonder whether there are more interesting ways to make $M_{\mathsf{F},p^*}$ look bad, perhaps similar in spirit to Rice's theorem?

Formal systems are not just bad at proving their own consistency, they are also famously bad at proving some sequence to be random. So we could ask whether a given finite sequence can be reproduced by some program shorter than $m$ symbols taking fewer than $n$ steps. The restriction to fewer than $n$ steps allows us to implement $p^*$ as a brute force search. If the sequence and $m$ are kept fixed and binary encoding is used for $n$, the resulting problem seems to be in $EXP$. Maybe it's better not to fix the sequence and $m$, because then the problem seems to be in $NEXP$.

What about a function $p^*$ based on Rice's theorem? No progress yet...

Answer 2

We could do something similar to Squark's question here:

Let $p^*$ be the program that takes an input $n$ and does the following: "Run $M_{p^*}(n)$ for $n$ steps. If it halted, output $|M_{p*}(n)| + 1$. Otherwise output $0$."

Now $M_{p^*}(n)$ takes at least $n$ steps (proof by contradiction) but $M_{p^*}(n)$ can be computed by just printing $0$, which takes $1$ step.

However, in this argument we're implicitly assuming that the formal system Hutter Search uses is consistent. The system itself can't assume that, so it doesn't find the 'proof' that $M_{p^*}(n) = 0$ for all $n$.