Is Godel's G statement an arbitrary construction or is it derived by rules?

Question

Godel's proof involves a statement G. I undestand that it is losely arranged to look like "This statement G is not provable in this sytem". My question is how this statement was created and used in Godel's proof. Is the statement just an arrangement of symbols that is then analyzed and shown to be undecidable by the rules of the system in which it is composed? Or, is this statement a careful construction that is derived by the rules in the first place, and it is a result of the system? I am trying to understand if the statement is arbitrarily chosen to show how the system resolves the statement using a proof, or if the statement is a result of the system's axioms and rules. Is there a better explanation as to how the statement is constructed?

Answer 1

"Is this statement a careful construction that is derived by the rules in the first place, and it is a result of the system?" I'm not sure what this really means. But recall, the whole point of a Gödel sentence $G_T$ for the theory $T$ is that it is not derivable by the rules of $T$, is not a "result" of the system!

If, however, you are asking how Gödel himself arrives at the construction of the statement $G$, the underlying "diagonalization" idea is a fairly simple one (though not "derived by rules"). But you need to understand something here of the background ideas of Gödel-numbering, and how that allows for facts about proofs to be coded up as arithmetical facts, before you can really understand how the diagonalization works to give Gödel what he wants.

For more, take a look, for example, at the explanations in my Gödel Without (Too Many) Tears downloadable from https://logicmatters.net/igt. Or for other textbook explanations -- and there are some wonderful options here -- see the recommendations in Ch. 6 of the Beginning Mathematical Logic Study Guide, freely downloadable at https://logicmatters.net/tyl.