Edit: So the reason we don’t get the 5-and-10 problem is that we don’t get ☐(☐(A=5=>U=5 /\ A=10=>U=0) ⇒ (A=5=>U=5) /\ A=10=>U=0), because ☐ doesn’t have A’s source code as an axiom. Okay. (Seems like this solves the problem by reintroducing a cartesian barrier by which we can cleanly separate the decision process from all else.) (My own favorite solution A = argmax_a(max_u(☐(A=a=>U>=u))) also makes ☐ unable to predict the outcome of A’s sourcecode, because ☐ doesn’t know it won’t find a proof for A=10=>U>=6.)
How would f() map 10 to 0? Wouldn’t that require that from
A() := 10
U() :=
if A() = 10
return 10
if A() = 5
return 5
there’s a proof of
U() = 0
?
My understanding is that in the original formulation, the agent takes it’s own definition along with a description of the universe and looks for proofs of the form
[A() = 10 -> U() = x] & [A() = 5 -> U() = y ]
But since “A()” is the same in both sides of the expression, one of the implications is guaranteed to be vacuously true. So the output of the program depends on the order in which it looks for proofs. But here f looks for theorems starting from different axioms depending on it’s input, so “A()” and “U()” in f(5) can be different than “A()” and “U()” when f(10).
Edit: So the reason we don’t get the 5-and-10 problem is that we don’t get ☐(☐(A=5=>U=5 /\ A=10=>U=0) ⇒ (A=5=>U=5) /\ A=10=>U=0), because ☐ doesn’t have A’s source code as an axiom. Okay. (Seems like this solves the problem by reintroducing a cartesian barrier by which we can cleanly separate the decision process from all else.) (My own favorite solution A = argmax_a(max_u(☐(A=a=>U>=u))) also makes ☐ unable to predict the outcome of A’s sourcecode, because ☐ doesn’t know it won’t find a proof for A=10=>U>=6.)
How would f() map 10 to 0? Wouldn’t that require that from
there’s a proof of
?
My understanding is that in the original formulation, the agent takes it’s own definition along with a description of the universe and looks for proofs of the form
But since “A()” is the same in both sides of the expression, one of the implications is guaranteed to be vacuously true. So the output of the program depends on the order in which it looks for proofs. But here f looks for theorems starting from different axioms depending on it’s input, so “A()” and “U()” in f(5) can be different than “A()” and “U()” when f(10).