[Tainnor]

> It's just that Godel's proof cannot be rendered in PA

This is incorrect, the proof can be carried out in very weak subsystems of PA.