Bounded arithmetic and truth definition (Q1107528)

\(S^1_2\) is S. Buss' system of bounded arithmetic. \(S^1_2\) is the union o f theories \(S^ i_2\) which differ by the number of bounded but not sharply bounded quantifiers in formulas allowed in appropriate induction schemes. One of the most important problems is whether the theories \(S^ i_2\) form a proper hierarchy. This paper explores possibilities of deciding this question with the aid of the classical machinery of Gödel sentences applied to some special consistency notions for subsystems of \(S^1_2\). \(S^ i_{2,n}\) is obtained from \(S^ i_2\) by adding to the language the function \(x\#\mathstrut^ n_3 y\) defined as \(\exp(| x| \# | y|_ n)\) where \(| y|_ n\) is \(\log_2(y+1)\) iterated \(n\) times. The new functions provide bounds that are needed to define values of formalized terms of \(S^ i_2\) whose Gödel numbers are \(n\)-small i.e. equal to \(| u|_ n\) for some \(u\). Consequently a truth formula for \(S^ i_2\) is constructed in \(S\) \(i_{2,n}\) together with a Gödel sentence which is provable in \(S_{2,n}^{i+1}\) but not in \(S^ i_2\). Variants of the second incompleteness theorem follow. \(\overset\circ U^1_2\) and \(\overset\circ T^1_2\) are Buss' systems of second order bounded arithmetic related to PSPACE and EXPTIME respectively. It is shown that \(\overset\circ U^1_2\) has a truth formula for sharply bounded formulas of \(S^1_2\) and \(\overset\circ V^1_2\) has a truth formula for \(\Sigma^ b_1\)-formulas. It follows that \(\overset\circ U^1_2\) is not a conservative extension of \(\tilde S^0_2\) (a system for sharply bounded formulas defined in the paper) and \(\overset\circ V^1_2\) is not a conser vative extension of \(S^1_2\).