A very detailed, low-level proof of Gödel's incompleteness theorems is
- S. Świerczkowski, Finite sets and Gödel’s incompleteness theorems, Dissertationes Mathematicae 422 (2003), 1-58, https://eudml.org/doc/285944
It's based on the theory of hereditarily finite sets, which is closely related to PA.
