Why is it OK to rely on the Fundamental Theorem of Arithmetic when using Gödel numbering?

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

Gödel's original proof of the First Incompleteness theorem relies on Gödel numbering. Now, the use of Gödel numbering relies on the fact that the Fundamental Theorem of Arithmetic is true and thus the prime factorization of a number is unique and thus we can encode and decode any expression in Peano Arithmetic using natural numbers.

My question is, how can we use a non-trivial result like the Fundamental Theorem of Arithmetic in the meta-language that describes Peano Arithmetic, when, the result actually requires a proof from within Peano Arithmetic itself, not like other trivial things we believe to be true (i.e. existence of natural numbers and the axioms for addition and multiplication which we want to interpret in the natural way - Platonism)?

I understand we could instead use a different way of enumeration, e.g. a pairing function and the Chinese Remainder Theorem or simply string concatenation, but, then the need for a proof of uniqueness when encoding and decoding remains and in general, I am interested in the structure of Gödel's original proof.

Basically, I have two ideas of how it might be possible to resolve this:

1. Prove the Fundamental Theorem of Arithmetic within a different sound (?) system.

2. Maybe there is nothing needed to be done to 'resolve' this, because I am just misinterpreting something and it is actually acceptable to use provable sentences of PA in the meta-language.

EDIT: I have realized how to make my question less confusing:

Say PA proves FTA. Then if we only assume PA is consistent, that does not rule out the possibility of FTA being false. Now, if FTA is false, then PA and the meta-language too includes a false statement and thus the whole proof is useless.

How is this resolved? Is it maybe related to the fact the originally we actually assume $\omega$-consistency and obviously, for each natural number $n$ separately its unique prime factorization can simply be found algorithmically?

-

2
The theorem states that your theory cannot be both consistent and complete, so it's a win-win. I don't see the problem. – Thierry Zell Jan 29 2011 at 4:28
It has been a while since I worked through that proof, but is the unique factorization really needed or just a canonical one (without the fact that as it happens it is unique)? What if you use a greedy factorization where you divide out all 2's you can then all 3's (from what is left) then all 4's etc. That gives a code. – Aaron Meyerowitz Jan 29 2011 at 20:51

6
Why are number theorists allowed to use numbers? Shouldn't they first establish that it is safe to use them? – Andrej Bauer Jan 30 2011 at 8:32

3
The point of my question is this: if all other mathematicians are allowed to take numbers for granted, why isn't Gödel? All he does is apply the mathematical method to the study of a certain system for manipulation of symbols known as "first order logic" and "Peano arithmetic". The subject of his study is no less mysterious, magical, or "fundamental" as all the other subjects of study in mathematics. – Andrej Bauer Jan 30 2011 at 18:49

4
And I am sure Gödel knew how to prove the fundamental theorem of arithmetic. Perhaps I should have been more precise: when Gödel does mathematics is allowed to use whatever mathematics is considered "standard" by his peers. My pet peeve is this: why do "ordinary" mathematicians think that "logicians" must secure the ground on which they stand, when those same mathematicians stand on the same ground together with logicians? – Andrej Bauer Jan 31 2011 at 13:40
show 2 more comments

5 Answers

Just like most mathematical theorems, you can formalize Godel's Theorems in some first order language (with some "standard" interpretation under which the formalization means what it's supposed to mean), turn the proof into a purely syntactic string of formulas, and figure out which formulas in that first order language are needed as axioms. I'm embarrassed to say I don't know exactly how strong the assumptions we need are to carry out the proof of Godel's Theorems, but there will be some weak fragment of ZFC probably not much stronger than PA which will do. So we would be using a theory slightly stronger than PA to establish the incompleteness of PA, but why should that be a problem?

The axioms needed for the proofs of Godel's Theorems are probably pretty natural, probably pretty close to PA, and probably have a natural interpretation. If you believe these axioms have this interpretation, then you would have no problem with Godel's proofs or the interpretation of the theorems. If not, then you're probably pretty close to believing PA is inconsistent, in which case you would probably:

1. Accept that the formalized versions of Godel's Theorems follow from whatever axioms are used, but only because you believe those axioms are inconsistent.
2. Deny that the formalized versions of Godel's Theorems mean what they're supposed to mean, and just regard what's happening in point 1 as a valid string of symbolic manipulations.
3. Accept the natural language meaning of Godel's Theorems, in spite of point 2, for trivial reasons, since they say, "if PA is consistent, ..."

EDIT: (in response to your edit) So we're assuming PA proves FTA, PA is consistent, and FTA might be false? What do you mean by "false," you mean false in the standard intepretation? In that case, PA would be false in the standard interpretation. Now if we take Godel's first theorem to say, "If PA is consistent, then there is a true formula in the standard interpretation which is not provable from PA," then this meta-theorem is certainly true.

