Definability of computations
Jan Krajı́ček · Cambridge University Press eBooks · 1995
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 ≥ n k …” 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 .