A wonderful book about the general pattern is Smullyan's Diagonalization and Self-reference (but it also goes more specifically into arithmetic). I also just found this recent article which contains an exposition of Lawvere's diagonalisation argument, which makes sense in cartesian closed categories...
Smullyan's page 17, adapted to Lawvere's setting seems to give a very general formal description of diagonalisation.