"true but unprovable" ... bugs me
Rightly so. "Unprovable" means unprovable in some particular system. A refinement of a system by adding more axioms and rules might make one of Gödel's pair p|~p provable. We expect to get new truths from a system through deductions. But we must specify what the system includes.
first---
I suppose a dumb, simple-minded example might start with a little finite set {a , b}, where a and b are specified to be distinct elements. A binary operation "*" might be specified for these elements: * == {<<a, a>, a>, <<b, b>, b>, <<a, b>, b>, <<b, a>, b>}.
So the following statements are logical atomic TRUE statements in this system:
a * a = a, b * b = b, a * b = b, b * a = b.
The axioms might be specified as:
a = a, b = b, a * a = a, b * b = b. (note: no mention of anything like "a * b" or "b * a" in these axioms)
The deduction rules might allow substitutions of equalities and consequences of applied modus ponens.
This happens to be (by specification) a semigroup under *, but not a group. {a} and {b}, with the appropriate parts of *, form separate subgroups.
OK. a~=b, a * b = b and b * a = b are true in this system, but I don't think they can be proven using these axioms. It's not a provable system.
But we already know the logical atomic truths of this system, so we can deduce basic logical molecular truths from these by enjoining them and their negations into complex expressions. It is as complete (in the sense of Gödel) as propositional logic and predicate logic allow it to be.
Adjoin some more axioms (like a * b = b and b * a = b) and you might get a new system that is provable.
done---
Gödel admits that you can add the independent p (or else its negation ~p) as a new axiom to an arithmetic system and make a new system that is equally as consistent as the starting system. But now (since the new system still has the power to generate arithmetic) he will create a new imaging into the new system and recreate his result. Another true but unprovable statement is revealed.