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


  [1]: https://www.impan.pl/en/publishing-house/journals-and-series/dissertationes-mathematicae/all/422//88124/finite-sets-and-godel-s-incompleteness-theorems