> The First Incompleteness Theorem tells us that assuming PA is consistent, one can formulate propositions that cannot be proved (nor disproved) on the basis of PA, but which are nevertheless true.

As far as I know, that last clause was never a claim made by Godel. Specifically the claim that these propositions are nevertheless true. This follows quite simply from the assumption that either a proposition is true, or its negation is true (i.e. the law of the excluded middle). But I recall reading that Godel, in his proofs, went to great lengths to avoid the law of the excluded middle over infinite sets.

Indeed, (again AFAIK) godel's first incompleteness theory still holds in constructive mathematics (roughly where the law of the excluded middle cannot be used). As such, I think the addition that these propositions are 'nevertheless true' actually hides a lot of complexity. Because there are philosophical positions in which these independent propositions are neither true not false.

And really, this is why we call them independent. The truthiness of these propositions is not determined by their axiom systems. It's a rather big philosophical stance to say that the 'truth' of these propositions can be determined outside of the axiomatic systems. It seems to me like that claims there is an objective (as in, not dependent on an axiomatic system) definition of what is true.