I realized that AFT stands for Axiomatized Formal Theory.
There is Church's theorem that says that pure first-order predicate calculus is not decidable. This is proved by showing that Turing machines can be encoded in predicate calculus and the fact that a machine halts can be expresses as a formula. There is also a theorem that Robinson's system $Q$ (Peano Arithmetic without induction) is undecidable. This is proved by showing that computable functions are representable in $Q$. Again, for each machine and input there exists a formula saying that the machine halts on that input, and the machine indeed halts iff that formula is provable.
These two results can be found, for example, in the Open Logic Project books "Sets, Logic, Computation" and "Incompleteness and Computability". Another comprehensive book that deals with this is Computability and Logic by Boolos et al.
The diagonal argument is used, in particular, in the proof of second Gödel's theorem about incompleteness of Peano Arithmetic.