This chapter presents important definability results for fragments of bounded arithmetic.

A Turing machine M will be given by its set of states Q, the alphabet Σ, the number of working tapes, the transition function, and its clocks, that is, an explicit time bound. Most results of the form “Given machine M the theory T can prove …” could be actually proved in a bit stronger form: “For any k the theory T can prove that for any M running in time ≥ nk …” A natural formulation for such results is in terms of models of T and computations within such models, but in this chapter we shall omit these formulations.

An instantaneous description of a computation of machine M on input x consists of the current state, the positions of the heads, the content of all tapes, and the current time: That is, it is a sequence of symbols whose length is proportional to the time bound for n:= |x|.

A computation will be coded by the sequence of the consecutive instantaneous descriptions.

Now we shall consider several bounded formulas defining these elementary concepts. They are all in the language L+ and thus also (by Lemma 5.4.1) in L.