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.
