Editing Post's theorem (section)

===Formalization of Turing machines in first-order arithmetic===
The operation of a [[Turing machine]] <math>T</math> on input <math>n</math> can be formalized logically in [[first-order arithmetic]]. For example, we may use [[First-order_logic#Non-logical_symbols|symbol]]s <math>A_k</math>, <math>B_k</math>, and <math>C_k</math> for the tape configuration, machine state and location along the tape after <math>k</math> steps, respectively. <math>T</math>'s [[transition system]] determines the relation between <math>(A_k,B_k,C_k)</math> and <math>(A_{k+1},B_{k+1},C_{k+1})</math>; their initial values (for <math>k=0</math>) are the input, the initial state and zero, respectively. The machine halts if and only if there is a number <math>k</math> such that <math>B_k</math> is the halting state.

The exact relation depends on the specific implementation of the notion of Turing machine (e.g. their alphabet, allowed mode of motion along the tape, etc.)

In case <math>T</math> halts at time <math>n_1</math>, the relation between <math>(A_k,B_k,C_k)</math> and <math>(A_{k+1},B_{k+1},C_{k+1})</math> must be satisfied only for k bounded from above by <math>n_1</math>.

Thus there is a formula <math>\varphi(n,n_1)</math> in [[first-order arithmetic]] with no un[[bounded quantifier]]s, such that <math>T</math> halts on input <math>n</math> at time <math>n_1</math> at most if and only if <math>\varphi(n,n_1)</math> is satisfied.