A very detailed, low-level proof of Gödel's incompleteness theorems is "[Finite sets and Go ̈del’s incompleteness theorems][1]". It's based on the theory of hereditarily finite sets, which is closely related to PA.


  [1]: http://journals.impan.gov.pl/dm/PDF/dm422-0-00.pdf