# Why is Godel's first theorem not a proof from the inside?

Why is Godel's first theorem not a proof for the truth of the so called undecidable proposition? You may say it's a proof from the outside, but if not all proofs from the outside be formalized inside the system then the system is really not powerful.

-
Could you state the version of Godel's first theorem you are working from? –  Colin McQuillan Jan 10 '11 at 12:42
@Zirui: In fact, Goedel notes (though never actually goes on to prove since he never gave the second part of his paper) that one can formally prove within the system that $\mathrm{Con}(T)\rightarrow \mathrm{G}$, where $\mathrm{G}$ is the Goedel statement and $\mathrm{Con}(T)$ is the consistency of $T$. That's the 2nd Incompleteness Theorem; so one can mirror part of Goedel's argument "inside" the system. However, the argument for the "truth" of G is an argument about the standard model, not about the theory. –  Arturo Magidin Jan 10 '11 at 16:47
@Zirui: You need to state the precise version of first incompleteness you are talking about. There are many versions, and their hypotheses vary in ways that affect the answer to your question. –  Andres Caicedo Jan 10 '11 at 18:30
@Zirui Wang: The Goedel statement is an objective statement about numbers; it does not, in fact, assert its own provability. The latter is an interpretation we can give to the objective statement about numbers in the metatheory. Because this is happening in the metatheory, there is no reason to assume that such an argument can be done formally within the theory; moreover, that argument is being done about the standard model of the theory, as I noted above; a formal theory cannot refer to its own "standard model". (cont...) –  Arturo Magidin Jan 12 '11 at 17:54
@Zirui Wang: (cont...) Finally, as I noted above, the argument Goedel makes is that if the theory is consistent, then $G$ must be true (in the standard model). This is in fact the statement $\mathrm{Con}(T)\rightarrow G$. And the Second Incompleteness Theorem shows that in fact you can formally prove $\mathrm{Con}(T)\rightarrow G$ in the theory; this is why we know that you cannot formally prove $\mathrm{Con}(T)$ (because we know we cannot formally prove $G$, and if you could formally prove $\mathrm{Con}(T)$, then by modus ponens you would be able to formally prove $G$). –  Arturo Magidin Jan 12 '11 at 17:56