Can this problem be solved by adjusting maximal length of checked proofs such that unprovability of proves(“A()==”Defect” && B()=”Cooperate”″, maxDC) is provable by proves(..., maxsteps)?
Yes, that occurred to me too, and I think it does the job.
I wonder if there are theorems of the form “There’s no significantly better way to show that P isn’t provable in N steps than by listing all proofs of length N and observing that P isn’t proved”. Then of course maxsteps would need to be exponential in maxDC.
On the other hand the fact that proves(“A()==”Cooperate” && B()==”Cooperate”″) was called means that A()==”Defect” && B()==”Cooperate” is unprovable under maxDC proof length. The question is can this fact be used in proof. The proof checker can be programmed to add such self-evident propositions into set of axioms, but I can’t clearly see consequences of this. And I have a bad feeling of mixing meta- and object levels.
I’m not sure if your idea will work, but have some notation to help you avoid mixing the levels. Here’s how you say “try to prove this fact conditional on some other fact”:
function main()
{
if (proves(outputs(1), n1))
return 1;
else if (proves("implies(!proves(outputs(1), n1), eval(outputs(2)))", n2))
return 2;
else
return 0;
}
OK, so first we try to prove P1 = “A()==”Defect” && B()==”Cooperate”“ using some theory T, then on failing that, we try to prove P2 = “A()==”Cooperate” && B()==”Cooperate”” using the augmented theory T’ = T + “T cannot prove P1 in maxDC steps”.
And then T’ can prove that “If T’ proves P2 then P2 is true”.
And note that the number of steps doesn’t matter any more.
“P isn’t provable in N steps” is in Co-NP. Since in general it’s an open question whether P=Co-NP, there might be a polynomial time algorithm to solve it, or their might not, respectively.
On the other hand, if you
1) Showed some large class of particular problems (ones that can reduced to from [no typo there] nonequivalent SAT instances, which I suspect is most of them) weren’t provable in N=cP steps IF it’s unprovable, then
2) You would have shown a sufficiently large class of SAT problems weren’t easily solvable in N=kP steps,
3) which would imply P!=NP (and also P!=Co-NP).
If on the other hand your whole class of problems is unprovable, then you can prove P isn’t provable by your theorem, which is presumably smaller than N in this context.
So, in summary my guess interesting classes of P, your question is equivalent to “Does P=NP?”, which we know is a tough nut to crack.
Can this problem be solved by adjusting maximal length of checked proofs such that unprovability of proves(“A()==”Defect” && B()=”Cooperate”″, maxDC) is provable by proves(..., maxsteps)?
Yes, that occurred to me too, and I think it does the job.
I wonder if there are theorems of the form “There’s no significantly better way to show that P isn’t provable in N steps than by listing all proofs of length N and observing that P isn’t proved”. Then of course maxsteps would need to be exponential in maxDC.
On the other hand the fact that proves(“A()==”Cooperate” && B()==”Cooperate”″) was called means that A()==”Defect” && B()==”Cooperate” is unprovable under maxDC proof length. The question is can this fact be used in proof. The proof checker can be programmed to add such self-evident propositions into set of axioms, but I can’t clearly see consequences of this. And I have a bad feeling of mixing meta- and object levels.
I’m not sure if your idea will work, but have some notation to help you avoid mixing the levels. Here’s how you say “try to prove this fact conditional on some other fact”:
OK, so first we try to prove P1 = “A()==”Defect” && B()==”Cooperate”“ using some theory T, then on failing that, we try to prove P2 = “A()==”Cooperate” && B()==”Cooperate”” using the augmented theory T’ = T + “T cannot prove P1 in maxDC steps”.
And then T’ can prove that “If T’ proves P2 then P2 is true”.
And note that the number of steps doesn’t matter any more.
So perhaps Nesov’s idea was OK all along?
“P isn’t provable in N steps” is in Co-NP. Since in general it’s an open question whether P=Co-NP, there might be a polynomial time algorithm to solve it, or their might not, respectively.
On the other hand, if you 1) Showed some large class of particular problems (ones that can reduced to from [no typo there] nonequivalent SAT instances, which I suspect is most of them) weren’t provable in N=cP steps IF it’s unprovable, then 2) You would have shown a sufficiently large class of SAT problems weren’t easily solvable in N=kP steps, 3) which would imply P!=NP (and also P!=Co-NP).
If on the other hand your whole class of problems is unprovable, then you can prove P isn’t provable by your theorem, which is presumably smaller than N in this context.
So, in summary my guess interesting classes of P, your question is equivalent to “Does P=NP?”, which we know is a tough nut to crack.