So it is perfectly okay to have a statement that is obviously true, but still cannot be proved using some set of axioms and rules.
The underlying reason is that if you imagine a Platonic realm where all abstractions allegedly exist, the problem is that there are actually multiple abstractions [“models”] compatible with ZF, but different from each other in many important ways.
So, when you say Godel’s sentence is obviously true, in which “abstraction” is it true?
Arguably, the numbers we care about. Set theory helpfully adds that second-order arithmetic (arithmetic using the language of sets) has only a single model (up to what is called ‘isomorphism’, meaning a precise analogy) and that Godel’s original sentence is ‘true’ within this abstraction.
So, when you say Godel’s sentence is obviously true, in which “abstraction” is it true?
Arguably, the numbers we care about. Set theory helpfully adds that second-order arithmetic (arithmetic using the language of sets) has only a single model (up to what is called ‘isomorphism’, meaning a precise analogy) and that Godel’s original sentence is ‘true’ within this abstraction.