Thanks for the analysis. I’ll try to clarify those points, then.
Of course, I’m not suggesting my answer as a solution to the prisoner’s dilemma. I actually don’t think this kind of mathematical analysis is even relevant to the prisoner’s dilemma in practice—I think the latter is best dealt with by pre-commitments, reputation tracking etc. to change the payoff matrix and in particular change the assumption that the interaction is one-off—which it typically isn’t anyway. (Note that in cases involving actual criminals, we need witness protection programs to make it even approximately one-off.)
As for the logic engine, hey, I just unrolled the search loop then deleted 3^^^^3 − 1 lines of unreachable code. No different than optimizing compilers do every day :-)
If we look at the logic puzzle aspect though, this is in similar vein to this statement is true (the reverse of the classic this statement is false liar paradox—it has two consistent solutions instead of none—note that return 0 is just as valid a solution as return 1).
And if you ask what sort of proof system permits that, you start investigating higher-order logic, and self-reference, and the classic paradoxes thereof, and type theory and other possible solutions thereto, which are topics that are of very real significance to software verification and other branches of AI.
In summary, I think this puzzle goes places interesting enough that it’s actually worth taking apart and analyzing.
Actually, this statement is provable. This is the “Henkin sentence” and it is indeed provable in Peano arithmetic, so no need for stronger things like type theory etc. My proof in 1 is basically a translation of the proofs of the Henkin sentence and Löb’s theorem (which is used to prove the former).
Yes, in that sense you’re right, this is isomorphic to the Henkin sentence, which is provable in first-order Peano arithmetic, if you set everything up just right in terms of precisely chosen axioms and their correspondence to the original code. (Note that there is no guarantee of such correspondence—return 0 is, after all, also a correct solution to the problem.)
But the metaproof in which you showed this, and the sketch you gave of how you would go about implementing it, are not written in first-order PA. And by the time you have actually written out all the axioms, implemented the proof checker etc., it will be apparent that almost all the real work is not being done on the computer, but in your brain, using methods far more powerful than first-order PA.
If we don’t regard this as a problem, then we should be willing to accept return 1 as a solution. But if we do regard this as a problem (and I think we should; apart from anything else, it means nearly all problems that would benefit from formal solution, don’t actually receive such, because there just isn’t that much skilled human labor to go around—this problem is itself an example of that; you didn’t have time to more than sketch the implementation) then we have to climb the ladder of more powerful formal techniques.
Thanks for the analysis. I’ll try to clarify those points, then.
Of course, I’m not suggesting my answer as a solution to the prisoner’s dilemma. I actually don’t think this kind of mathematical analysis is even relevant to the prisoner’s dilemma in practice—I think the latter is best dealt with by pre-commitments, reputation tracking etc. to change the payoff matrix and in particular change the assumption that the interaction is one-off—which it typically isn’t anyway. (Note that in cases involving actual criminals, we need witness protection programs to make it even approximately one-off.)
As for the logic engine, hey, I just unrolled the search loop then deleted 3^^^^3 − 1 lines of unreachable code. No different than optimizing compilers do every day :-)
If we look at the logic puzzle aspect though, this is in similar vein to this statement is true (the reverse of the classic this statement is false liar paradox—it has two consistent solutions instead of none—note that return 0 is just as valid a solution as return 1).
And if you ask what sort of proof system permits that, you start investigating higher-order logic, and self-reference, and the classic paradoxes thereof, and type theory and other possible solutions thereto, which are topics that are of very real significance to software verification and other branches of AI.
In summary, I think this puzzle goes places interesting enough that it’s actually worth taking apart and analyzing.
Actually, this statement is provable. This is the “Henkin sentence” and it is indeed provable in Peano arithmetic, so no need for stronger things like type theory etc. My proof in 1 is basically a translation of the proofs of the Henkin sentence and Löb’s theorem (which is used to prove the former).
Yes, in that sense you’re right, this is isomorphic to the Henkin sentence, which is provable in first-order Peano arithmetic, if you set everything up just right in terms of precisely chosen axioms and their correspondence to the original code. (Note that there is no guarantee of such correspondence—return 0 is, after all, also a correct solution to the problem.)
But the metaproof in which you showed this, and the sketch you gave of how you would go about implementing it, are not written in first-order PA. And by the time you have actually written out all the axioms, implemented the proof checker etc., it will be apparent that almost all the real work is not being done on the computer, but in your brain, using methods far more powerful than first-order PA.
If we don’t regard this as a problem, then we should be willing to accept return 1 as a solution. But if we do regard this as a problem (and I think we should; apart from anything else, it means nearly all problems that would benefit from formal solution, don’t actually receive such, because there just isn’t that much skilled human labor to go around—this problem is itself an example of that; you didn’t have time to more than sketch the implementation) then we have to climb the ladder of more powerful formal techniques.
And once again I will ask the downvoters, which part of my comment do you disagree with?