= 27d567bc2d48d9f40e9ccc20ea370b15)
Kindly comments on A model of UDT with a halting oracle - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (100)
A will check for one of those first, and then return it. The order in which it checks 1 and 2 doesn't matter, because this can only happen if S is unsound.
So, the primary point is to make it trivial to show that there is no proof in S regarding the output of A?
Exactly. We're worried about proving something like "A()=1 ⇒ U()=0" by proving "A()≠1", which would convince A() not to return 1. This avoids shortcuts of that nature.
So, in the example given, it is clear that A()=1. and also clear that S cannot prove that A()=1. What system are we using to show that A()=1, and why do we believe that that system is sound?
EDIT: More generally, is there any sound formal system T which can prove that A()=1 for all sound formal systems S that can prove that A()=1 ⇒ U()=1000000 and A()=2 ⇒ U()=1000?
If so, then T cannot prove that A()=1 ⇒ U()=1000000 and A()=2 ⇒ U()=1000, why do we believe that? If not, why do we believe that A()=1?
Presumably whichever system one typically uses to reason about the soundness of Peano arithmetic would suffice.
Considering that the algorithm involved is already impossible to implement by virtue of calling a halting oracle, I don't see what further harm it does to make the additional assumption that Peano arithmetic is sound.
The provable oracle is only needed for the general case implementation: If you have a proof that S does not prove A()≠n for any n, and a the further proofs that A()=n ⇒ U()=u for each n, then the need for the oracle is satisfied. If you replace the oracle with a routine which sometimes breaks down and cries, this specific example might still work.
What I'm saying is that either there exists a sound system which can prove the three statements A()=1, A()=1 ⇒ U()=1000000 and A()=2 ⇒ U()=1000, or there does not exist such a sound system. If such a system exists, then it does not prove that A()=1 ⇒ A()≠2 (or any other value), and therefore does not contain Peano arithmetic. Since the proof here does make all three claims, either the system used here either does not contain PA or is unsound. Since PA is assumed whenever numbers are used, the system is unsound.
The claim that the algorithm will do the right thing in Newcomb's problem is suspect, because any formal system that can use the proof provided is unsound.
Why not?
Because such a system would prove that A()≠2, which would result in A() returning 2 in the first step, when that system is used as the system S. Since it proves something which is not true, it is unsound.
A sound system need not include the axioms of PA to include the axiom "Anything that PA proves is true".
Such a system T can be sound and still prove that A()=1, but cannot prove that A()=1 ⇒ A()≠2, because:
T does not contain the axiom A=n ⇒ A≠m, for m≠n. Therefore A()=1 ⇒ A()≠2 is not provable in T
PA does not prove (T proves A()=1 ⇒ A()≠2), and does not include the axiom "Anything that T proves is true." A()=1 is not provable in PA, and therefore A()≠2 is not provable in PA.
No sound system that can be used as S can prove that A()≠2: Since U only requires that S to be sound and be able to prove A()=a ⇒ U()=u for all permissible a, no sound system can prove A()=a ⇒ U()=u for all permissible a and A()≠2.
Wait, no, no, no. The system in which we are working to analyze the algorithm A() and prove that it works correctly is not the same as the system S used by A()! Although S is not powerful enough to prove A()≠2 -- this would require that S is aware of its own soundness -- we can pick a system S that we know is sound, or can assume to be sound, such as Peano arithmetic, and based on that assumption we can prove that A()=1.
What are the requirements of S? The only ones given is that S is a formal system and we know that S proves A()=a ⇒ U()=u for all permissible a.
Why does the system we are are using to evaluate A() not meet the requirements of S?
I understand the point is to formalize a system where we take the action which results in the best outcome, but why is it important that S not be able to prove that A()≠2 or A()≠1? No function can evaluate it's own output and use that as a factor in determining its output, and any counterfactual proof along the lines of
A()≠2 ⇒ (A()=2 ⇒ U()=3^^^3)
cannot force A() to return 2, because A()≠2 has already been proven.