Typical forcings, NP search problems and an extension of a theorem of Riis (Q2659102)

One of the central results in proof complexity is Ajtai's theorem. In model-theoretic terms it states that there is a model of \(I\Delta_0\) plus a predicate that codes an injective map from \(n\) into \(n\) that is not surjective (for some nonstandard n). This has later been quantitatively improved to full bounded arithmetic \(T_2\). Besides the pigeonhole principle, only a few other principles are known to be, in this sense, independent of \(T_2\). A celebrated theorem of Riis is proved by a forcing-type argument and gives a general criterion for independence from the weaker theory \(T^1_2\). The criterion is simply that the principle fails in some infinite model (like the pigeonhole principle). The current paper extends Riis' theorem and shows that strong principles are independent from \(T^1_2\) extended with a weak principle. Being weak or strong are simple combinatorial properties. This is proved as an application of a general forcing method. The provability or independence of principles in bounded arithmetics is tightly connected to the computational complexity of associated total NP search problems. The paper covers this connection in some detail and gives some improvements of earlier results.