A nonasymptotic lower time bound for a strictly bounded second-order arithmetic

We obtain a nonasymptotic lower time bound for deciding sentences of bounded second-order arithmetic with respect to a form of the random access machine with stored programs. More precisely, let P be an arbitrary program for the model under consideration which recognized true formulas with a given range of parameters. Let p be the length of P and let N be an arbitrary natural number. We show how to construct a formula G ( x ) with one free variable with length not more than 400 symbols (where each constant is considered as one symbol) and a value f of x such that the time required by P to decide the truth of G ( f ) is at least N + 1 steps. Furthermore, the G constructed does not depend on P and the length of f is less than p + 400 .