Editing Post's theorem (section)

===Implementation example===
For example, for a [[prefix code|prefix-free]] Turing machine with binary alphabet and no blank symbol, we may use the following notations:
*<math>A_k</math> is the 1-[[Arity|ary]] [[First-order_logic#Non-logical_symbols|symbol]] for the configuration of the whole tape after <math>k</math> steps (which we may write as a number with [[least significant bit|LSB]] first, the value of the m-th location on the tape being its m-th least significant bit). In particular <math>A_0</math> is the initial configuration of the tape, which corresponds the input to the machine.
*<math>B_k</math> is the 1-[[Arity|ary]] symbol for the Turing machine state after <math>k</math> steps. In particular, <math>B_0=q_I</math>, the initial state of the Turing machine.
*<math>C_k</math> is the 1-[[Arity|ary]] symbol for the Turing machine location on the tape after <math>k</math> steps. In particular <math>C_0=0</math>.
* <math>M(q,b)</math> is the transition function of the Turing machine, written as a function from a doublet (machine state, bit read by the machine) to a triplet (new machine state, bit written by the machine, +1 or -1 machine movement along the tape).
*<math>bit(j,m)</math> is the j-th bit of a number <math>m</math>. This can be written as a first-order arithmetic formula with no unbounded quantifiers.

For a [[prefix code|prefix-free]] Turing machine we may use, for input n, the initial tape configuration <math>t(n)= cat(2^{ceil(log_2 n)}-1,0,n)</math> where cat stands for concatenation; thus <math>t(n)</math> is a <math>\log(n)-</math>length string of <math>1-s</math> followed by <math>0</math> and then by <math>n</math>. 

The operation of the Turing machine at the first <math>n_1</math> steps can thus be written as the conjunction of the initial conditions and the following formulas, quantified over <math>k</math> for all <math>k<n_1</math>:
*<math>(B_{k+1}, bit(C_k ,A_{k+1}), D) = M(B_k, bit(C_k ,A_k))</math>. Since M has a finite domain, this can be replaced by a first-order [[Quantifier-free formula|quantifier-free]] arithmetic formula. The exact formula obviously depends on M.
*<math>C_{k+1} = C_k+D</math> 
*<math>\forall j: j\ne C_k \rightarrow bit(j ,A_{k+1}) = bit(j ,A_k)</math>. Note that at the first <math>n_1</math> steps, <math>T</math> never arrives at a location along the tape greater than <math>n_1</math>. Thus the [[universal quantifier]] over j can be [[bounded quantifier|bounded]] by <math>n_1</math>+1, as bits beyond this location have no relevance for the machine's operation.

T 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, where:
:<math>\begin{align}\varphi(n,n_1) =& (A_0=t(n)) \land (B_0=q_I) \land (C_0=0) \land (B_{n_1}=q_H)\\ &\land \forall k<n_1: ((B_{k+1},bit(C_k,A_{k+1}),1) = M(B_k,bit(C_k,A_k)) \land C_{k+1}=C_k+1)&\\ &\lor ((B_{k+1},bit(C_k ,A_{k+1}),-1) = M(B_k,bit(C_k,A_k)) \land C_{k+1}=C_k-1))& \\&\land \forall j<n_1+1: j\ne C_k \rightarrow (bit(j,A_{k+1})=bit(j,A_k)) & \end{align}</math>

This is a first-order arithmetic formula with no unbounded quantifiers, i.e. it is in <math>\Sigma^0_0</math>.