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