Truth definition for $\Delta _ 0$ formulas and PSPACE computations
Volume 252 / 2021
Fundamenta Mathematicae 252 (2021), 1-38
MSC: 03F30, 03F35, 68Q15.
DOI: 10.4064/fm578-1-2020
Published online: 3 July 2020
Abstract
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 $\textrm {PSPACE}$ computations. Also, we show that an extension of Buss’s theory $S^1_2$ with such a truth definition admits a $\textrm {PSPACE}$ witnessing theorem.