On the metamathematics of the P vs. NP question

We review the work (from 1976 to 1996) by several researchers on the metamathematics of P vs. NP. That work points towards the possibility that, given some strong consistent axiomatic system S with a recursively enumerable set of theorems which includes arithmetic, for the Σ2 sentence [P=NP][P=NP] that formalizes the P=NPP=NP hypothesis, S+[P=NP]S+[P=NP] is consistent. We consider the work of several authors like for instance [J. Hartmanis, J. Hopcroft, Independence results in computer science, SIGACT News 13 (1976); M. O’Donnell, A programming language theorem which is independent of Peano Arithmetic, in: Proceedings of the 11th Annual ACM Symposium on the Theory of Computation, 1979, pp. 176–188; R.A. DeMillo, R.J. Lipton, The consistency of P = NP and related problems with fragments of number theory, in: Proceedings of the 12th Annual ACM Symposium on the Theory of Computing, 1980, pp. 45–57; D. Joseph, P. Young, Fast programs for initial segments and polynomial time computation in weak models of arithmetic, STOC Milwaukee 1981, 1981, pp. 55–61; W. Kowalczyk, A sufficient condition for the consistency of P = NP with Peano Arithmetic, Fund. Inform. 5 (1982) 233–245]. We then relate all those results to the [N.C.A. da Costa, F.A. Doria, Consequences of an exotic formulation for P = NP  , Appl. Math. Comput. 145 (2003) 655–665, also “Addendum” 172 (2006) 1364–1367] conditional consistency result for ZFC+[P=NP]ZFC+[P=NP] and elaborate on it.