Right. MIRI’s most important paper to date, Definability of Truth in Probabilistic Logic, isn’t constructive either. However, you take what you can get.
I think there are two different kinds of constructivity being discussed here: regarding existence theorems and regarding the values of variables. We can afford to be nonconstructive about existence theorems, but if you want to characterize the value of a variable like “the optimal action for the agent to take”, your solution must necessarily be constructive in the sense of being algorithmic. You can say, “the action with the highest expected utility under the agent’s uncertainty at the time the action was calculated!”, but of course, that assumes that you know how to define and calculate expected utility, which, as the paper shows, you often don’t.
I brought up Laplace’s Demon because it seems to me like it might be possible to treat Omega as adversarial in the No Free Lunch sense, that it might be possible that any decision theory can be “broken” by some sufficiently perverse situation, when we make the paradoxical assumption that our agent has unlimited computing resources and our adversary has unlimited computing resources and we can reason perfectly about each-other (ie: that Omega is Laplace’s Demon but we can reason about Omega).
I think there are two different kinds of constructivity being discussed here: regarding existence theorems and regarding the values of variables. We can afford to be nonconstructive about existence theorems, but if you want to characterize the value of a variable like “the optimal action for the agent to take”, your solution must necessarily be constructive in the sense of being algorithmic. You can say, “the action with the highest expected utility under the agent’s uncertainty at the time the action was calculated!”, but of course, that assumes that you know how to define and calculate expected utility, which, as the paper shows, you often don’t.
I brought up Laplace’s Demon because it seems to me like it might be possible to treat Omega as adversarial in the No Free Lunch sense, that it might be possible that any decision theory can be “broken” by some sufficiently perverse situation, when we make the paradoxical assumption that our agent has unlimited computing resources and our adversary has unlimited computing resources and we can reason perfectly about each-other (ie: that Omega is Laplace’s Demon but we can reason about Omega).