When we don’t know how to solve a problem even given infinite computing power, the very work we are trying to do is in some sense murky to us.
I wonder where this goes with questions about infinite domains. It seems to me that I understand what it means to argmax a generic bounded function on a generic domain, but I don’t know an algorithm for it and as far as I know there can’t be one. So it seems taking this very seriously would lead us to some form of constructionism.
Hmm. If we’re trying to argmax some function f over the real numbers, then the simplest algorithm would be something like “iterate over all mathematical expressions e; for each one, check whether the program ‘iterate over all provable theorems, halting when you find one that says e=argmaxf’ halts; if it does, return e.”
...but I guess that’s not guaranteed to ever halt, since there could conceivably be an infinite procession of ever-more-complex expressions, eking out ever-smaller gains on f. It seems possible that no matter what (reasonably powerful) mathematical language you choose, there are function-expressions with finite maxima at values not expressible in your language. Which is maybe what you meant by “as far as I know there can’t be [an algorithm for it].”
(I’m assuming our mathematical language doesn’t have the word argmax, since in that case we’d pretty quickly stumble on the expression argmaxf, verify that argmaxf=argmaxf, and return it, which is obviously a cop-out.)
I wonder where this goes with questions about infinite domains. It seems to me that I understand what it means to argmax a generic bounded function on a generic domain, but I don’t know an algorithm for it and as far as I know there can’t be one. So it seems taking this very seriously would lead us to some form of constructionism.
Hmm. If we’re trying to argmax some function f over the real numbers, then the simplest algorithm would be something like “iterate over all mathematical expressions e; for each one, check whether the program ‘iterate over all provable theorems, halting when you find one that says e=argmaxf’ halts; if it does, return e.”
...but I guess that’s not guaranteed to ever halt, since there could conceivably be an infinite procession of ever-more-complex expressions, eking out ever-smaller gains on f. It seems possible that no matter what (reasonably powerful) mathematical language you choose, there are function-expressions with finite maxima at values not expressible in your language. Which is maybe what you meant by “as far as I know there can’t be [an algorithm for it].”
(I’m assuming our mathematical language doesn’t have the word argmax, since in that case we’d pretty quickly stumble on the expression argmaxf, verify that argmaxf=argmaxf, and return it, which is obviously a cop-out.)