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