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.
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.