Your self-fulfilling prophecy example works for the iteration of the for loop (described in “For each xi, assume the output of X is xi, and try to deduce the expected value of U.”) in which the output is assumed to be a, but for the iteration in which the output is assumed to be b, proving that the output is a would be to prove a contradiction. “if (output X)=b then U=0″ is one possible outcome, but U could also equal anything else.
I don’t see how the NDT algorithm as given allows “(output X)=a” to be proved outside of the for loop at all. I would think it would take (output X)=whatever for each iteration through the for loop as a given before trying to prove anything, in which case in the run of the for loop in which (output X)=b is the given, proving (output X)=a is a clear contradiction, one which I would think our prover could avoid unless our axiomatic system is contradictory in the first place.
Or to rephrase, I don’t think “For each xi, assume the output of X is xi, and try to deduce the expected value of U.” and “(That is, try and deduce statements of the form “if (output X)=xi then U=ui” for some ui).” are actually equivalent at all, and I think the self-fulfilling prophecy example follows the second and ignores the first.
The point is that ‘given (output X)=a’ may eventually let you prove a contradiction when the output is not, in fact, a, and you have added a false statement as input.
In practice, one does not use a two-way axiom of (output X)=a but an one-way substitution rule ‘replace (output X) with a’ . The rule may be applied once at start, or through first N steps of deduction process (to catch the cases where deduction manages to deduce X from a slightly modified X that was included inside the ‘other algorithm’ ; note that one can’t do it forever because at some point the proof checker arrives at X from first principles, and the contradiction can be introduced by substitution.
The issue he described is specific to using (outputs X)=a as given, which allows you to e.g. do some algebra, arrive at a number a for any reason, and then replace a with (output X) , which lets you contradict yourself, or make a self fulfilling prophesy. The intent of making it a given, is to make the substitutions one way, but the theorem prover can do substitutions other way around.
Here’s what I think you’re saying: there is one value that will actually be output, call it o. In every iteration of the for loop except the one where you assume the output is o, you have assumed a false statement. From this contradiction you should be able to derive anything, and in particular, derive U(this choice)=some large negative number, such that o will appear to be the best choice. Furthermore, this argument makes no reference to what o actually is, so the algorithm can output any choice this way.
That’s a very good argument, although I never would have figured it out from the article and it took some thinking to get it from your comment. I think it proves that the algorithm is underspecified though, not (necessarily) faulty; the description given is not enough to actually figure out what the algorithm will output.
As for the rest of your comment, I think by “in practice” you mean “in decision theories other than NDT which work better”?
re: the argument, not mine, they explained it somewhere else, albeit it is hard to get.
By in practice, I mean in anything that haven’t got computing power substantially larger than that of the universe. You don’t feed the tail into the dragon when your dragon has finite mouth and long tail, that is to say, you dont feed source code into theorem provers if you don’t have to; instead you actively try to simplify the stuff that is being processed by theorem prover. You don’t make equivalence of your code with provisional output an axiom, you make it a substitution rule that works one way (it still makes nonsense eventually, but easily long after all the stars in the universe have burnt themselves out, and that can too be fixed). That is assuming you are using state of the art automated algebra package to implement decision theory.
Your self-fulfilling prophecy example works for the iteration of the for loop (described in “For each xi, assume the output of X is xi, and try to deduce the expected value of U.”) in which the output is assumed to be a, but for the iteration in which the output is assumed to be b, proving that the output is a would be to prove a contradiction. “if (output X)=b then U=0″ is one possible outcome, but U could also equal anything else.
I don’t see how the NDT algorithm as given allows “(output X)=a” to be proved outside of the for loop at all. I would think it would take (output X)=whatever for each iteration through the for loop as a given before trying to prove anything, in which case in the run of the for loop in which (output X)=b is the given, proving (output X)=a is a clear contradiction, one which I would think our prover could avoid unless our axiomatic system is contradictory in the first place.
Or to rephrase, I don’t think “For each xi, assume the output of X is xi, and try to deduce the expected value of U.” and “(That is, try and deduce statements of the form “if (output X)=xi then U=ui” for some ui).” are actually equivalent at all, and I think the self-fulfilling prophecy example follows the second and ignores the first.
The point is that ‘given (output X)=a’ may eventually let you prove a contradiction when the output is not, in fact, a, and you have added a false statement as input.
In practice, one does not use a two-way axiom of (output X)=a but an one-way substitution rule ‘replace (output X) with a’ . The rule may be applied once at start, or through first N steps of deduction process (to catch the cases where deduction manages to deduce X from a slightly modified X that was included inside the ‘other algorithm’ ; note that one can’t do it forever because at some point the proof checker arrives at X from first principles, and the contradiction can be introduced by substitution.
The issue he described is specific to using (outputs X)=a as given, which allows you to e.g. do some algebra, arrive at a number a for any reason, and then replace a with (output X) , which lets you contradict yourself, or make a self fulfilling prophesy. The intent of making it a given, is to make the substitutions one way, but the theorem prover can do substitutions other way around.
Here’s what I think you’re saying: there is one value that will actually be output, call it o. In every iteration of the for loop except the one where you assume the output is o, you have assumed a false statement. From this contradiction you should be able to derive anything, and in particular, derive U(this choice)=some large negative number, such that o will appear to be the best choice. Furthermore, this argument makes no reference to what o actually is, so the algorithm can output any choice this way.
That’s a very good argument, although I never would have figured it out from the article and it took some thinking to get it from your comment. I think it proves that the algorithm is underspecified though, not (necessarily) faulty; the description given is not enough to actually figure out what the algorithm will output.
As for the rest of your comment, I think by “in practice” you mean “in decision theories other than NDT which work better”?
re: the argument, not mine, they explained it somewhere else, albeit it is hard to get.
By in practice, I mean in anything that haven’t got computing power substantially larger than that of the universe. You don’t feed the tail into the dragon when your dragon has finite mouth and long tail, that is to say, you dont feed source code into theorem provers if you don’t have to; instead you actively try to simplify the stuff that is being processed by theorem prover. You don’t make equivalence of your code with provisional output an axiom, you make it a substitution rule that works one way (it still makes nonsense eventually, but easily long after all the stars in the universe have burnt themselves out, and that can too be fixed). That is assuming you are using state of the art automated algebra package to implement decision theory.