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