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.
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.
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.
Just assume S is Peano arithmetic. Then the proof in the post is probably valid in something like ZFC.
Why does the system we are are using to evaluate A() not meet the requirements of S?
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.
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.
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.
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.
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.
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.
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).
It does imply that. What happens is that you (in “common sense” system) don’t prove A()=2 as a consequence of proving (say) both (A()=1 ⇒ U()=1000000) and (A()=2 ⇒ U()=3^^^3), since the value of A() is determined by what S can prove, not by what “common sense” can prove.
No, I’m using common sense both to evaluate A() and as S. In sound common sense, A()≠2 does not imply (A()=2 ⇒ U()=3^^^3).
That’s because in common sense A()=2 ⇒ U()=1000 is true and provable, and (A()=2 ⇒ U()=1000) implies (A()=2 ⇒ U()≠3^^^3)), and in common sense (A()=2 ⇒ U()≠3^^^3)) and (A()=2 ⇒ U()=3^^^3)) are contradicting statements rather than proof that A()≠2.
The soundness of common sense is very much in dispute, except in the case of common sense along with some basic axioms of fully described formal systems- common sense with those added axioms is clearly unsound.
In sound common sense, A()≠2 does not imply (A()=2 ⇒ U()=3^^^3).
Okay, then I don’t know what kind of reasoning system this “common sense” is or how to build an inference system that implements it to put as S in A(). As a result, discussing it becomes unfruitful unless you give more details about what it is and/or motivation for considering it an interesting/relevant construction.
(What I wanted to point out in the grandparent is that the wrong conclusion can be completely explained by reasoning-from-outside being separate from S, without reasoning-from-outside losing any standard properties.)
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
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.
It does imply that. What happens is that you (in “common sense” system) don’t prove A()=2 as a consequence of proving (say) both (A()=1 ⇒ U()=1000000) and (A()=2 ⇒ U()=3^^^3), since the value of A() is determined by what S can prove, not by what “common sense” can prove.
No, I’m using common sense both to evaluate A() and as S. In sound common sense, A()≠2 does not imply (A()=2 ⇒ U()=3^^^3).
That’s because in common sense A()=2 ⇒ U()=1000 is true and provable, and (A()=2 ⇒ U()=1000) implies (A()=2 ⇒ U()≠3^^^3)), and in common sense (A()=2 ⇒ U()≠3^^^3)) and (A()=2 ⇒ U()=3^^^3)) are contradicting statements rather than proof that A()≠2.
The soundness of common sense is very much in dispute, except in the case of common sense along with some basic axioms of fully described formal systems- common sense with those added axioms is clearly unsound.
Okay, then I don’t know what kind of reasoning system this “common sense” is or how to build an inference system that implements it to put as S in A(). As a result, discussing it becomes unfruitful unless you give more details about what it is and/or motivation for considering it an interesting/relevant construction.
(What I wanted to point out in the grandparent is that the wrong conclusion can be completely explained by reasoning-from-outside being separate from S, without reasoning-from-outside losing any standard properties.)