Gödel's proof method and fundamental theorem of arithmetic I am a novice to Gödel's proof (the theorem that consistency contradicts completeness), and, as it seems to me, he uses the fundamental theorem of arithmetic to uniquely number any formula. My question is: It seems like the proof is circular?

Note that $\sf PA$ proves the fundamental theorem of arithmetic (the usual proof goes through just fine), then $\sf PA$ proves that the encoding is unique.

It is important to note that the function mapping a formula to its number is _not_ internal to the model of $\sf PA$, a model of $\sf PA$ is not aware of the syntax which lives in "a different place". What happens is that we define a set of codes and some rules, and we prove that these codes and rules are, internally, similar to those of the language and logic, so we can talk about formula as if they were integers.

The key part is to show that the set of these codes (or at least the sets of relevant codes) are recursive, or recursively enumerable (and not recursive).