In the alternative algorithm for the five-and-ten problem, why should we use the first proof that we find? How about this algorithm:
A2 :=
Spend some time t searching for proofs of sentences of the form
"A2() = a → U() = x"
for a ∈ {5, 10}, x ∈ {0, 5, 10}.
For each found proof and corresponding pair (a, x):
if x > x*:
a* := a
x* := x
Return x*
If this one searches long enough (depending on how complicated U is), it will return 10, even if the non-spurious proofs are longer than the spurious ones.
In the alternative algorithm for the five-and-ten problem, why should we use the first proof that we find? How about this algorithm:
If this one searches long enough (depending on how complicated U is), it will return 10, even if the non-spurious proofs are longer than the spurious ones.
I guess then it would have to prove that it will find a proof with x > 0 within t. This is difficult.