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