What I don't understand is how to extract information from the number that encode the computation history.
I know it's defined in Kleene's Introduction to Metamathematics. But what page?
References are welcome. More information on Kleene's T predicate can be found here.
On
The description given on Wikipedia is adequate for most purposes:
The ternary relation $T_1(e,i,x)$ takes three natural numbers as arguments. The triples of numbers $(e,i,x)$ that belong to the relation (the ones for which $T_1(e,i,x)$ is true) are defined to be exactly the triples in which $x$ encodes a computation history of the computable function with index $e$ when run with input $i$, and the program halts as the last step of this computation history. That is, $T_1$ first asks whether $x$ is the Gödel number of a finite sequence $\langle x_j \rangle$ of complete configurations of the Turing machine with index $e$, running a computation on input $i$. If so, $T_1$ 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, $T_1$ finally asks whether the sequence $\langle x_j \rangle$ ends with the machine in a halting state. If all three of these questions have a positive answer, then $T_1(e,i,x)$ holds (is true). Otherwise, $T_1(e,i,x)$ does not hold (is false).
A more thorough (but still somewhat informal) discussion is given in Enderton's chapter of the Handbook of Mathematical Logic. Formal details of Gödel coding are given in Smorynski's chapter of the same Handbook. Before embarking on this, Smorynski writes:
The details of an encoding are fascinating to work out and boring to read. The author wrote the present section for his own benefit and his feelings will not be hurt if the reader chooses to skip it.
Wikipedia also gives details on Gödel numbering for sequences.
My recommendation is that you work out your own encoding in full detail. This is a valuable and interesting exercise that is best done in private...
On
Shoenfield's Recursion theory also contains a detailed construction of Kleene's $T$ predicate. It can freely be downloaded from Link
There is also a more indirect proof method, which is to first show that any computable relation is definable in arithmetic and then note that the relation represented by the T predicate is computable. In fact the relation is primitive recursive, but the computability is easier to see, via Church's thesis. Also, not only the computable relations are definable, all the arithmetical relations are also definable.
The proof that every primitive recursive relation (or function) is representable in arithmetic is somewhat easier than a proof specifically for the T predicate, because you can ignore details of Turing machines. Essentially the only issue is proving that one can quantify over finite sequences. There is a complete proof in many textbooks and in section 2.2 of these lecture notes by Stephen Simpson: http://www.math.psu.edu/simpson/notes/fom.pdf .
There is also a proof in section 49 of Kleene's Introduction to metamathematics, at least for primitive recursive functions. The general result for arithmetical relations follows immediately by simply adding quantifiers and using the normal form theorem from computability to show that one-quantifier relations are definable. This may require proving that the T predicate is primitive recursive, but this is easier than proving it is representable in arithmetic, because one can use primitive recursion freely without having to worry about the $\beta$ function at the same time.