A wonderful book about the general pattern is Smullyan's Diagonalization and Self-reference (but it also goes more specifically into arithmetic). I can't resist to makealso just found this answer self-referringthis 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.