Proving the existence of a $\Pi_1$-sentence in True Arithmetic that is independent of Peano Arithmetic

computabilitylogic

I am trying to wrap my head around how to prove the following statement:

There exists some $\Pi_1$-sentence $A$ such that $A \in \textbf{TA}$ but $\{A, \neg A\} \cap \textbf{PA} = \emptyset$.

$\textbf{TA}$ represents True Arithmetic which is the set of statements in the language of arithmetic that are true under the natural model $\underline{\mathbb{N}}$. $\textbf{PA}$ represents Peano Arithmetic which is the set of statements in the language of arithmetic that are logical consequences of the set of Peano axioms $\Gamma$. In this context, we are under the assumption that $\textbf{PA}$ is, in fact, sound.

Under the assumption of soundness of $\textbf{PA}$ and its axiomatizability we can begin to prove parts of this statement. If $A \in \textbf{TA}$ then we are sure that $\neg A \notin \textbf{PA}$ by the soundness of $\textbf{PA}$; moreover, since $\textbf{PA}$ is axiomatizable (hence $\Gamma$ is recursively enumerable) by the completeness of the first-order $LK$ proof system if $A \in \textbf{PA}$ then $\textbf{PA} \vdash A$. With this in mind, the main statement I am interested in proving might be the following:

There exists some $\Pi_1$-sentence $A$ such that $A \in \textbf{TA}$ but $\textbf{PA} \not\vdash A$.

Is this going to just be a simple usage of the Godel sentence $G$ or am I missing something?

Best Answer

Yes, this is just an application of Godel's theorem. The sentence "PA is consistent" is already $\Pi_1$ ("every $x$ is not the code for a PA-proof of $0=1$"). And we know that it's in TA (obvious) and not PA-provable (Godel).

This also works for the sentence whipped up in the proof of the first incompleteness theorem - that's also $\Pi_1$, in TA, and not PA-provable - but I find working with consistency statements a bit more concrete at first.