A wonderful book about the general pattern is Smullyan's [Diagonalization and Self-reference][1] (but it also goes more specifically into arithmetic). I also just found [this][2] 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.

  [1]: http://books.google.com/books?id=uH53QgAACAAJ&dq=smullyan+self-reference&hl=en&ei=nx2aTNH3LZSTOOfHwLkJ&sa=X&oi=book_result&ct=result&resnum=1&ved=0CCUQ6AEwAA
  [2]: http://arxiv.org/abs/1006.0992