What are the ∀∑1b-consequences of T21 and T22? Original Research Article

We formulate schemes (M1) and (M2) of the “typical” ∀∑1b-sentences that are provable in T21, respectively T22. As an application, we reprove a recent result of Buss and Krajíček (1994) which describes witnesses for the ∀∑1b-sentences provable in T21 in terms of solutions to PLS-problems.