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://doi.org/10.4064/dm422-0-1 

It's based on the theory of hereditarily finite sets, which is closely related to PA.