# T_1=PA+(all true independent statements of PA)

Given Peano Arithmetic PA, is it possible to form the theory $T_1=PA$+{all true but unprovable statements of PA}?

Then define $T_{n+1}=T_n$+{all true but unprovable statements of $T_n$}

Then let $Q=T_{\infty}$. Is it possible to say anything about Q? Is it a well-defined theory? Is it consistent? Does Godel's second theorem apply to it? Is it possible to construct a true unprovable statement of Q?

Also, what is the system in which we deduce a statement to be true but unprovable in another system, what are the additional axioms?

-
"True" in what model? There is a model where the Goedel statement $G$ is true, and one where the Goedel statement is false (that's why it's formally undecidable); so, do we add $G$ or do we not add $G$? –  Arturo Magidin May 9 '11 at 19:03
@pi_yum_yum: You learned wrong; the Goedel statement is not "this statement is unprovable", the Goedel statement is "there does not exist $n$ such that $n$ satisfies the following arithmetical property"; it is only in the metalanguage that it can be interpreted as making a statement about provability. The Goedel statement is formally undecidable, which means there are models where it is false (assuming PA is consistent). "Truth" is about models, "provability" is about formal theories. You are conflating the two; if you want to talk about "truth", you need to specify a model. –  Arturo Magidin May 9 '11 at 19:11
If you mean true in the standard model, then your $T_1$ is called true arithmetic. It's already a complete theory (every sentence is either true or false in the standard model), so there's nothing more you can add without either expanding the language or becoming inconsistent. –  Chris Eagle May 9 '11 at 19:12
Or more generally: if you fix a model $M$ and by "true" you mean "true in $M$", then the theory is complete and consistent (assuming consistency of PA) because every sentence is either true in the model or false in the model. But, assuming Church's Thesis, we have no algorithmic way of determining if a given statement $S$ is in $T_1$, or its negation is. –  Arturo Magidin May 9 '11 at 19:17
@Arturo: It is standard usage to say "true" in the context of PA to mean "true of the standard model". If working with set theories, "true" would mean "true in the universe of sets". –  Andres Caicedo May 9 '11 at 20:43

Assuming "true" refers to a particular model, any statement in $T_1$ that is true but unprovable (in $T_1$) is already unprovable in $PA$, so your recursion stops: $T_\infty = T_2 = T_1$. Any statement in $T_1$ that is true is either provable in $PA$ or is an axiom of $T_1$, so it is provable in $T_1$. But Goedel's theorems don't apply to $T_1$, because there is no formula expressing the statement "$A$ is an axiom of $T_1$".