Search is never called on (M,M), only on (M,FB) and (M,DB). (And of course all combinations of FB and DB.)
If M(M)=C is provable in PA+i, then M(M) returns D.
Which proof is broken, and why? This is a case where intuiting what the agent will do, without proving it, is unreliable; it’s not very feasible for humans to consciously grok the ramifications of a depth-five stack of “I know that they know that I know...”
Lemma 8: “Masquerade(FB)=C” and “FB(Masquerade)=C” are provable in PA+3.
And your proof of that claim is simply proof that “Masquerade(FB)=D” and “FB(Masquerade)=D” are not true in PA+3.
Proof: Lemmas 5 and 6, and the consistency of PA+2, imply that when Masquerade arrives at the sanity-check stage, it has the variables set as utility=U(C,C), my_move=C and their_move=C. Thus PA+3 can prove that “if ‘FB(M)=C’ is provable in PA+3, then M(FB)=C”. And of course, “if ‘M(FB)=C’ is provable in PA+3, then FB(M)=C” is provable in PA+3, since again PA+3 can prove that PA through PA+2 won’t have found proofs of contrary conclusions before it gets around to trying to find cooperation in PA+3. Therefore we have the desired Löbian cycle!
However, “if ‘FB(M)=D’ is provable in PA+3, then M(FB)=D”. And of course, “if ‘M(FB)=D’ is provable in PA+3, then FB(M)=D” is provable in PA+3…
For PA+3 to be consistent, then it cannot prove that FB(M)=D and FB(M)=C. Since it cannot prove one but not the other, and the proofs are identical, it cannot prove either.
However, “if ‘FB(M)=D’ is provable in PA+3, then M(FB)=D”.
Are you claiming that this is provable in PA+3? How?
As the proof of Lemma 8 says, by the time we reach the sanity-check stage, we have my_move == their_move == C, and PA+3 knows this. Thus, in the sanity-check stage, Masquerade looks for a proof of ‘FB(M)=C’ in any of the PA+i (i<N), and if it finds one, it returns C. Thus, to show that M(FB)=D, PA+3 would need to conclude that “PA+3 does NOT prove ‘FB(M)=C’—and neither does PA+4, … PA+(N-1).” I don’t see how it’s supposed to do that?
And of course, “if ‘M(FB)=D’ is provable in PA+3, then FB(M)=D” is provable in PA+3...
I don’t see this one, either. FairBot looks for proofs of ‘M(FB)=C’ in PA, PA+1, PA+2 and PA+3 before it gets around to looking for proofs of ‘M(FB)=D’ in PA+3. Therefore, to conclude “FB(M)=D” from “PA+3 proves ‘M(FB)=C’”, it would seem that PA+3 must first conclude that “‘M(FB)=C’ is NOT provable in PA+3”; and again, I do not see how it would do that.
You aren’t trying to develop a new strategy, you are trying to select from one or more already existing strategies based on which one is optimal. You do this by finding where the biggest proven payoff is and then emulating the behavior among your potential strategies that results in the highest payoff. It doesn’t generalize well because you ask PA+i what your partner will do against each of the other potential strategies, but only emulate those strategies if PA+i proves that they also would do that against you. In cases where the complexity of the other decision maker were significant, Masquerade would always fall back on its default- try writing a few RPS programs, that need to throw Rock, Paper Scissors against each other and have access to each other’s source code but not random numbers. Payoffs for a win are 3-0, for a tie 2-2.
M(M)=C IFF PA+i proves that M(M)=C. PA+i proves that M(M)=C IFF (PA proves M(M)=C or PA+i proves M(M)≠D)
M(M)=C IFF PA proves that M(M)=C or PA proves M(M)≠D.
I’m probably missing some magic property of PA+i in that simplification, but otherwise it’s the last three lines of your program, given that the sanity check is checking for C,C.
Thank you. You have finally proven to me that Lob’s theorem is as absurd as it sounds on the face of it. If PA+i can prove “If
You have finally proven to me that Lob’s theorem is as absurd as it sounds on the face of it.
When math seems absurd to you, this is generally a signal that you’ve got something interesting to learn, rather than that you’ve got a superior epistemic vantage point to mathematics.
No, seriously, this stuff is awesome and you should check it out. I’m realizing that I need a better grasp of it in order to write it up, so I’m checking out The Logic of Provability on Monday.
Oh, I agree that it’s true in mathematics. I just recognize that things which are proven within a strict construction of mathematics might not apply outside that strict interpretation.
It’s the intersection between Godel and Lob’s theorems that really throws me off- anything which is not false in PA can be proven in PA, including nonce statements, but there are things that are true in PA which cannot be proven in PA, and there is a mechanism for generating such statements.
Consider the statement G: “G cannot be proven in PA”. G is proven in PA+1, because if PA were to have a proof of G, then G would be false and PA would prove something which is false. So far, so good- but PA proves that PA+1 proves G; since the only axiom in PA+1 not in PA is “PA is sound”, PA proves that “PA is sound->G is true”.
If PA is not sound, then PA proves G is true. (trivial, since an unsound system proves everything)
PA is either (sound or not sound).
PA proves (if PA is sound, G is true.)
PA proves that (if PA is not sound, PA proves that G is true)
(PA proves that G is true) within PA implies G is true.
PA proves that G is true If PA is (sound or unsound).
PA proves that G is true.
PA proves that PA is not sound.
I’m not sure if I’m literally only using the axiom “S is either sound or not sound” to prove “S proves that S is not sound”. I’m sure that the principle of explosion requires a few axioms more, and that I’ve made a (common?) fatal error somewhere, but I’m comfortable with calling mathematical constructions “Absurd” without calling them false.
The best response to “X is absurd” is “Reality is absurd”, a point with which I will readily agree.
EDIT: Corrected a couple of major typos resulting in GCE, other errors are probably still present.
Search is never called on (M,M), only on (M,FB) and (M,DB). (And of course all combinations of FB and DB.)
Which proof is broken, and why? This is a case where intuiting what the agent will do, without proving it, is unreliable; it’s not very feasible for humans to consciously grok the ramifications of a depth-five stack of “I know that they know that I know...”
Lemma 8: “Masquerade(FB)=C” and “FB(Masquerade)=C” are provable in PA+3.
And your proof of that claim is simply proof that “Masquerade(FB)=D” and “FB(Masquerade)=D” are not true in PA+3.
Proof: Lemmas 5 and 6, and the consistency of PA+2, imply that when Masquerade arrives at the sanity-check stage, it has the variables set as utility=U(C,C), my_move=C and their_move=C. Thus PA+3 can prove that “if ‘FB(M)=C’ is provable in PA+3, then M(FB)=C”. And of course, “if ‘M(FB)=C’ is provable in PA+3, then FB(M)=C” is provable in PA+3, since again PA+3 can prove that PA through PA+2 won’t have found proofs of contrary conclusions before it gets around to trying to find cooperation in PA+3. Therefore we have the desired Löbian cycle!
However, “if ‘FB(M)=D’ is provable in PA+3, then M(FB)=D”. And of course, “if ‘M(FB)=D’ is provable in PA+3, then FB(M)=D” is provable in PA+3… For PA+3 to be consistent, then it cannot prove that FB(M)=D and FB(M)=C. Since it cannot prove one but not the other, and the proofs are identical, it cannot prove either.
Are you claiming that this is provable in PA+3? How?
As the proof of Lemma 8 says, by the time we reach the sanity-check stage, we have my_move == their_move == C, and PA+3 knows this. Thus, in the sanity-check stage, Masquerade looks for a proof of ‘FB(M)=C’ in any of the PA+i (i<N), and if it finds one, it returns C. Thus, to show that M(FB)=D, PA+3 would need to conclude that “PA+3 does NOT prove ‘FB(M)=C’—and neither does PA+4, … PA+(N-1).” I don’t see how it’s supposed to do that?
I don’t see this one, either. FairBot looks for proofs of ‘M(FB)=C’ in PA, PA+1, PA+2 and PA+3 before it gets around to looking for proofs of ‘M(FB)=D’ in PA+3. Therefore, to conclude “FB(M)=D” from “PA+3 proves ‘M(FB)=C’”, it would seem that PA+3 must first conclude that “‘M(FB)=C’ is NOT provable in PA+3”; and again, I do not see how it would do that.
Oh, I see the premise now.
You aren’t trying to develop a new strategy, you are trying to select from one or more already existing strategies based on which one is optimal. You do this by finding where the biggest proven payoff is and then emulating the behavior among your potential strategies that results in the highest payoff. It doesn’t generalize well because you ask PA+i what your partner will do against each of the other potential strategies, but only emulate those strategies if PA+i proves that they also would do that against you. In cases where the complexity of the other decision maker were significant, Masquerade would always fall back on its default- try writing a few RPS programs, that need to throw Rock, Paper Scissors against each other and have access to each other’s source code but not random numbers. Payoffs for a win are 3-0, for a tie 2-2.
M(M)=C IFF PA+i proves that M(M)=C. PA+i proves that M(M)=C IFF (PA proves M(M)=C or PA+i proves M(M)≠D)
PA+i proves M(M)≠D IFF (PA proves M(M)≠D or PA+i proves M(M)=C)
M(M)=C IFF PA proves that M(M)=C or PA proves M(M)≠D.
I’m probably missing some magic property of PA+i in that simplification, but otherwise it’s the last three lines of your program, given that the sanity check is checking for C,C.
Thank you. You have finally proven to me that Lob’s theorem is as absurd as it sounds on the face of it. If PA+i can prove “If
When math seems absurd to you, this is generally a signal that you’ve got something interesting to learn, rather than that you’ve got a superior epistemic vantage point to mathematics.
No, seriously, this stuff is awesome and you should check it out. I’m realizing that I need a better grasp of it in order to write it up, so I’m checking out The Logic of Provability on Monday.
Oh, I agree that it’s true in mathematics. I just recognize that things which are proven within a strict construction of mathematics might not apply outside that strict interpretation.
It’s the intersection between Godel and Lob’s theorems that really throws me off- anything which is not false in PA can be proven in PA, including nonce statements, but there are things that are true in PA which cannot be proven in PA, and there is a mechanism for generating such statements.
Consider the statement G: “G cannot be proven in PA”. G is proven in PA+1, because if PA were to have a proof of G, then G would be false and PA would prove something which is false. So far, so good- but PA proves that PA+1 proves G; since the only axiom in PA+1 not in PA is “PA is sound”, PA proves that “PA is sound->G is true”.
If PA is not sound, then PA proves G is true. (trivial, since an unsound system proves everything)
PA is either (sound or not sound).
PA proves (if PA is sound, G is true.)
PA proves that (if PA is not sound, PA proves that G is true)
(PA proves that G is true) within PA implies G is true.
PA proves that G is true If PA is (sound or unsound).
PA proves that G is true.
PA proves that PA is not sound.
I’m not sure if I’m literally only using the axiom “S is either sound or not sound” to prove “S proves that S is not sound”. I’m sure that the principle of explosion requires a few axioms more, and that I’ve made a (common?) fatal error somewhere, but I’m comfortable with calling mathematical constructions “Absurd” without calling them false.
The best response to “X is absurd” is “Reality is absurd”, a point with which I will readily agree.
EDIT: Corrected a couple of major typos resulting in GCE, other errors are probably still present.