EDIT: Ignas requested an explanation of some of the basics to make sense of my claim, "If PA proves FTA, and FTA fails in the standard model, then so does PA." It's too big to fit in a comment so I'm adding it to my response:

Let $\mathcal{L}$ denote the first order language of number theory, we'll have lower case Greek letters vary over sentences of $\mathcal{L}$, upper case Greek letters vary over sets of sentences of $\mathcal{L}$, and upper case Roman letters vary over $\mathcal{L}$ structures. We write $M \vDash \varphi$ to denote that $\varphi$ is true in the model $M$, i.e. when its symbols are interpreted according to $M$. Tarski's definition of truth for a sentence in a given model is by recursion on the complexity of the sentence. We write $M \vDash \Sigma$ if every member of $\Sigma$ is true in $M$. We write $\Sigma \vDash \varphi$ if for every $M$, $M \vDash \Sigma$ implies $M \vDash \varphi$, i.e. if every model of $\Sigma$ is also a model of $\varphi$.

For provability, we write $\Sigma \vdash \varphi$ to say that there is a (finite) proof of $\varphi$ using (finitely many) sentences from $\Sigma$ as axioms.

The Soundness Theorem states that for all $\Sigma ,\ \varphi$, if $\Sigma \vdash \varphi$ then $\Sigma \vDash \varphi$. It's this theorem, with PA in place of $\Sigma$ and FTA in place of $\varphi$, that I'm using to establish the claim you're asking about. The converse of this theorem is also true; it's Godel's Completeness Theorem. Putting these two theorems together, they say that the relations $\vdash$ and $\vDash$ are the same relation between sets of sentences and sentences. One (perhaps not immediately obvious) way to rephrase this is, "being true in every model is the same as being provable from no axioms." Contrast this Godel's Incompletness Theorem, which says that "being true in the standard model of number theory is not the same as being provable from PA."

-

1
I am pretty sure that the incompleteness theorems can be proved in PA. I.e., you can prove something like "if ZFC is consistent then so is ZFC+$\neg$Con(ZFC)" in PA (the same for ZFC replaced by weaker theories such as PA itself). – Stefan Geschke Jan 29 2011 at 5:58
I guess it depends on how you word Godel's Theorem. Take the first one for instance. If it says something like, "if basic arithmetic is consistent, then there's a formula that's true in $\mathbb{N}$ but not provable from basic arithmetic" then to express this you need some theory capable of expressing "true in $\mathbb{N}$." PA can't even talk about $\mathbb{N}$. I suppose there may be equivalent formluations of Godel's Theorem which sidestep the need to talk about $\mathbb{N}$, but then the question becomes: What axioms do you need to prove that equivalence? – Amit Kumar Gupta Jan 29 2011 at 6:09
I see. This is not a problem if you formulate the first incompleteness theorem as something like "if T is r.e. axiomatizable, consistent, and allows representations of recursive functions and relations, then T is incomplete". This gets you that PA is incomplete (if consistent, which we all believe to be the case) and once you are in a theory that allows it to talk about $\mathbb N$ in any reasonable way, then you get the theorem in the form that you quote. – Stefan Geschke Jan 29 2011 at 6:23
@Amit Kumar Gupta: whatever metatheory you formalize the proof in can talk about $\mathbb{N}$, though. – Carl Mummert Jan 30 2011 at 23:14
Regarding your edit: Yes, I meant false under standard interpretation. What do you mean by "PA would be false"? Inconsistent? Well, it does not have to be as long as PA does not prove $\neg$FTA. What am I misunderstanding here? – Ignas Jan 31 2011 at 0:32
show 4 more comments

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.

Stefan has explained the essential points well, but let me add some details and a reference. For the first incompleteness theorem, one can work with a very weak theory of arithmetic. One needs to be able to define the relevant recursive predicates and functions (in particular those that describe the coding process) and prove that these represent, in the theory under consideration, the intended functions and relations. Here "represent" is a rather weak requirement. A formula $\phi(x,y)$ represents a function $f$ in a theory $T$ if, for each natural number $n$, $T$ proves the formula `$(\forall y)(\phi([n],y)\iff y=[f(n)])$`, where the square brackets mean the numeral for the number inside. (Note that $T$ need not prove `$\forall x\exists y\phi(x,y)$`.) A weak theory like Robinson's Q suffices to represent all recursive functions and predicates, so the first incompleteness theorem applies to all theories with at least the strength of Q. For the second incompleteness theorem, on the other hand, one needs to prove, in the theory under consideration, some basic properties of the coding, for example that concatenations can always be coded. PA suffices for this (and so do some weaker theories; `$\Sigma^0_1$` induction seems to suffice). So the second incompleteness theorem is usually stated for theories that have at least the strewngth of PA. The details of what needs to be proved, as well as most of the details of the proofs, can be found in Shoenfield's book "Mathematical Logic"; I believe they're also in Goedel's original paper. (I'm away from home and writing this on an unfamiliar computer, which I can't persuade to preview any of my TeX code, so I apologize if it contains errors.)

