[lisper]

> the first incompleteness theorem tells us that any logical framework which can express Peano arithmetic must necessarily contain true (resp. false) facts for which no (resp. counter) proof can be given.

Not quite. Any logical framework which can express Peano arithmetic must necessarily contain true facts for which no proof can be given within PA. The proof of Godel's theorem itself is a (constructive!) proof of the truth of such a statement. It's just that Godel's proof cannot be rendered in PA, but even that is contingent on the assumption that PA consistent, which also cannot be proven within PA if PA is in fact consistent. In order to prove any of these things you need to transcend PA somehow.

[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.