= 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)
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.
Just assume S is Peano arithmetic. Then the proof in the post is probably valid in something like ZFC.
The algorithm would work fine if S were ZFC, it's just that then we would need to talk about the soundness of ZFC in the proof.
We're not worried about that kind of counterfactual proof, for the reasons you give. We're worried about self-fulfilling counterfactual proofs. Suppose A() proves that A()=1, then concludes that box2 = 0, and uses that to prove that 1 is the best thing to return. This isn't impossible, because everything S proves did turn out to be correct; it just leads to A() one-boxing.
Can this scenario be established in ZFC or PA?
How do you prove A()=1 without proving that A()=1?
Where P(V) designates the existence of a proof in S that V is true:
P(V)⇒V (because S is sound)
P(A()=1) ⇒ P(A()≠2) ⇒ P((A()=2 ⇒ U()=3^^^3)) (counterfactual)
P(A()=2 ⇒ U()=3^^^3) ∪ P(A()1=⇒ U()=1000000) ⇒ A()=2 (because A() will return the a with the highest proven U())
∴ P(A()=1) ⇒ A()=2 ∴ S cannot prove that A()=1 unless S is unsound
UNLESS: we have a system S which cannot prove a counterfactual; in such a system A()≠2 does not imply (A()=2 ⇒ U()=3^^^3) Since counterfactuals are not useful, I don't see a disadvantage in not being able to prove them.
I find myself unable to parse this.
Edit: but I think I know what the problem is anyway. Although A() could eventually find a proof of A()=2 ⇒ U()=3^^^3 if there is a proof of A()≠2, it could also find a proof of A()=2 ⇒ U()=-3^^^3, because it's not specified which order the proofs will be checked in.
However, if we ensure that no proof of A()≠2 exists, then there exists at most one u, for which S proves that A()=a ⇒ U()=u. This means that the above isn't a problem.
S proves A()=1 implies S proves A()≠2
S proves A()≠2 implies that S proves (A()=2 ⇒ U()=3^^^3)
(S proves (A()=2 ⇒ U()=3^^^3), union with S proves (A()=1⇒ U()=1000000)), implies that A()=2
Therefore, if S proves A()=1, then A()=2