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