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