Editing Post's theorem (section)

===Oracle machines===

Similarly, the operation of an [[oracle machine]] <math>T</math> with an oracle O that halts after at most <math>n_1</math> steps on input <math>n</math> can be described by a first-order formula <math>\varphi_O(n,n_1)</math>, except that the formula <math>\varphi_1(n,n_1)</math> now includes:
* A new predicate, <math>O_m</math>, giving the oracle answer. This predicate must satisfy some formula to be discussed below.
* An additional tape - the oracle tape - on which <math>T</math> has to write the number m for every call O(m) to the oracle; writing on this tape can be logically formalized in a similar manner to writing on the machine's tape. Note that an oracle machine that halts after at most <math>n_1</math> steps has time to write at most <math>n_1</math> digits on the oracle tape. So the oracle can only be called with numbers m satisfying <math>m<2^{n_1}</math>.

If the oracle is for a decision problem, <math>O_m</math> is always "Yes" or "No", which we may formalize as 0 or 1. Suppose the decision problem itself can be formalized by a first-order arithmetic formula <math>\psi^O(m)</math>.
Then <math>T</math> halts on <math>n</math> after at most <math>n_1</math> steps if and only if the following formula is satisfied:
<math>\varphi_O(n,n_1) =\forall m<2^{n_1}:((\psi^O(m)\rightarrow (O_m=1)) \land(\lnot\psi^O(m)\rightarrow (O_m=0))) \land {\varphi_O}_1(n,n_1)</math>

where <math>{\varphi_O}_1(n,n_1)</math> is a first-order formula with no unbounded quantifiers.