-
@Andreas , do you know of a reference that pursues the question of how little/much of PA is actually required? I seem to recall "Metamathematics of first order arithmetic" treats some of this, but don't recall the explicit suggestion that $\Sigma^0_1$ induction seems enough (I do not have the book with me, though, so I cannot currently check). – Andres Caicedo Jan 29 2011 at 20:59

2
I learned only recently that Pudlak proved in 1985, by model-theoretic techniques, that Q does not prove Con(Q), along with finer results. This is in the paper "Cuts, consistency statements and interpretations" from the JSL volume 50. I don't think that anyone has proved a sort of reverse-mathematics result that characterizes the amount of induction required to verify the Hilbert-Bernays conditions. $Sigma^0_1$ induction is certainly enough, but I don't remember about weaker theories at the moment. – Carl Mummert Jan 30 2011 at 23:12
@Carl, many thanks! I'll check the reference. – Andres Caicedo Jan 31 2011 at 1:03
Feferman proves a version of the second incompleteness theorem in his system $FS_0$: citeseerx.ist.psu.edu/viewdoc/… I don't think $FS_0$ is weaker than $\Sigma_1$ induction though. – Timothy Chow Jan 31 2011 at 15:58

I am not absolutely sure I understand your problems with the meta-language and such.
You take your favorite base theory, let's say PA or something stronger like ZFC. But I am quite sure that PA is enough. You prove the fundamental theorem of arithmetic in PA (or rather, a la Goedel, you prove that the $\beta$-function does what it is supposed to do). This tells you that you can code finite sequences and hence that you can talk about strings, languages, and proofs.

Now you continue and define a formula Con(PA) that expresses that PA is consistent. In the same way you can define a formula Con(PA+$\neg$Con(PA)), that expresses the obvious thing. Note that the PA that appears in these formulas is not the meta-mathematical PA but the internal PA of the model that you are in. Anyhow. This is just the usual confusion that arises with the incompleteness theorems. Now you prove, still only using PA, the statement "Con(PA) implies Con(PA+$\neg$Con(PA))" and you are done.

This is a purely number theoretic proof.

-

Here is a way to think about it. When you use something like Fund Theorem of Arithmetic to prove Godel numbering, you are referring to the abstract set $\mathbf N$, which "exists". The Fundamental Theorem of Arithmetic is simply true about this set, irrespective of any logical system which one is constructing. If you like, you can prove the Fundamental Theorem of Arithmetic, more or less rigorously, in a metalanguage. But the proof in this metalanguage is completely orthogonal to any proofs one might construct in the logical system, such as Peano axioms.

-

1
This may well be true, but it is not the issue at hand. The numbering of formulas and its reliance or not on the FTA happens inside the theory (as explained by the answers below). – Andres Caicedo Jan 29 2011 at 22:14

1
Oh no no no, that would be pretty much the worst case, since claiming that FTA is "simply true" would render the whole proof rather vague and non-rigorous. And on the contrary, as Andres pointed out, the proofs in the meta-language are actually established within PA itself, since PA is the meta language too. – Ignas Jan 30 2011 at 1:39

1
The Godel incompleteness theorem shows that $Th(\cal N)$ is undecidable. Any first-order statement, such as FTA, which is true on $\mathbf N$ is part of $Th(\cal N)$. Proving that it is part of $Th(\cal N)$ can be regarded as simply a fact (which one prove if one wishes). – David Harris Jan 31 2011 at 23:24

It's a trick of encoding. You encode the formulas of the theory into a fixed collection of integers which have a certain form.

Now, you have defined somewhere in the background a natural notion of multiplication, addition, and equality of integers. So you are free to ask questions about whether or not two numbers are equal, and whether or not for some number $x$, there is a formula in the language of PA, for which $x$ is the encoding of, and this allows you to go backwards, in the metatheory. (that is take a number and see if it encodes a sentence)

That being said, you are never starting with a number and going backwards in the formal theory (that is to say turning it into the sentence it encodes, as this would require FTA), you are always going forward, taking the Gödel encoding of a given sentence.

It's this careful dance and intermingling of the syntax and semantics that makes the proof of this theorem so much fun to go over.

Hope this clears it up a little bit. I know it probably doesn't completely answer your question.

-
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 58, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": false, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.3, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.946240246295929, "perplexity_flag": "head"}