I think CM with a logical coin is not well-defined. Say Omega determines whether or not the millionth digit of pi is even. If it’s even, you verify this and then Omega asks you to pay $1000; if it’s odd Omega gives you $1000000 iff. you would have paid Omega had the millionth digit of pi been even. But the counterfactual “would you have paid Omega had the millionth digit of pi been even and you verified this” is undefined if the digit is in fact odd, since you would have realized that it is odd during verification. If you don’t actually verify it, then the problem is well-defined because Omega can just lie to you. I guess you could ask the counterfactual “what if your digit verification procedure malfunctioned and said the digit was even”, but now we’re getting into doubting your own mental faculties.

Perhaps I am missing the obvious, but why is this a hard problem? So our protagonist AI has some algorithm to determine if the millionth digit of pi is odd- he cannot run it yet, but he has it. Lets call that function f{}, that returns a 1 if the digit is odd, or a 0 if it is even. He also has some other function like:
sub pay_or_no
{
if (f{})
{
pay(1000);
}

In this fashion, Omega can verify the algorithm that returns the millionth digit of pi, independently verify the algorithm that pays based on that return, and our protagonist gets his money.

This seems to be the correct answer to jacobt’s question. The key is looking at the length of proofs. The general rule should go like this: when you’re trying to decide which of two impossible counterfactuals “a()=x implies b()=y” and “a()=x implies b()=z” is more true even though “a()=x” is false, go with the one that has the shorter proof. We already use that rule when implementing agents that compute counterfactuals about their own actions. Now we can just implement Omega using the same rule. If the millionth digit of pi is in fact odd, but the statement “millionth digit of pi is even ⇒ agent pays up” has a much shorter proof than “millionth digit of pi is even ⇒ agent doesn’t pay up”, Omega should think that the agent would pay up.

The idea seems so obvious in retrospect, I don’t understand how I missed it. Thanks!

If the millionth digit of pi is in fact odd, but the statement “millionth digit of pi is even ⇒ agent pays up” has a much shorter proof than “millionth digit of pi is even ⇒ agent doesn’t pay up”, Omega should think that the agent would pay up.

This seems equivalent to:

has a much shorter proof than “millionth digit of pi is odd”

But does that make sense? What if it were possible to have really short proofs of whether the n-th digit of pi is even or odd and it’s impossible for the agent to arrange to have a shorter proof of “millionth digit of pi is even ⇒ agent pays up”? Why should the agent be penalized for that?

Maybe the whole point of a logical coinflip is about being harder to prove than simple statements about the agent. If the coinflip were simple compared the the agent, like “1!=1”, then a CDT agent would not have precommitted to cooperate, because the agent would have figured out in advance that 1=1. So it’s not clear that a UDT agent should cooperate either.

I agree, this seems like a reasonable way of defining dependencies between constant symbols. In case of logical uncertainty, I think you’d want to look into how relative lengths of proofs depend on adding more theorems as axioms (so that they don’t cost any proof length to use). This way, different agents or an agent in different situations would have different ideas about which dependencies are natural.

This goes all the way back to trying to define dependencies by analogy with AIXI/K-complexity, I think we were talking about this on the list in spring 2011.

Good point, thanks. You’re right that even-world looks just as impossible from odd-world’s POV as odd-world looks from even-world, so Omega also needs to compute impossible counterfactuals when deciding whether to give you the million. The challenge of solving the problem now looks very similar to the challenge of formulating the problem in the first place :-)

Why not? It seems to me that to determine that the staple maximizer’s offer is fair, you need to look at the staple maximizer’s assessment of you in the impossible world where it gets control. That’s very similar to looking at Omega’s assessment of you in the impossible world where it’s deciding whether to give you the million. Or maybe I’m wrong, all this recursion is making me confused...

What I meant is, in my version of the problem, you don’t have to solve the problem (say what Omega does exactly) in order to formulate the problem, since “the staple maximizer’s assessment of you in the impossible world where it gets control” is part of the solution, not part of the problem specification.

