= 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)
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
Right, so I answered this in the edit before you made this reply, but just to reiterate: just because S proves (A()=2 ⇒ U()=3^^^3, and (A()=1⇒ U()=1000000), doesn't mean that A() will return 2. A() just seizes on the first values u1 and u2 for which S proves A()=1⇒U()=u1 and A()=2⇒U()=u2.
If we believe that S is sound, then these values will happen to be such that the utility for the one A() does return is correct: either A()=1 and u1=1000 (and u2 can be anything), or A()=2 and u2=1000000 (and u1 can be anything). However, we would like it to be true that u1=1000 and u2=1000000, no matter what A() returns, because this lets A() make the correct decision.
To do this,we play chicken. Now the counterfactual proofs we have been looking at die. However, the proof that A()=1⇒U()=1000 by looking at U()'s code sticks around. This ensures that this will be the proof that A() finds.
So long as the result of A() depends on what S can prove it's results imply, S cannot prove anything about the results of A() and still be sound. I demonstrated that if S is sound, it cannot prove that A()=1.
My confusion was in trying to apply an unsound system that is more general and native to me: Common sense, combined with a random assortment of logical statements that are true in PA but not in common sense.
Common sense proves that A()=1 easily, which implies A()≠2, but in sound common sense, A()≠2 does not imply (A()=2 ⇒ U()=3^^^3).
The system S "Sound common sense, plus the axiom 'Whatever PA proves is true'" works perfectly both for S and to prove that A()=1. It's just not yet possible to list all of the axioms of that system, nor to prove that we are working in that system at any time.