Example call of T1. The 1st argument gives the source code (in
C rather than as a
Gödel numbere) of a computable function, viz. the
Collatz functionf. The 2nd argument gives the natural number i to which f is to be applied. The 3rd argument gives a sequence x of computation steps simulating the evaluation of f on i (as an equation chain rather than a Gödel sequence number). The predicate call evaluates to true since x is actually the correct computation sequence for the call f(5), and ends with an expression not involving f anymore. Function U, applied to the sequence x, will return its final expression, viz. 1.
The definition depends on a suitable
Gödel numbering that assigns natural numbers to
computable functions (given as
Turing machines). This numbering must be sufficiently effective that, given an index of a computable function and an input to the function, it is possible to effectively simulate the computation of the function on that input. The predicate is obtained by formalizing this simulation.
The
ternary relation takes three natural numbers as arguments. is true if encodes a computation history of the computable function with index when run with input , and the program halts as the last step of this computation history. That is,
first asks whether is the
Gödel number of a finite sequence of complete configurations of the Turing machine with index , running a computation on input .
If so, then asks if this sequence begins with the starting state of the computation and each successive element of the sequence corresponds to a single step of the Turing machine.
If it does, finally asks whether the sequence ends with the machine in a halting state.
If all three of these questions have a positive answer, then is true, otherwise, it is false.
The predicate is
primitive recursive in the sense that there is a primitive recursive function that, given inputs for the predicate, correctly determines the truth value of the predicate on those inputs.
There is a corresponding primitive recursive function such that if is true then returns the output of the function with index on input .
Because Kleene's formalism attaches a number of inputs to each function, the predicate can only be used for functions that take one input. There are additional predicates for functions with multiple inputs; the relation
is true if encodes a halting computation of the function with index on the inputs .
Like , all functions are primitive recursive.
Because of this, any theory of arithmetic that is able to represent every primitive recursive function is able to represent and . Examples of such arithmetical theories include
Robinson arithmetic and stronger theories such as
Peano arithmetic.
Normal form theorem
The predicates can be used to obtain Kleene's normal form theorem for computable functions (Soare 1987, p. 15; Kleene 1943, p. 52—53). This states there exists a fixed
primitive recursive function such that a function is computable if and only if there is a number such that for all one has
,
where μ is the
μ operator ( is the smallest natural number for which is true) and is true if both sides are undefined or if both are defined and they are equal. By the theorem, the definition of every
general recursive functionf can be rewritten into a normal form such that the μ operator is used only once, viz. immediately below the topmost , which is independent of the computable function .
Arithmetical hierarchy
In addition to encoding computability, the T predicate can be used to generate
complete sets in the
arithmetical hierarchy. In particular, the set
which is of the same
Turing degree as the
halting problem, is a complete unary relation (Soare 1987, pp. 28, 41). More generally, the set
is a -complete (n+1)-ary predicate. Thus, once a representation of the Tn predicate is obtained in a theory of arithmetic, a representation of a -complete predicate can be obtained from it.
This construction can be extended higher in the arithmetical hierarchy, as in
Post's theorem (compare Hinman 2005, p. 397). For example, if a set is complete then the set
is complete.
Notes
^The predicate described here was presented in (Kleene 1943) and (Kleene 1952), and this is what is usually called "Kleene's T predicate". (Kleene 1967) uses the letter T to describe a different predicate related to computable functions, but which cannot be used to obtain Kleene's normal form theorem.
References
Peter Hinman, 2005, Fundamentals of Mathematical Logic, A K Peters.
ISBN978-1-56881-262-5