I think CM with a logical coin is not well-defined. Say Omega determines whether or not the millionth digit of pi is even. If it’s even, you verify this and then Omega asks you to pay $1000; if it’s odd Omega gives you $1000000 iff. you would have paid Omega had the millionth digit of pi been even. But the counterfactual “would you have paid Omega had the millionth digit of pi been even and you verified this” is undefined if the digit is in fact odd, since you would have realized that it is odd during verification. If you don’t actually verify it, then the problem is well-defined because Omega can just lie to you. I guess you could ask the counterfactual “what if your digit verification procedure malfunctioned and said the digit was even”, but now we’re getting into doubting your own mental faculties.

Perhaps I am missing the obvious, but why is this a hard problem? So our protagonist AI has some algorithm to determine if the millionth digit of pi is odd- he cannot run it yet, but he has it. Lets call that function f{}, that returns a 1 if the digit is odd, or a 0 if it is even. He also has some other function like: sub pay_or_no { if (f{}) { pay(1000); }

In this fashion, Omega can verify the algorithm that returns the millionth digit of pi, independently verify the algorithm that pays based on that return, and our protagonist gets his money.

!!!!

This seems to be the correct answer to jacobt’s question. The key is looking at the length of proofs. The general rule should go like this: when you’re trying to decide which of two impossible counterfactuals “a()=x implies b()=y” and “a()=x implies b()=z” is more true even though “a()=x” is false, go with the one that has the shorter proof. We already use that rule when implementing agents that compute counterfactuals about their own actions. Now we can just implement Omega using the same rule. If the millionth digit of pi is in fact odd, but the statement “millionth digit of pi is even ⇒ agent pays up” has a much shorter proof than “millionth digit of pi is even ⇒ agent doesn’t pay up”, Omega should think that the agent would pay up.

The idea seems so obvious in retrospect, I don’t understand how I missed it. Thanks!

This seems equivalent to:

But does that make sense? What if it were possible to have really short proofs of whether the n-th digit of pi is even or odd and it’s impossible for the agent to arrange to have a shorter proof of “millionth digit of pi is even ⇒ agent pays up”? Why should the agent be penalized for that?

Maybe the whole point of a logical coinflip is about being harder to prove than simple statements about the agent. If the coinflip were simple compared the the agent, like “1!=1”, then a CDT agent would not have precommitted to cooperate, because the agent would have figured out in advance that 1=1. So it’s not clear that a UDT agent should cooperate either.

I agree, this seems like a reasonable way of defining dependencies between constant symbols. In case of logical uncertainty, I think you’d want to look into how relative lengths of proofs depend on adding more theorems as axioms (so that they don’t cost any proof length to use). This way, different agents or an agent in different situations would have different ideas about which dependencies are natural.

This goes all the way back to trying to define dependencies by analogy with AIXI/K-complexity, I think we were talking about this on the list in spring 2011.

Good point, thanks. You’re right that even-world looks just as impossible from odd-world’s POV as odd-world looks from even-world, so Omega also needs to compute impossible counterfactuals when deciding whether to give you the million. The challenge of solving the problem now looks very similar to the challenge of formulating the problem in the first place :-)

I pointed out the same issue before, but it doesn’t seem to affect my bargaining problem.

Why not? It seems to me that to determine that the staple maximizer’s offer is fair, you need to look at the staple maximizer’s assessment of you in the impossible world where it gets control. That’s very similar to looking at Omega’s assessment of you in the impossible world where it’s deciding whether to give you the million. Or maybe I’m wrong, all this recursion is making me confused...

What I meant is, in my version of the problem, you don’t have to solve the problem (say what Omega does exactly) in order to formulate the problem, since “the staple maximizer’s assessment of you in the impossible world where it gets control” is part of the solution, not part of the problem specification.