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.