No. The idea is similar to that of Cantor’s diagonal argument, whuch implies that the real numbers, expressed as decimals, can’t be counted. So it involves assigning an integer to all propositions, that can be proven from the axioms-not, just, the axioms-and showing that this assignment implies the existence of an integer, that doesn’t belong to this set. This integer then corresponds to a proposition, for which, therefore, it can't be decided whether it's true or false.

Stam Nicolis , Ok, but first just at the level of axioms. If a system of axioms like plane Euclidean Geometry has only 5 axioms then there would be 5 Godel numbers, that are composite whole numbers that correspond, one to each axiom? Is that correct? Similarly, if there are 8 axioms that are in Zermelo-Fraenkel set theory then there would be 8 whole number that correspond to the 8 axioms under Godel's numbering system. Is that right? Does anyone ever list these 8 composite numbers?

No, because the specific numbers aren't required, there's not a unique choice. An example of how ``Gödel numbering'' works may be found here: https://seop.illc.uva.nl/entries/goedel-incompleteness/sup1.html. Another nice presentation is here: https://www.quantamagazine.org/how-godels-incompleteness-theorems-work-20200714/

Yes, I'm not trying to understand how the incompleteness theorem is proved, even if the impetus behind Gödel numbering is to prove the incompleteness theorem, but merely if there is an isomorphism between certain elements number theory and formal systems, including axioms and theorems. It sounds like you are saying that the relationship is not exactly an isomorphism since the numbering is not unique.

If you fix a Gödel numbering system and there are 5 axioms to the system, say the axioms of Euclidean geometry, then it seems as though there would be 5 primary composite numbers within this fixed system (corresponding to the axioms) as well as the other initially defined Godel numbers which would be fundamental to that system, the theorems would be arithmetic functions dependent on this set of fixed numbers even if the whole numbers are not unique.

Essentially I'm trying to understand if number theory as a subject can say anything about formal systems.

One other thing that no one seems to have brought up yet. If one works in first-order logic ... as is usual, then some axioms which would be single statements in second-order logic become axiom schemas, which are an infinite number of first-order statements. Examples are the Induction Axiom in Peano Arithmetic and the Separation and Replacement Axioms in ZFC. So when this occurs, the answer to your question is No ... infinitely many composite numbers would be needed to code the infinitely many first-order axioms that arise from a single second-order axiom.

@James Dudziak, thanks for the references to first and second-order logic and the example of the Induction Axiom in Peano Arithmetic. That....."infinitely many composite numbers would be needed to code the infinitely many first-order axioms that arise from a single second-order axiom." is very interesting. I'm curious to see what this would mean from an number-theoretic point of view, but again unfortunately, most references to Gödel Numbering seem to only stress its use in the proof of the incompleteness theorem.

Jason, since I don't know the context of your interest in having finitely many Gödel numbers, I cannot really say much. If you are interested in analyzing a single number theory proof in, say Peano Arithmetic, then, since a proof has finitely many steps, the number of axioms used in the proof would be finite, in particular, only finitely many instances of induction would be used.

My interest in having only finitely many Gödel numbers is that it is said that some systems such as plane Euclidean geometry have only a finite number of axioms. Assuming there are no unidentified Axiom Schemas in plane Euclidean geometry then there are only either 5 or a finite number of axioms. It would seem that if one mapped these 5 axioms to their Gödel numbers (after fixing a system of Gödel numbers), then these five numbers would be fundamental to all theorems deduced within Euclidean geometry if one mapped the theorems to their Gödel numbers. This seems to be implied by the logic of Gödel's analysis.

What I was thinking about in terms of number theory is more along the lines of "going in the other direction," starting with a result in number theory and then try to conclude something about formal systems or axioms. For example, does a series of Gödel numbers fit into something like a collection of generating functions. The Gödel numbers realized by the generating function are the Gödel numbers for an infinite number of axioms. For example, 1/(1 - x)^2, is the generating function for 1,2,3,4,5,...the whole numbers, or 1/(1-x)^3 is the generating function for 1,3,6,10, 15, ...the triangular numbers. These are not Gödel numbers since not all of the numbers in these sequences factor into the product of all primes less than a given prime where each prime is raised to a given number.

With regard to an axiom system for geometry handled in a manner that conforms to modern first-order logic, the article "What is elementary geometry?" by Alfred Tarski might be of interest to you. Tarski's formulation is also, in my humble opinion, incredibly elegant. It has one axiom schema, dealing with continuity, but usually one is only interested in a few instances of the schema, one being the Circle-Segment Axiom.

My knowledge of number theory and generating functions is nonexistent but my first impression with what you propose is that it might come to grief over what others have already mentioned, the arbitrary nature of Gödel numbering. The correspondence between statements and their Gödel numbers is anything but canonical.

With that, I've probably reached the end of my ability to say anything possibly useful! Best Wishes and Good Luck!

@James Dudziak, Thanks!

Jason Hadnot - the simple answer to your question is YES. The more complicated answer is that Godel numbering is just a coding of sentences into numbers. Yes, as has been pointed out there are many possible coding. The only thing that is really important is every sentence gets a unique representation as a number. The point about such a coding is that everything you can do to manipulate sentences can now be done by number theoretic functions. Schema present no particular difficulty, provided we get the coding right we can have a function for instantiating any instance of a schema i.e. a function that takes a number representing a schema and some numbers representing the items to be instantiated and delivers a number representing the instantiation.

One minor aside on the number of axioms: any finite list of axioms can, of course, be represented as a single conjunctive axiom, and so can be made to correspond to a single number under coding.

Jason Hadnot ; James Dudziak

From what I understand, you are asking whether it is sensible to investigate the nature of numbers coding axioms (finitely many) of a given theory, or more generally, study a formal theory with respect to its coding and see whether it is possible to "extrapolate" from theorems provable in this theory a number representing a code of a formulation of an axiom. It has already been said that the Gödel numbering used in the proof of the Incompleteness theorem is canonical and probably given its computational inefficiency maybe also inadequate for this particular question (again, assuming that I understood your question correctly).

However, the main idea of understanding how theorems are, in some sense, computationally linked to the premises which entail them is a very interesting question. It is clear that the possibility of arithmetizing a formal theory enables to provide a number theoretical interpretation to the objects of a formal theory (syntax, semantics and proof theory). In this sense, one could ask whether it is possible to find a "preferable" coding for a formal theory in order to make your question easier to formulate and answer. This is of course extremely vague, but to make things more precise, you could try to pick a specific theory (Euclidean Geometry), formalise the axioms and define different codings and see whether, with respect to what you are trying to investigate, it is possible to establish how a particular choice of coding affects the nature of the numbers coding your axioms.

Finally, I wanted to conclude by referring to a recent program in mathematical logic called Reverse Mathematics. They are basically trying to isolate axioms from theorems (which is some sense related to the remark you made "[..]going in the other direction, starting with a result in number theory and then try to conclude something about formal systems or axioms.") and they actually use a lot of computability theory and subsystems of second-order arithmetic. I am not an expert on this particular topic, but I suggest you to look into it if you are interested.

I would be happy to carry on this discussion with you and also, if during the past year you obtained some interesting results that you can share, I would be glad to hear them.

Thank you and best regards!

Jean Paul Schemeil

Links for Reverse Mathematics:

Simpson, Stephen G. (2009), Subsystems of second-order arithmetic, Perspectives in Logic (2nd ed.), Cambridge University Press, doi:10.1017/CBO9780511581007, ISBN 978-0-521-88439-6, MR 2517689

https://en.wikipedia.org/wiki/Reverse_mathematics