Truth Definition For Delta(0) Formulas And Pspace Computations

One of the long-standing open problems in bounded arithmetic is whether there exists a truth definition for bounded formulas which does not use the exponentiation function. We relate the existence of a sufficiently good truth definition for bounded formulas in a given theory T to the representation of PSPACE computations. Also, we show that an extension of Buss's theory S-2(1) with such a truth definition admits a PSPACE witnessing theorem.