How the hell will it find proof that U() returns 100 if U() does not have 100 in a single return statement, and clearly can only return 5 or 10? Or are you meaning 10 here? Still, how it can find such proof with any but a very broken proof system?
It seems to me that even a very simple set of axioms will allow it to treat A() as a black box that returns x here, arriving at correct proof that if x=1 then U()=5 , without ever recursing into itself. When i have to make bots in game do something, i dont make bots emulate bots, i just say, x is the every bot’s output in those circumstances, then apply algebra to find x from equation that got x on both sides.
edit: furthermore, the proof systems that can prove a contradiction, can prove anything.
I guess i miss something about decision theories. I, basically, do applied math for a living, meaning that I do decisions using math, in the domain where it works. First thing I do when I need to get rid of recursion, is turn this into an equation with x (or many unknowns). You just treat the bot as black box, which outputs the value that the bot outputs. Then, you can arrive at equation with one solution or many solutions or infinitely many solutions. I don’t need to secondguess myself by running myself in emulator. Black-box unknown works fine.
As one of my math teachers used to say, “if something’s obvious, that means it’s easy to prove”. Can you prove that the agent cannot easily prove that A()=1 implies U()=100?
edit: nevermind, did read the post before explanation was added. Guys, seriously, this stuff is confusing enough and its really hard to see what is the point of exercise even, when theres no actual hints on that. Furthermore, it is not mainstream knowledge of any kind. The updateless decision theory is specifically lesswrong thing. It’s not easy for those who write practical deciding agents to get the point of exercise with the newcomb’s , as in practical approach, there’s simply two ways to write down the payoffs in newcomb, which looks too much like typical problem formalizing problem descriptions written in English (and newcomb’s just doesn’t even look like a problem description that different people would understand exactly in same way)
It doesn’t prove U()=100, it proves [A()=1 implies U()=100]. Simultaneously having the proof that [A()=1 implies U()=5] allows you to disprove A()=1, which is perfectly fine, since actually A()=2.
How the hell will it find proof that U() returns 100 if U() does not have 100 in a single return statement, and clearly can only return 5 or 10? Or are you meaning 10 here? Still, how it can find such proof with any but a very broken proof system?
It seems to me that even a very simple set of axioms will allow it to treat A() as a black box that returns x here, arriving at correct proof that if x=1 then U()=5 , without ever recursing into itself. When i have to make bots in game do something, i dont make bots emulate bots, i just say, x is the every bot’s output in those circumstances, then apply algebra to find x from equation that got x on both sides.
edit: furthermore, the proof systems that can prove a contradiction, can prove anything.
I guess i miss something about decision theories. I, basically, do applied math for a living, meaning that I do decisions using math, in the domain where it works. First thing I do when I need to get rid of recursion, is turn this into an equation with x (or many unknowns). You just treat the bot as black box, which outputs the value that the bot outputs. Then, you can arrive at equation with one solution or many solutions or infinitely many solutions. I don’t need to secondguess myself by running myself in emulator. Black-box unknown works fine.
As one of my math teachers used to say, “if something’s obvious, that means it’s easy to prove”. Can you prove that the agent cannot easily prove that A()=1 implies U()=100?
edit: nevermind, did read the post before explanation was added. Guys, seriously, this stuff is confusing enough and its really hard to see what is the point of exercise even, when theres no actual hints on that. Furthermore, it is not mainstream knowledge of any kind. The updateless decision theory is specifically lesswrong thing. It’s not easy for those who write practical deciding agents to get the point of exercise with the newcomb’s , as in practical approach, there’s simply two ways to write down the payoffs in newcomb, which looks too much like typical problem formalizing problem descriptions written in English (and newcomb’s just doesn’t even look like a problem description that different people would understand exactly in same way)
It doesn’t prove U()=100, it proves [A()=1 implies U()=100]. Simultaneously having the proof that [A()=1 implies U()=5] allows you to disprove A()=1, which is perfectly fine, since actually A()=2.