I am interested in understanding how Godel was able to prove his two celebrated theorems. I usually start with the most elementary book (something that perhaps a high school kid can understand) in order to gain perspective and then, I move on to more advanced books. Following that strategy, I read the book Godel's Proof written by Ernest Nagel, James R. Newman, and Douglas R. Hofstadter, and it did give me the basic idea involved in his proofs. However, it is far from a rigorous treatment just as the authors mention in that book.
After reading the book multiple times, I still have this unsettling feeling about Godel's proofs. He defines Godel numbers in a certain way, which now requires us to trust ourselves with the 'concept of numbers' which is itself, a part that is developed from the axioms.
Specifically, we have the number 0 defined as the empty set, the number 1 as the set containing the empty set etc. Using basic axioms of set theory, the 'concept of numbers' is developed and hence, have their own formulas describing as to exactly what a number is.
Note however, that the Godel numbering, is using 'the concept of numbers' and hence, is using these formulas, which in turn are developed from basic axioms, in order to number other formulas developed using the same axiom system. Can you really assign to each formula developed in the axiom system, a number, which itself is essentially a formula developed from the axioms of the same system? Isn't that circular logic?
I am perhaps getting this doubt because I lack the knowledge of the rigorous proof that Godel came up with. However, with the limited knowledge that I have, I'm not able to pull myself out of this unsettling feeling that there is circular logic in Godel's theorems.
I would greatly appreciate it if you can explain to me as to where my thinking is wrong.
If you have programming background, you should be able to understand this computability-based explanation of the incompleteness theorems, at least until the section titled "Explicitly independent sentence". It will take a significant amount of time and mental effort to work through it, but I can guarantee it is much easier to grasp than a rigorous explanation using the conventional approach (i.e. via the fixed-point lemma).
I cannot really make sense of your doubt about circularity, and I suspect (as you also did) that it is due to your current lack of a rigorous proof of the incompleteness theorem. So perhaps after you understand the proof you will either have no more doubt or you will be able to make precise your inquiry. In the meantime, it might be worth keeping in mind that the incompleteness theorems are themselves theorems of some formal system MS, which is often called the meta-system. MS does not need to assume much; it more or less just needs to support basic reasoning about finite strings, so that you can reason about programs and program execution, which are used (as per the linked post) to define general formal systems, and so that you can reason about formal systems that can reason about programs.
I also want to note that Godel numbering is not actually the core of the incompleteness theorems. It is necessary if you want to prove that theories of arithmetic like PA or PA− or Q are incomplete, but the incompleteness phenomenon is not due to the ability to encode finite sequences of natural numbers as a single natural number and decode it via arithmetical formula. I say a bit more here.
But note that a formal system that is able to reason about programs of course can reason about its own proof verifier, at least to verify that itself proves a theorem if it really does. That is not circular in any sense; an analogy is that you can write a program in any decent programming language L that expects an input (P,X,k) where P is a program in L and X is an input for P and k is a natural number, and outputs "yes" if P on input X halts within k steps, but outputs "no" otherwise. This program is written in L and verifies halting execution of programs written in L. No circularity!